|
1 theory Test_compat |
|
2 imports "Parser" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 text {* |
|
6 example 1 |
|
7 |
|
8 single let binding |
|
9 *} |
|
10 |
|
11 nominal_datatype lam = |
|
12 VAR "name" |
|
13 | APP "lam" "lam" |
|
14 | LET bp::"bp" t::"lam" bind "bi bp" in t |
|
15 and bp = |
|
16 BP "name" "lam" |
|
17 binder |
|
18 bi::"bp \<Rightarrow> atom set" |
|
19 where |
|
20 "bi (BP x t) = {atom x}" |
|
21 |
|
22 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
|
23 |
|
24 abbreviation "VAR \<equiv> VAR_raw" |
|
25 abbreviation "APP \<equiv> APP_raw" |
|
26 abbreviation "LET \<equiv> LET_raw" |
|
27 abbreviation "BP \<equiv> BP_raw" |
|
28 abbreviation "bi \<equiv> bi_raw" |
|
29 |
|
30 (* non-recursive case *) |
|
31 |
|
32 inductive |
|
33 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
|
34 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
|
35 compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
|
36 where |
|
37 "x = y \<Longrightarrow> alpha_lam (VAR x) (VAR y)" |
|
38 | "alpha_lam l1 s1 \<and> alpha_lam l2 s2 \<Longrightarrow> alpha_lam (APP l1 l2) (APP s1 s2)" |
|
39 | "\<exists>pi. (bi bp, lam) \<approx>gen alpha_lam fv_lam_raw pi (bi bp', lam') \<and> compat_bp bp pi bp' |
|
40 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
|
41 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
|
42 | "alpha_lam t t' \<and> pi \<bullet> x = x' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" |
|
43 |
|
44 lemma test1: |
|
45 assumes "distinct [x, y]" |
|
46 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
47 (LET (BP y (VAR x)) (VAR y))" |
|
48 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
|
49 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
50 apply(simp add: alpha_gen fresh_star_def) |
|
51 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
|
52 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
|
53 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
|
54 done |
|
55 |
|
56 lemma test2: |
|
57 assumes asm: "distinct [x, y]" |
|
58 shows "\<not> alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
59 (LET (BP y (VAR y)) (VAR y))" |
|
60 using asm |
|
61 apply(clarify) |
|
62 apply(erule alpha_lam.cases) |
|
63 apply(simp_all) |
|
64 apply(erule exE) |
|
65 apply(clarify) |
|
66 apply(simp add: alpha_gen fresh_star_def) |
|
67 apply(erule alpha_lam.cases) |
|
68 apply(simp_all) |
|
69 apply(clarify) |
|
70 apply(erule compat_bp.cases) |
|
71 apply(simp_all) |
|
72 apply(clarify) |
|
73 apply(erule alpha_lam.cases) |
|
74 apply(simp_all) |
|
75 done |
|
76 |
|
77 (* recursive case where we have also bind "bi bp" in bp *) |
|
78 |
|
79 inductive |
|
80 Alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
|
81 Alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
|
82 Compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
|
83 where |
|
84 "x = y \<Longrightarrow> Alpha_lam (VAR x) (VAR y)" |
|
85 | "Alpha_lam l1 s1 \<and> Alpha_lam l2 s2 \<Longrightarrow> Alpha_lam (APP l1 l2) (APP s1 s2)" |
|
86 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
|
87 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
|
88 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
|
89 | "Alpha_lam (pi \<bullet> t) t' \<and> pi \<bullet> x = x' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
|
90 |
|
91 lemma Test1: |
|
92 assumes "distinct [x, y]" |
|
93 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
94 (LET (BP y (VAR y)) (VAR y))" |
|
95 apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) |
|
96 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
97 apply(simp add: alpha_gen fresh_star_def) |
|
98 apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) |
|
99 apply(rule Alpha_lam_Alpha_bp_Compat_bp.intros) |
|
100 apply(simp add: Alpha_lam_Alpha_bp_Compat_bp.intros(1)) |
|
101 done |
|
102 |
|
103 lemma Test2: |
|
104 assumes asm: "distinct [x, y]" |
|
105 shows "\<not> Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
|
106 (LET (BP y (VAR x)) (VAR y))" |
|
107 using asm |
|
108 apply(clarify) |
|
109 apply(erule Alpha_lam.cases) |
|
110 apply(simp_all) |
|
111 apply(erule exE) |
|
112 apply(clarify) |
|
113 apply(simp add: alpha_gen fresh_star_def) |
|
114 apply(erule Alpha_lam.cases) |
|
115 apply(simp_all) |
|
116 apply(clarify) |
|
117 apply(erule Compat_bp.cases) |
|
118 apply(simp_all) |
|
119 apply(clarify) |
|
120 apply(erule Alpha_lam.cases) |
|
121 apply(simp_all) |
|
122 done |
|
123 |
|
124 |
|
125 text {* example 2 *} |
|
126 |
|
127 nominal_datatype trm' = |
|
128 Var "name" |
|
129 | App "trm'" "trm'" |
|
130 | Lam x::"name" t::"trm'" bind x in t |
|
131 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
|
132 and pat' = |
|
133 PN |
|
134 | PS "name" |
|
135 | PD "name" "name" |
|
136 binder |
|
137 f::"pat' \<Rightarrow> atom set" |
|
138 where |
|
139 "f PN = {}" |
|
140 | "f (PS x) = {atom x}" |
|
141 | "f (PD x y) = {atom x} \<union> {atom y}" |
|
142 |
|
143 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
|
144 |
|
145 abbreviation "Var \<equiv> VAR_raw" |
|
146 abbreviation "App \<equiv> APP_raw" |
|
147 abbreviation "Lam \<equiv> Lam_raw" |
|
148 abbreviation "Lett \<equiv> Let_raw" |
|
149 abbreviation "PN \<equiv> PN_raw" |
|
150 abbreviation "PS \<equiv> PS_raw" |
|
151 abbreviation "PD \<equiv> PD_raw" |
|
152 abbreviation "f \<equiv> f_raw" |
|
153 |
|
154 (* not_yet_done |
|
155 name = namea \<Longrightarrow> alpha_trm'_raw (Var_raw name) (Var_raw namea) |
|
156 alpha_trm'_raw trm'_raw2 trm'_raw2a \<and> alpha_trm'_raw trm'_raw1 trm'_raw1a \<Longrightarrow> |
|
157 alpha_trm'_raw (App_raw trm'_raw1 trm'_raw2) (App_raw trm'_raw1a trm'_raw2a) |
|
158 \<exists>pi. ({atom name}, trm'_raw) \<approx>gen alpha_trm'_raw fv_trm'_raw pi ({atom namea}, trm'_rawa) \<Longrightarrow> |
|
159 alpha_trm'_raw (Lam_raw name trm'_raw) (Lam_raw namea trm'_rawa) |
|
160 \<exists>pi. (f_raw pat'_raw, |
|
161 trm'_raw2) \<approx>gen alpha_trm'_raw fv_trm'_raw pi (f_raw pat'_rawa, trm'_raw2a) \<and> |
|
162 alpha_trm'_raw trm'_raw1 trm'_raw1a \<and> |
|
163 (f_raw pat'_raw, |
|
164 pat'_raw) \<approx>gen alpha_pat'_raw fv_pat'_raw pi (f_raw pat'_rawa, pat'_rawa) \<Longrightarrow> |
|
165 alpha_trm'_raw (Let_raw pat'_raw trm'_raw1 trm'_raw2) (Let_raw pat'_rawa trm'_raw1a trm'_raw2a) |
|
166 True \<Longrightarrow> alpha_pat'_raw PN_raw PN_raw |
|
167 name = namea \<Longrightarrow> alpha_pat'_raw (PS_raw name) (PS_raw namea) |
|
168 name2 = name2a \<and> name1 = name1a \<Longrightarrow> alpha_pat'_raw (PD_raw name1 name2) (PD_raw name1a name2a) |
|
169 *) |
|
170 |
|
171 (* compat should be |
|
172 compat (PN) pi (PN) == True |
|
173 compat (PS x) pi (PS x') == pi o x = x' |
|
174 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
|
175 *) |
|
176 |
|
177 |
|
178 thm alpha_trm'_raw_alpha_pat'_raw.intros[no_vars] |
|
179 thm fv_trm'_raw_fv_pat'_raw.simps[no_vars] |
|
180 thm f_raw.simps |
|
181 (*thm trm'_pat'_induct |
|
182 thm trm'_pat'_perm |
|
183 thm trm'_pat'_fv |
|
184 thm trm'_pat'_bn |
|
185 thm trm'_pat'_inject*) |
|
186 |
|
187 nominal_datatype trm0 = |
|
188 Var0 "name" |
|
189 | App0 "trm0" "trm0" |
|
190 | Lam0 x::"name" t::"trm0" bind x in t |
|
191 | Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t |
|
192 and pat0 = |
|
193 PN0 |
|
194 | PS0 "name" |
|
195 | PD0 "pat0" "pat0" |
|
196 binder |
|
197 f0::"pat0 \<Rightarrow> atom set" |
|
198 where |
|
199 "f0 PN0 = {}" |
|
200 | "f0 (PS0 x) = {atom x}" |
|
201 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)" |
|
202 |
|
203 thm f0_raw.simps |
|
204 (*thm trm0_pat0_induct |
|
205 thm trm0_pat0_perm |
|
206 thm trm0_pat0_fv |
|
207 thm trm0_pat0_bn*) |
|
208 |
|
209 text {* example type schemes *} |
|
210 |
|
211 (* does not work yet |
|
212 nominal_datatype t = |
|
213 Var "name" |
|
214 | Fun "t" "t" |
|
215 |
|
216 nominal_datatype tyS = |
|
217 All xs::"name list" ty::"t_raw" bind xs in ty |
|
218 *) |
|
219 |
|
220 |
|
221 nominal_datatype t = |
|
222 Var "name" |
|
223 | Fun "t" "t" |
|
224 and tyS = |
|
225 All xs::"name set" ty::"t" bind xs in ty |
|
226 |
|
227 (* example 1 from Terms.thy *) |
|
228 |
|
229 nominal_datatype trm1 = |
|
230 Vr1 "name" |
|
231 | Ap1 "trm1" "trm1" |
|
232 | Lm1 x::"name" t::"trm1" bind x in t |
|
233 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t |
|
234 and bp1 = |
|
235 BUnit1 |
|
236 | BV1 "name" |
|
237 | BP1 "bp1" "bp1" |
|
238 binder |
|
239 bv1 |
|
240 where |
|
241 "bv1 (BUnit1) = {}" |
|
242 | "bv1 (BV1 x) = {atom x}" |
|
243 | "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
|
244 |
|
245 thm bv1_raw.simps |
|
246 |
|
247 (* example 2 from Terms.thy *) |
|
248 |
|
249 nominal_datatype trm2 = |
|
250 Vr2 "name" |
|
251 | Ap2 "trm2" "trm2" |
|
252 | Lm2 x::"name" t::"trm2" bind x in t |
|
253 | Lt2 r::"assign" t::"trm2" bind "bv2 r" in t |
|
254 and assign = |
|
255 As "name" "trm2" |
|
256 binder |
|
257 bv2 |
|
258 where |
|
259 "bv2 (As x t) = {atom x}" |
|
260 |
|
261 (* compat should be |
|
262 compat (As x t) pi (As x' t') == pi o x = x' & alpha t t' |
|
263 *) |
|
264 |
|
265 |
|
266 thm fv_trm2_raw_fv_assign_raw.simps[no_vars] |
|
267 thm alpha_trm2_raw_alpha_assign_raw.intros[no_vars] |
|
268 |
|
269 |
|
270 |
|
271 text {* example 3 from Terms.thy *} |
|
272 |
|
273 nominal_datatype trm3 = |
|
274 Vr3 "name" |
|
275 | Ap3 "trm3" "trm3" |
|
276 | Lm3 x::"name" t::"trm3" bind x in t |
|
277 | Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t |
|
278 and rassigns3 = |
|
279 ANil |
|
280 | ACons "name" "trm3" "rassigns3" |
|
281 binder |
|
282 bv3 |
|
283 where |
|
284 "bv3 ANil = {}" |
|
285 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
|
286 |
|
287 |
|
288 (* compat should be |
|
289 compat (ANil) pi (PNil) \<equiv> TRue |
|
290 compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
|
291 *) |
|
292 |
|
293 (* example 4 from Terms.thy *) |
|
294 |
|
295 (* fv_eqvt does not work, we need to repaire defined permute functions |
|
296 defined fv and defined alpha... *) |
|
297 nominal_datatype trm4 = |
|
298 Vr4 "name" |
|
299 | Ap4 "trm4" "trm4 list" |
|
300 | Lm4 x::"name" t::"trm4" bind x in t |
|
301 |
|
302 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
|
303 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
|
304 |
|
305 (* example 5 from Terms.thy *) |
|
306 |
|
307 nominal_datatype trm5 = |
|
308 Vr5 "name" |
|
309 | Ap5 "trm5" "trm5" |
|
310 | Lt5 l::"lts" t::"trm5" bind "bv5 l" in t |
|
311 and lts = |
|
312 Lnil |
|
313 | Lcons "name" "trm5" "lts" |
|
314 binder |
|
315 bv5 |
|
316 where |
|
317 "bv5 Lnil = {}" |
|
318 | "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
319 |
|
320 (* example 6 from Terms.thy *) |
|
321 |
|
322 (* BV is not respectful, needs to fail*) |
|
323 nominal_datatype trm6 = |
|
324 Vr6 "name" |
|
325 | Lm6 x::"name" t::"trm6" bind x in t |
|
326 | Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right |
|
327 binder |
|
328 bv6 |
|
329 where |
|
330 "bv6 (Vr6 n) = {}" |
|
331 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t" |
|
332 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" |
|
333 (* example 7 from Terms.thy *) |
|
334 |
|
335 (* BV is not respectful, needs to fail*) |
|
336 nominal_datatype trm7 = |
|
337 Vr7 "name" |
|
338 | Lm7 l::"name" r::"trm7" bind l in r |
|
339 | Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r |
|
340 binder |
|
341 bv7 |
|
342 where |
|
343 "bv7 (Vr7 n) = {atom n}" |
|
344 | "bv7 (Lm7 n t) = bv7 t - {atom n}" |
|
345 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" |
|
346 |
|
347 (* example 8 from Terms.thy *) |
|
348 |
|
349 nominal_datatype foo8 = |
|
350 Foo0 "name" |
|
351 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" |
|
352 and bar8 = |
|
353 Bar0 "name" |
|
354 | Bar1 "name" s::"name" b::"bar8" bind s in b |
|
355 binder |
|
356 bv8 |
|
357 where |
|
358 "bv8 (Bar0 x) = {}" |
|
359 | "bv8 (Bar1 v x b) = {atom v}" |
|
360 |
|
361 (* example 9 from Terms.thy *) |
|
362 |
|
363 (* BV is not respectful, needs to fail*) |
|
364 nominal_datatype lam9 = |
|
365 Var9 "name" |
|
366 | Lam9 n::"name" l::"lam9" bind n in l |
|
367 and bla9 = |
|
368 Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s |
|
369 binder |
|
370 bv9 |
|
371 where |
|
372 "bv9 (Var9 x) = {}" |
|
373 | "bv9 (Lam9 x b) = {atom x}" |
|
374 |
|
375 (* example from my PHD *) |
|
376 |
|
377 atom_decl coname |
|
378 |
|
379 nominal_datatype phd = |
|
380 Ax "name" "coname" |
|
381 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
382 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
383 | AndL1 n::"name" t::"phd" "name" bind n in t |
|
384 | AndL2 n::"name" t::"phd" "name" bind n in t |
|
385 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
|
386 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
387 |
|
388 thm alpha_phd_raw.intros[no_vars] |
|
389 thm fv_phd_raw.simps[no_vars] |
|
390 |
|
391 |
|
392 (* example form Leroy 96 about modules; OTT *) |
|
393 |
|
394 nominal_datatype mexp = |
|
395 Acc "path" |
|
396 | Stru "body" |
|
397 | Funct x::"name" "sexp" m::"mexp" bind x in m |
|
398 | FApp "mexp" "path" |
|
399 | Ascr "mexp" "sexp" |
|
400 and body = |
|
401 Empty |
|
402 | Seq c::defn d::"body" bind "cbinders c" in d |
|
403 and defn = |
|
404 Type "name" "tyty" |
|
405 | Dty "name" |
|
406 | DStru "name" "mexp" |
|
407 | Val "name" "trmtrm" |
|
408 and sexp = |
|
409 Sig sbody |
|
410 | SFunc "name" "sexp" "sexp" |
|
411 and sbody = |
|
412 SEmpty |
|
413 | SSeq C::spec D::sbody bind "Cbinders C" in D |
|
414 and spec = |
|
415 Type1 "name" |
|
416 | Type2 "name" "tyty" |
|
417 | SStru "name" "sexp" |
|
418 | SVal "name" "tyty" |
|
419 and tyty = |
|
420 Tyref1 "name" |
|
421 | Tyref2 "path" "tyty" |
|
422 | Fun "tyty" "tyty" |
|
423 and path = |
|
424 Sref1 "name" |
|
425 | Sref2 "path" "name" |
|
426 and trmtrm = |
|
427 Tref1 "name" |
|
428 | Tref2 "path" "name" |
|
429 | Lam' v::"name" "tyty" M::"trmtrm" bind v in M |
|
430 | App' "trmtrm" "trmtrm" |
|
431 | Let' "body" "trmtrm" |
|
432 binder |
|
433 cbinders :: "defn \<Rightarrow> atom set" |
|
434 and Cbinders :: "spec \<Rightarrow> atom set" |
|
435 where |
|
436 "cbinders (Type t T) = {atom t}" |
|
437 | "cbinders (Dty t) = {atom t}" |
|
438 | "cbinders (DStru x s) = {atom x}" |
|
439 | "cbinders (Val v M) = {atom v}" |
|
440 | "Cbinders (Type1 t) = {atom t}" |
|
441 | "Cbinders (Type2 t T) = {atom t}" |
|
442 | "Cbinders (SStru x S) = {atom x}" |
|
443 | "Cbinders (SVal v T) = {atom v}" |
|
444 |
|
445 (* core haskell *) |
|
446 print_theorems |
|
447 |
|
448 atom_decl var |
|
449 atom_decl tvar |
|
450 |
|
451 |
|
452 (* there are types, coercion types and regular types *) |
|
453 nominal_datatype tkind = |
|
454 KStar |
|
455 | KFun "tkind" "tkind" |
|
456 and ckind = |
|
457 CKEq "ty" "ty" |
|
458 and ty = |
|
459 TVar "tvar" |
|
460 | TC "string" |
|
461 | TApp "ty" "ty" |
|
462 | TFun "string" "ty list" |
|
463 | TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
|
464 | TEq "ty" "ty" "ty" |
|
465 and co = |
|
466 CC "string" |
|
467 | CApp "co" "co" |
|
468 | CFun "string" "co list" |
|
469 | CAll tv::"tvar" "ckind" C::"co" bind tv in C |
|
470 | CEq "co" "co" "co" |
|
471 | CSym "co" |
|
472 | CCir "co" "co" |
|
473 | CLeft "co" |
|
474 | CRight "co" |
|
475 | CSim "co" |
|
476 | CRightc "co" |
|
477 | CLeftc "co" |
|
478 | CCoe "co" "co" |
|
479 |
|
480 |
|
481 typedecl ty --"hack since ty is not yet defined" |
|
482 |
|
483 abbreviation |
|
484 "atoms A \<equiv> atom ` A" |
|
485 |
|
486 nominal_datatype trm = |
|
487 Var "var" |
|
488 | C "string" |
|
489 | LAM tv::"tvar" "kind" t::"trm" bind tv in t |
|
490 | APP "trm" "ty" |
|
491 | Lam v::"var" "ty" t::"trm" bind v in t |
|
492 | App "trm" "trm" |
|
493 | Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
494 | Case "trm" "assoc list" |
|
495 | Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
496 and assoc = |
|
497 A p::"pat" t::"trm" bind "bv p" in t |
|
498 and pat = |
|
499 K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
|
500 binder |
|
501 bv :: "pat \<Rightarrow> atom set" |
|
502 where |
|
503 "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
|
504 |
|
505 (* |
|
506 compat (K s ts vs) pi (K s' ts' vs') == |
|
507 s = s' & |
|
508 |
|
509 *) |
|
510 |
|
511 |
|
512 (*thm bv_raw.simps*) |
|
513 |
|
514 (* example 3 from Peter Sewell's bestiary *) |
|
515 nominal_datatype exp = |
|
516 VarP "name" |
|
517 | AppP "exp" "exp" |
|
518 | LamP x::"name" e::"exp" bind x in e |
|
519 | LetP x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
|
520 and pat = |
|
521 PVar "name" |
|
522 | PUnit |
|
523 | PPair "pat" "pat" |
|
524 binder |
|
525 bp :: "pat \<Rightarrow> atom set" |
|
526 where |
|
527 "bp (PVar x) = {atom x}" |
|
528 | "bp (PUnit) = {}" |
|
529 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
|
530 thm alpha_exp_raw_alpha_pat_raw.intros |
|
531 |
|
532 (* example 6 from Peter Sewell's bestiary *) |
|
533 nominal_datatype exp6 = |
|
534 EVar name |
|
535 | EPair exp6 exp6 |
|
536 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
|
537 and pat6 = |
|
538 PVar' name |
|
539 | PUnit' |
|
540 | PPair' pat6 pat6 |
|
541 binder |
|
542 bp6 :: "pat6 \<Rightarrow> atom set" |
|
543 where |
|
544 "bp6 (PVar' x) = {atom x}" |
|
545 | "bp6 (PUnit') = {}" |
|
546 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
|
547 thm alpha_exp6_raw_alpha_pat6_raw.intros |
|
548 |
|
549 (* example 7 from Peter Sewell's bestiary *) |
|
550 nominal_datatype exp7 = |
|
551 EVar name |
|
552 | EUnit |
|
553 | EPair exp7 exp7 |
|
554 | ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l |
|
555 and lrb = |
|
556 Assign name exp7 |
|
557 and lrbs = |
|
558 Single lrb |
|
559 | More lrb lrbs |
|
560 binder |
|
561 b7 :: "lrb \<Rightarrow> atom set" and |
|
562 b7s :: "lrbs \<Rightarrow> atom set" |
|
563 where |
|
564 "b7 (Assign x e) = {atom x}" |
|
565 | "b7s (Single a) = b7 a" |
|
566 | "b7s (More a as) = (b7 a) \<union> (b7s as)" |
|
567 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros |
|
568 |
|
569 (* example 8 from Peter Sewell's bestiary *) |
|
570 nominal_datatype exp8 = |
|
571 EVar name |
|
572 | EUnit |
|
573 | EPair exp8 exp8 |
|
574 | ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l |
|
575 and fnclause = |
|
576 K x::name p::pat8 e::exp8 bind "b_pat p" in e |
|
577 and fnclauses = |
|
578 S fnclause |
|
579 | ORs fnclause fnclauses |
|
580 and lrb8 = |
|
581 Clause fnclauses |
|
582 and lrbs8 = |
|
583 Single lrb8 |
|
584 | More lrb8 lrbs8 |
|
585 and pat8 = |
|
586 PVar name |
|
587 | PUnit |
|
588 | PPair pat8 pat8 |
|
589 binder |
|
590 b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and |
|
591 b_pat :: "pat8 \<Rightarrow> atom set" and |
|
592 b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
|
593 b_fnclause :: "fnclause \<Rightarrow> atom set" and |
|
594 b_lrb8 :: "lrb8 \<Rightarrow> atom set" |
|
595 where |
|
596 "b_lrbs8 (Single l) = b_lrb8 l" |
|
597 | "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls" |
|
598 | "b_pat (PVar x) = {atom x}" |
|
599 | "b_pat (PUnit) = {}" |
|
600 | "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2" |
|
601 | "b_fnclauses (S fc) = (b_fnclause fc)" |
|
602 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
|
603 | "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" |
|
604 | "b_fnclause (K x pat exp8) = {atom x}" |
|
605 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros |
|
606 |
|
607 |
|
608 |
|
609 |
|
610 (* example 9 from Peter Sewell's bestiary *) |
|
611 (* run out of steam at the moment *) |
|
612 |
|
613 end |
|
614 |
|
615 |
|
616 |