1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "delayed_updating/syntax/prototerm.ma".
16 include "delayed_updating/notation/functions/m_hook_1.ma".
17 include "delayed_updating/notation/functions/hash_1.ma".
18 include "delayed_updating/notation/functions/tau_2.ma".
19 include "delayed_updating/notation/functions/lamda_1.ma".
20 include "delayed_updating/notation/functions/at_2.ma".
22 (* CONSTRUCTORS FOR PROTOTERM ***********************************************)
24 definition prototerm_node_0 (l): prototerm ā
27 definition prototerm_node_1 (l): prototerm ā prototerm ā
28 Ī»t,p. āāq. q Ļµ t & lāq = p.
30 definition prototerm_node_1_2 (l1) (l2): prototerm ā prototerm ā
31 Ī»t,p. āāq. q Ļµ t & l1āl2āq = p.
33 definition prototerm_node_2 (l1) (l2): prototerm ā prototerm ā prototerm ā
35 āØāØ āāq. q Ļµ t1 & l1āq = p
36 | āāq. q Ļµ t2 & l2āq = p.
40 'MHook t = (prototerm_node_1 label_m t).
43 "outer variable reference by depth (prototerm)"
44 'Hash k = (prototerm_node_0 (label_d k)).
47 "inner variable reference by depth (prototerm)"
48 'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
51 "name-free functional abstraction (prototerm)"
52 'Lamda t = (prototerm_node_1 label_L t).
55 "application (prototerm)"
56 'At u t = (prototerm_node_2 label_S label_A u t).
58 (* Basic constructions *******************************************************)
60 lemma in_comp_oref_hd (k):
61 (š±kāš) Ļµ ā§£k.
64 lemma in_comp_iref_hd (t) (q) (k):
65 q Ļµ t ā š±kāšŗāq Ļµ šk.t.
66 /2 width=3 by ex2_intro/ qed.
68 lemma in_comp_abst_hd (t) (q):
69 q Ļµ t ā šāq Ļµ š.t.
70 /2 width=3 by ex2_intro/ qed.
72 lemma in_comp_appl_sd (u) (t) (q):
73 q Ļµ u ā š¦āq Ļµ ļ¼ u.t.
74 /3 width=3 by ex2_intro, or_introl/ qed.
76 lemma in_comp_appl_hd (u) (t) (q):
77 q Ļµ t ā šāq Ļµ ļ¼ u.t.
78 /3 width=3 by ex2_intro, or_intror/ qed.
80 (* Basic inversions *********************************************************)
82 lemma in_comp_inv_iref (t) (p) (k):
84 āāq. š±kāšŗāq = p & q Ļµ t.
86 /2 width=3 by ex2_intro/
89 lemma in_comp_inv_abst (t) (p):
91 āāq. šāq = p & q Ļµ t.
93 /2 width=3 by ex2_intro/
96 lemma in_comp_inv_appl (u) (t) (p):
98 āØāØ āāq. š¦āq = p & q Ļµ u
99 | āāq. šāq = p & q Ļµ t.
100 #u #t #p * * #q #Hq #Hp
101 /3 width=3 by ex2_intro, or_introl, or_intror/
104 (* Advanced inversions ******************************************************)
106 lemma in_comp_inv_abst_hd (t) (p):
107 (šāp) Ļµ š.t ā p Ļµ t.
109 elim (in_comp_inv_abst ā¦ H0) -H0 #q #H0 #Hq
110 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
113 lemma in_comp_inv_appl_sd (u) (t) (p):
114 (š¦āp) Ļµ ļ¼ u.t ā p Ļµ u.
116 elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
117 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
120 lemma in_comp_inv_appl_hd (u) (t) (p):
121 (šāp) Ļµ ļ¼ u.t ā p Ļµ t.
123 elim (in_comp_inv_appl ā¦ H0) -H0 * #q #H0 #Hq
124 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //