]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/ac.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / ac.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/arith/nat_le.ma".
16 include "static_2/notation/functions/one_0.ma".
17 include "static_2/notation/functions/two_0.ma".
18 include "static_2/notation/functions/omega_0.ma".
19
20 (* APPLICABILITY CONDITION **************************************************)
21
22 (* applicability condition specification *)
23 record ac: Type[0] ≝ {
24 (* applicability domain *)
25    ad: predicate nat
26 }.
27
28 (* applicability condition postulates *)
29 record ac_props (a): Prop ≝ {
30    ac_dec: ∀m. Decidable (∃∃n. ad a n & m ≤ n)
31 }.
32
33 (* Notable specifications ***************************************************)
34
35 definition apply_top: predicate nat ≝ λn. ⊤.
36
37 definition ac_top: ac ≝ mk_ac apply_top.
38
39 interpretation "any number (applicability domain)"
40   'Omega = (ac_top).
41
42 lemma ac_top_props: ac_props ac_top ≝ mk_ac_props ….
43 /3 width=3 by or_introl, ex2_intro/
44 qed.
45
46 definition ac_eq (k): ac ≝ mk_ac (eq … k).
47
48 interpretation "one (applicability domain)"
49   'Two = (ac_eq (nsucc nzero)).
50
51 interpretation "zero (applicability domain)"
52   'One = (ac_eq nzero).
53
54 lemma ac_eq_props (k): ac_props (ac_eq k) ≝ mk_ac_props ….
55 #m elim (nle_dec m k) #Hm
56 [ /3 width=3 by or_introl, ex2_intro/
57 | @or_intror * #n #Hn #Hmn destruct /2 width=1 by/
58 ]
59 qed.
60
61 definition ac_le (k): ac ≝ mk_ac (λn. n ≤ k).
62
63 lemma ac_le_props (k): ac_props (ac_le k) ≝ mk_ac_props ….
64 #m elim (nle_dec m k) #Hm
65 [ /3 width=3 by or_introl, ex2_intro/
66 | @or_intror * #n #Hn #Hmn
67   /3 width=3 by nle_trans/
68 ]
69 qed.