|
1 theory Terms |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 text {* primrec seems to be genarally faster than fun *} |
|
8 |
|
9 section {*** lets with binding patterns ***} |
|
10 |
|
11 datatype trm1 = |
|
12 Vr1 "name" |
|
13 | Ap1 "trm1" "trm1" |
|
14 | Lm1 "name" "trm1" --"name is bound in trm1" |
|
15 | Lt1 "bp" "trm1" "trm1" --"all variables in bp are bound in the 2nd trm1" |
|
16 and bp = |
|
17 BUnit |
|
18 | BVr "name" |
|
19 | BPr "bp" "bp" |
|
20 |
|
21 (* to be given by the user *) |
|
22 primrec |
|
23 bv1 |
|
24 where |
|
25 "bv1 (BUnit) = {}" |
|
26 | "bv1 (BVr x) = {x}" |
|
27 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
|
28 |
|
29 (* needs to be calculated by the package *) |
|
30 primrec |
|
31 fv_trm1 and fv_bp |
|
32 where |
|
33 "fv_trm1 (Vr1 x) = {x}" |
|
34 | "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)" |
|
35 | "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}" |
|
36 | "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)" |
|
37 | "fv_bp (BUnit) = {}" |
|
38 | "fv_bp (BVr x) = {x}" |
|
39 | "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)" |
|
40 |
|
41 (* needs to be stated by the package *) |
|
42 instantiation |
|
43 trm1 :: pt |
|
44 bp :: pt |
|
45 begin |
|
46 |
|
47 primrec |
|
48 perm_trm1 and perm_bp |
|
49 where |
|
50 "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)" |
|
51 | "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
52 | "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)" |
|
53 | "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)" |
|
54 | "perm_bp pi (BUnit) = BUnit" |
|
55 | "perm_bp pi (BVr a) = BVr (pi \<bullet> a)" |
|
56 | "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)" |
|
57 |
|
58 end |
|
59 |
|
60 inductive |
|
61 alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
|
62 where |
|
63 a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)" |
|
64 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2" |
|
65 | a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> |
|
66 (fv_trm1 t - {a})\<sharp>* pi \<and> |
|
67 (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b) |
|
68 \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s" |
|
69 | a4: "\<exists>pi::name prm.( |
|
70 t1 \<approx>1 t2 \<and> |
|
71 (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and> |
|
72 (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and> |
|
73 (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *) |
|
74 ) \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2" |
|
75 |
|
76 lemma alpha1_equivp: "equivp alpha1" sorry |
|
77 |
|
78 quotient_type qtrm1 = trm1 / alpha1 |
|
79 by (rule alpha1_equivp) |
|
80 |
|
81 |
|
82 section {*** lets with single assignments ***} |
|
83 |
|
84 datatype trm2 = |
|
85 Vr2 "name" |
|
86 | Ap2 "trm2" "trm2" |
|
87 | Lm2 "name" "trm2" |
|
88 | Lt2 "assign" "trm2" |
|
89 and assign = |
|
90 As "name" "trm2" |
|
91 |
|
92 (* to be given by the user *) |
|
93 primrec |
|
94 bv2 |
|
95 where |
|
96 "bv2 (As x t) = {x}" |
|
97 |
|
98 (* needs to be calculated by the package *) |
|
99 primrec |
|
100 fv_trm2 and fv_assign |
|
101 where |
|
102 "fv_trm2 (Vr2 x) = {x}" |
|
103 | "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)" |
|
104 | "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}" |
|
105 | "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)" |
|
106 | "fv_assign (As x t) = (fv_trm2 t)" |
|
107 |
|
108 (* needs to be stated by the package *) |
|
109 overloading |
|
110 perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2" (unchecked) |
|
111 perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked) |
|
112 begin |
|
113 |
|
114 primrec |
|
115 perm_trm2 and perm_assign |
|
116 where |
|
117 "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)" |
|
118 | "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)" |
|
119 | "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)" |
|
120 | "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)" |
|
121 | "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)" |
|
122 |
|
123 end |
|
124 |
|
125 inductive |
|
126 alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
|
127 where |
|
128 a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)" |
|
129 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2" |
|
130 | a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> |
|
131 (fv_trm2 t - {a})\<sharp>* pi \<and> |
|
132 (pi \<bullet> t) \<approx>2 s \<and> |
|
133 (pi \<bullet> a) = b) |
|
134 \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s" |
|
135 | a4: "\<exists>pi::name prm. ( |
|
136 fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and> |
|
137 (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and> |
|
138 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
|
139 ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2" |
|
140 |
|
141 lemma alpha2_equivp: "equivp alpha2" sorry |
|
142 |
|
143 quotient_type qtrm2 = trm2 / alpha2 |
|
144 by (rule alpha2_equivp) |
|
145 |
|
146 section {*** lets with many assignments ***} |
|
147 |
|
148 datatype trm3 = |
|
149 Vr3 "name" |
|
150 | Ap3 "trm3" "trm3" |
|
151 | Lm3 "name" "trm3" |
|
152 | Lt3 "assigns" "trm3" |
|
153 and assigns = |
|
154 ANil |
|
155 | ACons "name" "trm3" "assigns" |
|
156 |
|
157 (* to be given by the user *) |
|
158 primrec |
|
159 bv3 |
|
160 where |
|
161 "bv3 ANil = {}" |
|
162 | "bv3 (ACons x t as) = {x} \<union> (bv3 as)" |
|
163 |
|
164 primrec |
|
165 fv_trm3 and fv_assigns |
|
166 where |
|
167 "fv_trm3 (Vr3 x) = {x}" |
|
168 | "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)" |
|
169 | "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}" |
|
170 | "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)" |
|
171 | "fv_assigns (ANil) = {}" |
|
172 | "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)" |
|
173 |
|
174 (* needs to be stated by the package *) |
|
175 overloading |
|
176 perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3" (unchecked) |
|
177 perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked) |
|
178 begin |
|
179 |
|
180 primrec |
|
181 perm_trm3 and perm_assigns |
|
182 where |
|
183 "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)" |
|
184 | "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)" |
|
185 | "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)" |
|
186 | "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)" |
|
187 | "perm_assigns pi (ANil) = ANil" |
|
188 | "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)" |
|
189 |
|
190 end |
|
191 |
|
192 inductive |
|
193 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
|
194 where |
|
195 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
|
196 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
|
197 | a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> |
|
198 (fv_trm3 t - {a})\<sharp>* pi \<and> |
|
199 (pi \<bullet> t) \<approx>3 s \<and> |
|
200 (pi \<bullet> a) = b) |
|
201 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
|
202 | a4: "\<exists>pi::name prm. ( |
|
203 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
|
204 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
|
205 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
|
206 ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2" |
|
207 |
|
208 lemma alpha3_equivp: "equivp alpha3" sorry |
|
209 |
|
210 quotient_type qtrm3 = trm3 / alpha3 |
|
211 by (rule alpha3_equivp) |
|
212 |
|
213 |
|
214 section {*** lam with indirect list recursion ***} |
|
215 |
|
216 datatype trm4 = |
|
217 Vr4 "name" |
|
218 | Ap4 "trm4" "trm4 list" |
|
219 | Lm4 "name" "trm4" |
|
220 |
|
221 thm trm4.recs |
|
222 |
|
223 primrec |
|
224 fv_trm4 and fv_trm4_list |
|
225 where |
|
226 "fv_trm4 (Vr4 x) = {x}" |
|
227 | "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
|
228 | "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {x}" |
|
229 | "fv_trm4_list ([]) = {}" |
|
230 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
|
231 |
|
232 |
|
233 (* needs to be stated by the package *) |
|
234 (* there cannot be a clause for lists, as *) |
|
235 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
236 overloading |
|
237 perm_trm4 \<equiv> "perm :: 'x prm \<Rightarrow> trm4 \<Rightarrow> trm4" (unchecked) |
|
238 begin |
|
239 |
|
240 primrec |
|
241 perm_trm4 |
|
242 where |
|
243 "perm_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
|
244 | "perm_trm4 pi (Ap4 t ts) = Ap4 (perm_trm4 pi t) (pi \<bullet> ts)" |
|
245 | "perm_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (perm_trm4 pi t)" |
|
246 |
|
247 end |
|
248 |
|
249 inductive |
|
250 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
|
251 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
|
252 where |
|
253 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
|
254 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
|
255 | a4: "\<exists>pi::name prm. (fv_trm4 t - {a} = fv_trm4 s - {b} \<and> |
|
256 (fv_trm4 t - {a})\<sharp>* pi \<and> |
|
257 (pi \<bullet> t) \<approx>4 s \<and> |
|
258 (pi \<bullet> a) = b) |
|
259 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
|
260 | a5: "[] \<approx>4list []" |
|
261 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
|
262 |
|
263 lemma alpha4_equivp: "equivp alpha4" sorry |
|
264 lemma alpha4list_equivp: "equivp alpha4list" sorry |
|
265 |
|
266 quotient_type |
|
267 qtrm4 = trm4 / alpha4 and |
|
268 qtrm4list = "trm4 list" / alpha4list |
|
269 by (simp_all add: alpha4_equivp alpha4list_equivp) |
|
270 |
|
271 end |