3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 declare [[STEPS = 21]] |
6 declare [[STEPS = 21]] |
7 |
7 |
8 class s1 |
8 nominal_datatype lam = |
9 class s2 |
|
10 |
|
11 nominal_datatype lambda: |
|
12 ('a, 'b) lam = |
|
13 Var "name" |
9 Var "name" |
14 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" |
10 | App "lam" "lam" |
15 | Lam x::"name" l::"('a, 'b) lam" bind x in l |
11 | Lam x::"name" l::"lam" bind x in l |
16 |
12 |
17 thm distinct |
13 thm lam.distinct |
18 thm induct |
14 thm lam.induct |
19 thm exhaust |
15 thm lam.exhaust |
20 thm fv_defs |
16 thm lam.fv_defs |
21 thm bn_defs |
17 thm lam.bn_defs |
22 thm perm_simps |
18 thm lam.perm_simps |
23 thm eq_iff |
19 thm lam.eq_iff |
24 thm fv_bn_eqvt |
20 thm lam.fv_bn_eqvt |
25 thm size_eqvt |
21 thm lam.size_eqvt |
26 |
22 |
27 |
|
28 thm lam.fv |
|
29 thm lam.supp |
|
30 lemmas supp_fn' = lam.fv[simplified lam.supp] |
|
31 |
|
32 declare lam.perm[eqvt] |
|
33 |
23 |
34 |
24 |
35 section {* Strong Induction Principles*} |
25 section {* Strong Induction Principles*} |
36 |
26 |
37 (* |
27 (* |
38 Old way of establishing strong induction |
28 Old way of establishing strong induction |
39 principles by chosing a fresh name. |
29 principles by chosing a fresh name. |
40 *) |
30 *) |
|
31 (* |
41 lemma |
32 lemma |
42 fixes c::"'a::fs" |
33 fixes c::"'a::fs" |
43 assumes a1: "\<And>name c. P c (Var name)" |
34 assumes a1: "\<And>name c. P c (Var name)" |
44 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
35 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
45 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
36 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
77 apply(simp) |
68 apply(simp) |
78 done |
69 done |
79 then have "P c (0 \<bullet> lam)" by blast |
70 then have "P c (0 \<bullet> lam)" by blast |
80 then show "P c lam" by simp |
71 then show "P c lam" by simp |
81 qed |
72 qed |
82 |
73 *) |
83 (* |
74 (* |
84 New way of establishing strong induction |
75 New way of establishing strong induction |
85 principles by using a appropriate permutation. |
76 principles by using a appropriate permutation. |
86 *) |
77 *) |
|
78 (* |
87 lemma |
79 lemma |
88 fixes c::"'a::fs" |
80 fixes c::"'a::fs" |
89 assumes a1: "\<And>name c. P c (Var name)" |
81 assumes a1: "\<And>name c. P c (Var name)" |
90 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
82 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
91 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
83 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
235 apply(simp add: finite_supp) |
229 apply(simp add: finite_supp) |
236 apply(simp add: finite_supp) |
230 apply(simp add: finite_supp) |
237 apply(simp add: finite_supp) |
231 apply(simp add: finite_supp) |
238 apply(rule_tac p="-p" in permute_boolE) |
232 apply(rule_tac p="-p" in permute_boolE) |
239 apply(perm_strict_simp add: permute_minus_cancel) |
233 apply(perm_strict_simp add: permute_minus_cancel) |
240 (* supplied by the user *) |
234 --"supplied by the user" |
241 apply(simp add: fresh_star_prod) |
235 apply(simp add: fresh_star_prod) |
242 apply(simp add: fresh_star_def) |
236 apply(simp add: fresh_star_def) |
243 sorry |
237 sorry |
244 qed |
238 qed |
245 then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" . |
239 then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" . |
246 then show "P c \<Gamma> t T" by simp |
240 then show "P c \<Gamma> t T" by simp |
247 qed |
241 qed |
248 |
242 |
249 |
243 *) |
250 |
244 |
251 |
|
252 |
|
253 |
|
254 |
|
255 inductive |
|
256 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
|
257 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
|
258 where |
|
259 aa: "tt r a a" |
|
260 | bb: "tt r a b ==> tt r a c" |
|
261 |
|
262 (* PROBLEM: derived eqvt-theorem does not conform with [eqvt] |
|
263 equivariance tt |
|
264 *) |
|
265 |
|
266 |
|
267 inductive |
|
268 alpha_lam_raw' |
|
269 where |
|
270 a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)" |
|
271 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow> |
|
272 alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)" |
|
273 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow> |
|
274 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
|
275 |
|
276 equivariance alpha_lam_raw' |
|
277 |
|
278 thm eqvts_raw |
|
279 |
|
280 section {* size function *} |
|
281 |
|
282 lemma size_eqvt_raw: |
|
283 fixes t::"lam_raw" |
|
284 shows "size (pi \<bullet> t) = size t" |
|
285 apply (induct rule: lam_raw.inducts) |
|
286 apply simp_all |
|
287 done |
|
288 |
|
289 instantiation lam :: size |
|
290 begin |
|
291 |
|
292 quotient_definition |
|
293 "size_lam :: lam \<Rightarrow> nat" |
|
294 is |
|
295 "size :: lam_raw \<Rightarrow> nat" |
|
296 |
|
297 lemma size_rsp: |
|
298 "alpha_lam_raw x y \<Longrightarrow> size x = size y" |
|
299 apply (induct rule: alpha_lam_raw.inducts) |
|
300 apply (simp_all only: lam_raw.size) |
|
301 apply (simp_all only: alphas) |
|
302 apply clarify |
|
303 apply (simp_all only: size_eqvt_raw) |
|
304 done |
|
305 |
|
306 lemma [quot_respect]: |
|
307 "(alpha_lam_raw ===> op =) size size" |
|
308 by (simp_all add: size_rsp) |
|
309 |
|
310 lemma [quot_preserve]: |
|
311 "(rep_lam ---> id) size = size" |
|
312 by (simp_all add: size_lam_def) |
|
313 |
|
314 instance |
|
315 by default |
|
316 |
|
317 end |
|
318 |
|
319 lemmas size_lam[simp] = |
|
320 lam_raw.size(4)[quot_lifted] |
|
321 lam_raw.size(5)[quot_lifted] |
|
322 lam_raw.size(6)[quot_lifted] |
|
323 |
|
324 (* is this needed? *) |
|
325 lemma [measure_function]: |
|
326 "is_measure (size::lam\<Rightarrow>nat)" |
|
327 by (rule is_measure_trivial) |
|
328 |
245 |
329 section {* Matching *} |
246 section {* Matching *} |
330 |
247 |
331 definition |
248 definition |
332 MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
249 MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
510 primrec match_App_raw where |
427 primrec match_App_raw where |
511 "match_App_raw (Var_raw x) = None" |
428 "match_App_raw (Var_raw x) = None" |
512 | "match_App_raw (App_raw x y) = Some (x, y)" |
429 | "match_App_raw (App_raw x y) = Some (x, y)" |
513 | "match_App_raw (Lam_raw n t) = None" |
430 | "match_App_raw (Lam_raw n t) = None" |
514 |
431 |
|
432 (* |
515 quotient_definition |
433 quotient_definition |
516 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
434 "match_App :: lam \<Rightarrow> (lam \<times> lam) option" |
517 is match_App_raw |
435 is match_App_raw |
518 |
436 |
519 lemma [quot_respect]: |
437 lemma [quot_respect]: |
545 "z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)" |
463 "z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)" |
546 apply (simp_all add: match_Lam_def) |
464 apply (simp_all add: match_Lam_def) |
547 apply (simp add: lam_half_inj) |
465 apply (simp add: lam_half_inj) |
548 apply auto |
466 apply auto |
549 done |
467 done |
550 |
468 *) |
551 (* |
469 (* |
552 lemma match_Lam_simps2: |
470 lemma match_Lam_simps2: |
553 "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)" |
471 "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)" |
554 apply (rule_tac t="Lam n s" |
472 apply (rule_tac t="Lam n s" |
555 and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst) |
473 and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst) |
625 qed |
543 qed |
626 qed |
544 qed |
627 |
545 |
628 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
546 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted] |
629 *) |
547 *) |
630 |
548 (* |
631 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
549 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b" |
632 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
550 by (induct x rule: lam.induct) (simp_all add: match_App_simps) |
633 |
551 |
634 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
552 lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S" |
635 apply (induct x rule: lam.induct) |
553 apply (induct x rule: lam.induct) |