27 | "bv1 (BVr x) = {atom x}" |
29 | "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
30 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
29 |
31 |
30 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"] *} |
31 |
33 |
32 local_setup {* snd o define_fv_alpha "Terms.rtrm1" |
34 ML {* |
|
35 val elims_ref = ref (@{thms refl}) |
|
36 val intrs_ref = ref (@{thms refl}) |
|
37 *} |
|
38 ML elims_ref |
|
39 local_setup {* |
|
40 fn ctxt => |
|
41 let val ((fv, ind), ctxt') = |
|
42 define_fv_alpha "Terms.rtrm1" |
33 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
43 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
34 [[], [[]], [[], []]]] *} |
44 [[], [[]], [[], []]]] ctxt; |
35 print_theorems |
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 |
|
51 |
36 notation |
52 notation |
37 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
53 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
38 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
54 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
39 thm alpha_rtrm1_alpha_bp.intros |
55 thm alpha_rtrm1_alpha_bp.intros |
40 |
56 |
41 prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *} |
57 prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *} |
|
58 apply - |
|
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) |
42 sorry |
69 sorry |
43 |
70 |
44 lemma alpha1_inj: |
71 lemma alpha1_inj: |
45 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
72 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
46 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
73 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
854 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
881 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
855 print_theorems |
882 print_theorems |
856 |
883 |
857 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
884 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
858 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
885 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
|
886 print_theorems |
859 notation |
887 notation |
860 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
888 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
861 (* HERE THE RULES DIFFER *) |
889 (* HERE THE RULES DIFFER *) |
862 thm alpha_rtrm7.intros |
890 thm alpha_rtrm7.intros |
863 |
891 thm fv_rtrm7.simps |
864 inductive |
892 inductive |
865 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
893 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
866 where |
894 where |
867 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
895 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
868 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
896 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |