29 | "bv1 (BVr x) = {atom x}" |
29 | "bv1 (BVr x) = {atom x}" |
30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
31 |
31 |
32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
32 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
33 |
33 |
34 ML {* |
|
35 val elims_ref = ref (@{thms refl}) |
|
36 val intrs_ref = ref (@{thms refl}) |
|
37 *} |
|
38 ML elims_ref |
|
39 local_setup {* |
34 local_setup {* |
40 fn ctxt => |
35 snd o define_fv_alpha "Terms.rtrm1" |
41 let val ((fv, ind), ctxt') = |
|
42 define_fv_alpha "Terms.rtrm1" |
|
43 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
36 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
44 [[], [[]], [[], []]]] ctxt; |
37 [[], [[]], [[], []]]] *} |
45 val elims' = ProofContext.export ctxt' ctxt (#elims ind) |
|
46 val intrs' = ProofContext.export ctxt' ctxt (#intrs ind) |
|
47 val _ = (elims_ref := elims'); |
|
48 val _ = (intrs_ref := intrs'); |
|
49 in ctxt' end *} |
|
50 print_theorems |
38 print_theorems |
51 |
39 |
52 notation |
40 notation |
53 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
41 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
54 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
42 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
55 thm alpha_rtrm1_alpha_bp.intros |
43 thm alpha_rtrm1_alpha_bp.intros |
56 |
44 |
57 prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *} |
45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
58 apply - |
46 thm alpha1_inj |
59 prefer 4 |
|
60 apply (rule iffI) |
|
61 apply (tactic {* eresolve_tac (!elims_ref) 1 *}) |
|
62 apply (simp only: rtrm1.distinct) |
|
63 apply (simp only: rtrm1.distinct) |
|
64 apply (simp only: rtrm1.distinct) |
|
65 apply (rule conjI) apply (simp only: rtrm1.inject) |
|
66 apply (rule conjI) apply (simp only: rtrm1.inject) |
|
67 apply (simp only: rtrm1.inject) |
|
68 apply (simp only: alpha_rtrm1_alpha_bp.intros) |
|
69 sorry |
|
70 |
|
71 lemma alpha1_inj: |
|
72 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
|
73 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
|
74 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" |
|
75 "(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) = |
|
76 ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and> |
|
77 (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))" |
|
78 "alpha_bp BUnit BUnit" |
|
79 "(alpha_bp (BVr name) (BVr namea)) = (name = namea)" |
|
80 "(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)" |
|
81 apply - |
|
82 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
83 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
84 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
85 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
86 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
87 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
|
88 done |
|
89 |
47 |
90 lemma alpha_bp_refl: "alpha_bp a a" |
48 lemma alpha_bp_refl: "alpha_bp a a" |
91 apply induct |
49 apply induct |
92 apply (simp_all add: alpha1_inj) |
50 apply (simp_all add: alpha1_inj) |
93 done |
51 done |
342 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
300 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
343 |
301 |
344 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
302 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
345 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
303 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
346 [[[], []]]] *} |
304 [[[], []]]] *} |
347 print_theorems |
|
348 |
305 |
349 notation |
306 notation |
350 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
307 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
351 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
308 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
352 thm alpha_rtrm2_alpha_rassign.intros |
309 thm alpha_rtrm2_alpha_rassign.intros |
|
310 |
|
311 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *} |
|
312 thm alpha2_inj |
|
313 |
353 |
314 |
354 lemma alpha2_equivp: |
315 lemma alpha2_equivp: |
355 "equivp alpha_rtrm2" |
316 "equivp alpha_rtrm2" |
356 "equivp alpha_rassign" |
317 "equivp alpha_rassign" |
357 sorry |
318 sorry |
490 notation |
451 notation |
491 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
452 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
492 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
453 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
493 thm alpha_rtrm5_alpha_rlts.intros |
454 thm alpha_rtrm5_alpha_rlts.intros |
494 |
455 |
495 lemma alpha5_inj: |
456 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
496 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
457 thm alpha5_inj |
497 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
|
498 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and> |
|
499 (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))" |
|
500 "rLnil \<approx>l rLnil" |
|
501 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)" |
|
502 apply - |
|
503 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
|
504 apply rule |
|
505 apply (erule alpha_rtrm5.cases) |
|
506 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
|
507 apply rule |
|
508 apply (erule alpha_rtrm5.cases) |
|
509 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
|
510 apply rule |
|
511 apply (erule alpha_rtrm5.cases) |
|
512 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
|
513 apply rule |
|
514 apply (erule alpha_rlts.cases) |
|
515 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
|
516 done |
|
517 |
458 |
518 lemma alpha5_equivps: |
459 lemma alpha5_equivps: |
519 shows "equivp alpha_rtrm5" |
460 shows "equivp alpha_rtrm5" |
520 and "equivp alpha_rlts" |
461 and "equivp alpha_rlts" |
521 sorry |
462 sorry |
558 apply (simp_all add: alpha5_inj) |
499 apply (simp_all add: alpha5_inj) |
559 apply (erule exE)+ |
500 apply (erule exE)+ |
560 apply(unfold alpha_gen) |
501 apply(unfold alpha_gen) |
561 apply (erule conjE)+ |
502 apply (erule conjE)+ |
562 apply (rule conjI) |
503 apply (rule conjI) |
|
504 apply (rule_tac x="x \<bullet> pi" in exI) |
|
505 apply (rule conjI) |
|
506 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
507 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
508 apply(rule conjI) |
|
509 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
510 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
511 apply (subst permute_eqvt[symmetric]) |
|
512 apply (simp) |
563 apply (rule_tac x="x \<bullet> pia" in exI) |
513 apply (rule_tac x="x \<bullet> pia" in exI) |
564 apply (rule conjI) |
514 apply (rule conjI) |
565 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
515 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
566 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
516 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
567 apply(rule conjI) |
517 apply(rule conjI) |
568 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
518 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
569 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
519 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
570 apply (subst permute_eqvt[symmetric]) |
|
571 apply (simp) |
|
572 apply (rule_tac x="x \<bullet> pi" in exI) |
|
573 apply (rule conjI) |
|
574 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
575 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
576 apply(rule conjI) |
|
577 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
578 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
579 apply (subst permute_eqvt[symmetric]) |
520 apply (subst permute_eqvt[symmetric]) |
580 apply (simp) |
521 apply (simp) |
581 done |
522 done |
582 |
523 |
583 lemma alpha5_rfv: |
524 lemma alpha5_rfv: |
676 lemma lets_ok2: |
617 lemma lets_ok2: |
677 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
618 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
678 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
619 (Lt5 (Lcons y (Vr5 y) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
679 apply (subst alpha5_INJ) |
620 apply (subst alpha5_INJ) |
680 apply (rule conjI) |
621 apply (rule conjI) |
681 apply (rule_tac x="0 :: perm" in exI) |
622 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
682 apply (simp only: alpha_gen) |
623 apply (simp only: alpha_gen) |
683 apply (simp add: permute_trm5_lts fresh_star_def) |
624 apply (simp add: permute_trm5_lts fresh_star_def) |
684 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
625 apply (rule_tac x="0 :: perm" in exI) |
685 apply (simp only: alpha_gen) |
626 apply (simp only: alpha_gen) |
686 apply (simp add: permute_trm5_lts fresh_star_def) |
627 apply (simp add: permute_trm5_lts fresh_star_def) |
687 done |
628 done |
688 |
629 |
689 |
630 |