23 primrec |
23 primrec |
24 bv1 |
24 bv1 |
25 where |
25 where |
26 "bv1 (BUnit) = {}" |
26 "bv1 (BUnit) = {}" |
27 | "bv1 (BVr x) = {atom x}" |
27 | "bv1 (BVr x) = {atom x}" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)" |
28 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)" |
29 |
29 |
30 local_setup {* define_raw_fv "Terms.rtrm1" |
30 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
31 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
31 |
|
32 local_setup {* snd o define_fv_alpha "Terms.rtrm1" |
|
33 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]], |
32 [[], [[]], [[], []]]] *} |
34 [[], [[]], [[], []]]] *} |
33 print_theorems |
35 print_theorems |
34 |
36 notation |
35 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *} |
37 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
36 |
38 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
37 inductive |
39 thm alpha_rtrm1_alpha_bp.intros |
38 alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100) |
|
39 where |
|
40 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)" |
|
41 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2" |
|
42 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s" |
|
43 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2" |
|
44 |
40 |
45 lemma alpha1_inj: |
41 lemma alpha1_inj: |
46 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
42 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
47 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
43 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
48 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))" |
44 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha_rtrm1 fv_rtrm1 pi ({atom ab}, s)))" |
49 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))" |
45 "(rLt1 bp rtrm11 rtrm12 \<approx>1 rLt1 bpa rtrm11a rtrm12a) = |
|
46 ((\<exists>pi. (bv1 bp, bp) \<approx>gen alpha_bp fv_bp pi (bv1 bpa, bpa)) \<and> rtrm11 \<approx>1 rtrm11a \<and> |
|
47 (\<exists>pi. (bv1 bp, rtrm12) \<approx>gen alpha_rtrm1 fv_rtrm1 pi (bv1 bpa, rtrm12a)))" |
|
48 "alpha_bp BUnit BUnit" |
|
49 "(alpha_bp (BVr name) (BVr namea)) = (name = namea)" |
|
50 "(alpha_bp (BPr bp1 bp2) (BPr bp1a bp2a)) = (alpha_bp bp1 bp1a \<and> alpha_bp bp2 bp2a)" |
50 apply - |
51 apply - |
51 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
52 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
52 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
53 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
53 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
54 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
54 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros) |
55 apply rule apply (erule alpha_rtrm1.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
55 done |
56 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
56 |
57 apply rule apply (erule alpha_bp.cases) apply (simp_all add: alpha_rtrm1_alpha_bp.intros) |
57 (* Shouyld we derive it? But bv is given by the user? *) |
58 done |
|
59 |
|
60 lemma alpha_bp_refl: "alpha_bp a a" |
|
61 apply induct |
|
62 apply (simp_all add: alpha1_inj) |
|
63 done |
|
64 |
|
65 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" |
|
66 apply rule |
|
67 apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) |
|
68 apply (simp_all add: alpha_bp_refl) |
|
69 done |
|
70 |
|
71 lemma alpha_bp_eq: "alpha_bp = (op =)" |
|
72 apply (rule ext)+ |
|
73 apply (rule alpha_bp_eq_eq) |
|
74 done |
|
75 |
58 lemma bv1_eqvt[eqvt]: |
76 lemma bv1_eqvt[eqvt]: |
59 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
77 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
60 apply (induct x) |
78 apply (induct x) |
61 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt) |
79 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts) |
62 done |
80 done |
63 |
81 |
64 lemma fv_rtrm1_eqvt[eqvt]: |
82 lemma fv_rtrm1_eqvt[eqvt]: |
65 shows "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
83 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
66 apply (induct t) |
84 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
|
85 apply (induct t and b) |
67 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
86 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
68 done |
87 done |
69 |
88 |
70 |
|
71 lemma alpha1_eqvt: |
89 lemma alpha1_eqvt: |
72 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
90 "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
73 apply (induct t s rule: alpha1.inducts) |
91 "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)" |
|
92 apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) |
74 apply (simp_all add:eqvts alpha1_inj) |
93 apply (simp_all add:eqvts alpha1_inj) |
75 apply (erule exE) |
94 apply (erule exE) |
76 apply (rule_tac x="pi \<bullet> pia" in exI) |
95 apply (rule_tac x="pi \<bullet> pia" in exI) |
77 apply (simp add: alpha_gen) |
96 apply (simp add: alpha_gen) |
78 apply(erule conjE)+ |
97 apply(erule conjE)+ |
82 apply(rule conjI) |
101 apply(rule conjI) |
83 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
102 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
84 apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) |
103 apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) |
85 apply(simp add: permute_eqvt[symmetric]) |
104 apply(simp add: permute_eqvt[symmetric]) |
86 apply (erule exE) |
105 apply (erule exE) |
|
106 apply (erule exE) |
|
107 apply (rule conjI) |
87 apply (rule_tac x="pi \<bullet> pia" in exI) |
108 apply (rule_tac x="pi \<bullet> pia" in exI) |
88 apply (simp add: alpha_gen) |
109 apply (simp add: alpha_gen) |
89 apply(erule conjE)+ |
110 apply(erule conjE)+ |
90 apply(rule conjI) |
111 apply(rule conjI) |
91 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
112 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
92 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
113 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
93 apply(rule conjI) |
114 apply(rule conjI) |
94 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
115 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
95 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
116 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
96 apply(simp add: permute_eqvt[symmetric]) |
117 apply(simp add: permute_eqvt[symmetric]) |
97 done |
118 apply (rule_tac x="pi \<bullet> piaa" in exI) |
98 |
119 apply (simp add: alpha_gen) |
99 lemma alpha1_equivp: "equivp alpha1" |
120 apply(erule conjE)+ |
|
121 apply(rule conjI) |
|
122 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
123 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
124 apply(rule conjI) |
|
125 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
126 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
127 apply(simp add: permute_eqvt[symmetric]) |
|
128 done |
|
129 |
|
130 lemma alpha1_equivp: "equivp alpha_rtrm1" |
100 sorry |
131 sorry |
101 |
132 |
102 quotient_type trm1 = rtrm1 / alpha1 |
133 quotient_type trm1 = rtrm1 / alpha_rtrm1 |
103 by (rule alpha1_equivp) |
134 by (rule alpha1_equivp) |
104 |
135 |
105 quotient_definition |
136 local_setup {* |
106 "Vr1 :: name \<Rightarrow> trm1" |
137 (fn ctxt => ctxt |
107 is |
138 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
108 "rVr1" |
139 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
109 |
140 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) |
110 quotient_definition |
141 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
111 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
142 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
112 is |
143 *} |
113 "rAp1" |
144 print_theorems |
114 |
|
115 quotient_definition |
|
116 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
117 is |
|
118 "rLm1" |
|
119 |
|
120 quotient_definition |
|
121 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
122 is |
|
123 "rLt1" |
|
124 |
|
125 quotient_definition |
|
126 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
|
127 is |
|
128 "fv_rtrm1" |
|
129 |
145 |
130 lemma alpha_rfv1: |
146 lemma alpha_rfv1: |
131 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
147 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
132 apply(induct rule: alpha1.induct) |
148 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
133 apply(simp_all add: alpha_gen.simps) |
149 apply(simp_all add: alpha_gen.simps) |
134 done |
150 done |
135 |
151 |
136 lemma [quot_respect]: |
152 lemma [quot_respect]: |
137 "(op = ===> alpha1) rVr1 rVr1" |
153 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
138 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
154 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
139 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
155 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
140 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" |
156 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
141 apply (auto simp add: alpha1_inj) |
157 apply (auto simp add: alpha1_inj) |
142 apply (rule_tac x="0" in exI) |
158 apply (rule_tac x="0" in exI) |
143 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
159 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
144 apply (rule_tac x="0" in exI) |
160 apply (rule_tac x="0" in exI) |
|
161 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
|
162 apply (rule_tac x="0" in exI) |
145 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) |
163 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) |
146 done |
164 done |
147 |
165 |
148 lemma [quot_respect]: |
166 lemma [quot_respect]: |
149 "(op = ===> alpha1 ===> alpha1) permute permute" |
167 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
150 by (simp add: alpha1_eqvt) |
168 by (simp add: alpha1_eqvt) |
151 |
169 |
152 lemma [quot_respect]: |
170 lemma [quot_respect]: |
153 "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1" |
171 "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1" |
154 by (simp add: alpha_rfv1) |
172 by (simp add: alpha_rfv1) |
155 |
173 |
156 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
174 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
157 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
175 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
158 |
176 |
238 apply(simp add: alpha1_INJ) |
267 apply(simp add: alpha1_INJ) |
239 apply(simp add: Abs_eq_iff) |
268 apply(simp add: Abs_eq_iff) |
240 apply(simp add: alpha_gen.simps) |
269 apply(simp add: alpha_gen.simps) |
241 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
270 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) |
242 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
271 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
243 apply(simp add: supp_Abs fv_trm1) |
272 apply(simp add: supp_Abs fv_trm1 fv_eq_bv) |
244 apply(simp (no_asm) add: supp_def) |
273 apply(simp (no_asm) add: supp_def) |
245 apply(simp add: alpha1_INJ) |
274 apply(simp add: alpha1_INJ alpha_bp_eq) |
246 apply(simp add: Abs_eq_iff) |
275 apply(simp add: Abs_eq_iff) |
247 apply(simp add: alpha_gen) |
276 apply(simp add: alpha_gen) |
248 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
277 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) |
249 apply(simp add: Collect_imp_eq Collect_neg_eq) |
278 apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper) |
250 done |
279 done |
251 |
280 |
252 lemma trm1_supp: |
281 lemma trm1_supp: |
253 "supp (Vr1 x) = {atom x}" |
282 "supp (Vr1 x) = {atom x}" |
254 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
283 "supp (Ap1 t1 t2) = supp t1 \<union> supp t2" |
255 "supp (Lm1 x t) = (supp t) - {atom x}" |
284 "supp (Lm1 x t) = (supp t) - {atom x}" |
256 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
285 "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)" |
257 by (simp_all only: supp_fv fv_trm1) |
286 by (simp_all add: supp_fv fv_trm1 fv_eq_bv) |
258 |
287 |
259 lemma trm1_induct_strong: |
288 lemma trm1_induct_strong: |
260 assumes "\<And>name b. P b (Vr1 name)" |
289 assumes "\<And>name b. P b (Vr1 name)" |
261 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
290 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
262 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
291 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
278 primrec |
307 primrec |
279 rbv2 |
308 rbv2 |
280 where |
309 where |
281 "rbv2 (rAs x t) = {atom x}" |
310 "rbv2 (rAs x t) = {atom x}" |
282 |
311 |
283 local_setup {* define_raw_fv "Terms.rtrm2" |
|
284 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
|
285 [[[(NONE, 0)], []]]] *} |
|
286 print_theorems |
|
287 |
|
288 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
312 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *} |
289 |
313 |
290 inductive |
314 local_setup {* snd o define_fv_alpha "Terms.rtrm2" |
291 alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100) |
315 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv2}, 0)], [(SOME @{term rbv2}, 0)]]], |
|
316 [[[], []]]] *} |
|
317 print_theorems |
|
318 |
|
319 notation |
|
320 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
|
321 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
|
322 thm alpha_rtrm2_alpha_rassign.intros |
|
323 |
|
324 lemma alpha2_equivp: |
|
325 "equivp alpha_rtrm2" |
|
326 "equivp alpha_rassign" |
|
327 sorry |
|
328 |
|
329 quotient_type |
|
330 trm2 = rtrm2 / alpha_rtrm2 |
292 and |
331 and |
293 alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100) |
332 assign = rassign / alpha_rassign |
294 where |
|
295 a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)" |
|
296 | a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2" |
|
297 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s" |
|
298 | a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s)); |
|
299 \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk> |
|
300 \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s" |
|
301 | a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *) |
|
302 |
|
303 lemma alpha2_equivp: |
|
304 "equivp alpha2" |
|
305 "equivp alpha2a" |
|
306 sorry |
|
307 |
|
308 quotient_type |
|
309 trm2 = rtrm2 / alpha2 |
|
310 and |
|
311 assign = rassign / alpha2a |
|
312 by (auto intro: alpha2_equivp) |
333 by (auto intro: alpha2_equivp) |
313 |
334 |
|
335 local_setup {* |
|
336 (fn ctxt => ctxt |
|
337 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
|
338 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
|
339 |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2})) |
|
340 |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2})) |
|
341 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) |
|
342 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
|
343 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
|
344 *} |
|
345 print_theorems |
314 |
346 |
315 |
347 |
316 section {*** lets with many assignments ***} |
348 section {*** lets with many assignments ***} |
317 |
349 |
318 datatype trm3 = |
350 datatype trm3 = |
329 bv3 |
361 bv3 |
330 where |
362 where |
331 "bv3 ANil = {}" |
363 "bv3 ANil = {}" |
332 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
364 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
333 |
365 |
334 local_setup {* define_raw_fv "Terms.trm3" |
|
335 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
|
336 [[], [[(NONE, 0)], [], []]]] *} |
|
337 print_theorems |
|
338 |
|
339 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
366 setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *} |
340 |
367 |
341 inductive |
368 local_setup {* snd o define_fv_alpha "Terms.trm3" |
342 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
369 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv3}, 0)], [(SOME @{term bv3}, 0)]]], |
|
370 [[], [[], [], []]]] *} |
|
371 print_theorems |
|
372 |
|
373 notation |
|
374 alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and |
|
375 alpha_assigns ("_ \<approx>3a _" [100, 100] 100) |
|
376 thm alpha_trm3_alpha_assigns.intros |
|
377 |
|
378 lemma alpha3_equivp: |
|
379 "equivp alpha_trm3" |
|
380 "equivp alpha_assigns" |
|
381 sorry |
|
382 |
|
383 quotient_type |
|
384 qtrm3 = trm3 / alpha_trm3 |
343 and |
385 and |
344 alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100) |
386 qassigns = assigns / alpha_assigns |
345 where |
|
346 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
|
347 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
|
348 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
|
349 | a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s)); |
|
350 \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk> |
|
351 \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s" |
|
352 | a5: "ANil \<approx>3a ANil" |
|
353 | a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st" |
|
354 |
|
355 lemma alpha3_equivp: |
|
356 "equivp alpha3" |
|
357 "equivp alpha3a" |
|
358 sorry |
|
359 |
|
360 quotient_type |
|
361 qtrm3 = trm3 / alpha3 |
|
362 and |
|
363 qassigns = assigns / alpha3a |
|
364 by (auto intro: alpha3_equivp) |
387 by (auto intro: alpha3_equivp) |
365 |
388 |
366 |
389 |
367 section {*** lam with indirect list recursion ***} |
390 section {*** lam with indirect list recursion ***} |
368 |
391 |
391 done |
410 done |
392 |
411 |
393 thm permute_trm4_permute_trm4_list.simps |
412 thm permute_trm4_permute_trm4_list.simps |
394 thm permute_trm4_permute_trm4_list.simps[simplified repaired] |
413 thm permute_trm4_permute_trm4_list.simps[simplified repaired] |
395 |
414 |
396 inductive |
415 local_setup {* snd o define_fv_alpha "Terms.trm4" [ |
397 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
416 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
398 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
417 print_theorems |
399 where |
418 |
400 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
419 notation |
401 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
420 alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and |
402 | a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
421 alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100) |
403 | a5: "[] \<approx>4list []" |
422 thm alpha_trm4_alpha_trm4_list.intros |
404 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
423 |
405 |
424 lemma alpha4_equivp: "equivp alpha_trm4" sorry |
406 lemma alpha4_equivp: "equivp alpha4" sorry |
425 lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry |
407 lemma alpha4list_equivp: "equivp alpha4list" sorry |
|
408 |
426 |
409 quotient_type |
427 quotient_type |
410 qtrm4 = trm4 / alpha4 and |
428 qtrm4 = trm4 / alpha_trm4 and |
411 qtrm4list = "trm4 list" / alpha4list |
429 qtrm4list = "trm4 list" / alpha_trm4_list |
412 by (simp_all add: alpha4_equivp alpha4list_equivp) |
430 by (simp_all add: alpha4_equivp alpha4list_equivp) |
413 |
431 |
414 |
432 |
415 datatype rtrm5 = |
433 datatype rtrm5 = |
416 rVr5 "name" |
434 rVr5 "name" |
424 rbv5 |
442 rbv5 |
425 where |
443 where |
426 "rbv5 rLnil = {}" |
444 "rbv5 rLnil = {}" |
427 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
445 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
428 |
446 |
429 local_setup {* define_raw_fv "Terms.rtrm5" [ |
|
430 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE, 0)], [], []]] ] *} |
|
431 print_theorems |
|
432 |
447 |
433 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
448 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
434 print_theorems |
449 print_theorems |
435 |
450 |
436 inductive |
451 local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ |
437 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100) |
452 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
438 and |
453 print_theorems |
439 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
454 |
440 where |
455 (* Alternate version with additional binding of name in rlts in rLcons *) |
441 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
456 (*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [ |
442 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
457 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
443 | a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2)); |
458 print_theorems*) |
444 \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk> |
459 |
445 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
460 notation |
446 | a4: "rLnil \<approx>l rLnil" |
461 alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and |
447 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
462 alpha_rlts ("_ \<approx>l _" [100, 100] 100) |
448 |
463 thm alpha_rtrm5_alpha_rlts.intros |
449 print_theorems |
|
450 |
464 |
451 lemma alpha5_inj: |
465 lemma alpha5_inj: |
452 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
466 "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)" |
453 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
467 "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)" |
454 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and> |
468 "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha_rtrm5 fv_rtrm5 pi (rbv5 l2, t2))) \<and> |
455 (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))" |
469 (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alpha_rlts fv_rlts pi (rbv5 l2, l2))))" |
456 "rLnil \<approx>l rLnil" |
470 "rLnil \<approx>l rLnil" |
457 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)" |
471 "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)" |
458 apply - |
472 apply - |
459 apply (simp_all add: alpha5_alphalts.intros) |
473 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
460 apply rule |
474 apply rule |
461 apply (erule alpha5.cases) |
475 apply (erule alpha_rtrm5.cases) |
462 apply (simp_all add: alpha5_alphalts.intros) |
476 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
463 apply rule |
477 apply rule |
464 apply (erule alpha5.cases) |
478 apply (erule alpha_rtrm5.cases) |
465 apply (simp_all add: alpha5_alphalts.intros) |
479 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
466 apply rule |
480 apply rule |
467 apply (erule alpha5.cases) |
481 apply (erule alpha_rtrm5.cases) |
468 apply (simp_all add: alpha5_alphalts.intros) |
482 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
469 apply rule |
483 apply rule |
470 apply (erule alphalts.cases) |
484 apply (erule alpha_rlts.cases) |
471 apply (simp_all add: alpha5_alphalts.intros) |
485 apply (simp_all add: alpha_rtrm5_alpha_rlts.intros) |
472 done |
486 done |
473 |
487 |
474 lemma alpha5_equivps: |
488 lemma alpha5_equivps: |
475 shows "equivp alpha5" |
489 shows "equivp alpha_rtrm5" |
476 and "equivp alphalts" |
490 and "equivp alpha_rlts" |
477 sorry |
491 sorry |
478 |
492 |
479 quotient_type |
493 quotient_type |
480 trm5 = rtrm5 / alpha5 |
494 trm5 = rtrm5 / alpha_rtrm5 |
481 and |
495 and |
482 lts = rlts / alphalts |
496 lts = rlts / alpha_rlts |
483 by (auto intro: alpha5_equivps) |
497 by (auto intro: alpha5_equivps) |
484 |
498 |
485 quotient_definition |
499 local_setup {* |
486 "Vr5 :: name \<Rightarrow> trm5" |
500 (fn ctxt => ctxt |
487 is |
501 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
488 "rVr5" |
502 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
489 |
503 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
490 quotient_definition |
504 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
491 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5" |
505 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
492 is |
506 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
493 "rAp5" |
507 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
494 |
508 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
495 quotient_definition |
509 *} |
496 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5" |
510 print_theorems |
497 is |
|
498 "rLt5" |
|
499 |
|
500 quotient_definition |
|
501 "Lnil :: lts" |
|
502 is |
|
503 "rLnil" |
|
504 |
|
505 quotient_definition |
|
506 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts" |
|
507 is |
|
508 "rLcons" |
|
509 |
|
510 quotient_definition |
|
511 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
|
512 is |
|
513 "fv_rtrm5" |
|
514 |
|
515 quotient_definition |
|
516 "fv_lts :: lts \<Rightarrow> atom set" |
|
517 is |
|
518 "fv_rlts" |
|
519 |
|
520 quotient_definition |
|
521 "bv5 :: lts \<Rightarrow> atom set" |
|
522 is |
|
523 "rbv5" |
|
524 |
511 |
525 lemma rbv5_eqvt: |
512 lemma rbv5_eqvt: |
526 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
513 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
527 sorry |
514 sorry |
528 |
515 |
535 sorry |
522 sorry |
536 |
523 |
537 lemma alpha5_eqvt: |
524 lemma alpha5_eqvt: |
538 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
525 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
539 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
526 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
540 apply(induct rule: alpha5_alphalts.inducts) |
527 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
541 apply (simp_all add: alpha5_inj) |
528 apply (simp_all add: alpha5_inj) |
542 apply (erule exE)+ |
529 apply (erule exE)+ |
543 apply(unfold alpha_gen) |
530 apply(unfold alpha_gen) |
544 apply (erule conjE)+ |
531 apply (erule conjE)+ |
545 apply (rule conjI) |
532 apply (rule conjI) |
546 apply (rule_tac x="x \<bullet> pi" in exI) |
533 apply (rule_tac x="x \<bullet> pia" in exI) |
547 apply (rule conjI) |
534 apply (rule conjI) |
548 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
535 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
549 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
536 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
550 apply(rule conjI) |
537 apply(rule conjI) |
551 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
538 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
552 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
539 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
553 apply (subst permute_eqvt[symmetric]) |
540 apply (subst permute_eqvt[symmetric]) |
554 apply (simp) |
541 apply (simp) |
555 apply (rule_tac x="x \<bullet> pia" in exI) |
542 apply (rule_tac x="x \<bullet> pi" in exI) |
556 apply (rule conjI) |
543 apply (rule conjI) |
557 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
544 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
558 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
545 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
559 apply(rule conjI) |
546 apply(rule conjI) |
560 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
547 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
564 done |
551 done |
565 |
552 |
566 lemma alpha5_rfv: |
553 lemma alpha5_rfv: |
567 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
554 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
568 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
555 "(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)" |
569 apply(induct rule: alpha5_alphalts.inducts) |
556 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
570 apply(simp_all add: alpha_gen) |
557 apply(simp_all add: alpha_gen) |
571 done |
558 done |
572 |
559 |
573 lemma bv_list_rsp: |
560 lemma bv_list_rsp: |
574 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
561 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
575 apply(induct rule: alpha5_alphalts.inducts(2)) |
562 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts(2)) |
576 apply(simp_all) |
563 apply(simp_all) |
577 done |
564 done |
578 |
565 |
579 lemma [quot_respect]: |
566 lemma [quot_respect]: |
580 "(alphalts ===> op =) fv_rlts fv_rlts" |
567 "(alpha_rlts ===> op =) fv_rlts fv_rlts" |
581 "(alpha5 ===> op =) fv_rtrm5 fv_rtrm5" |
568 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
582 "(alphalts ===> op =) rbv5 rbv5" |
569 "(alpha_rlts ===> op =) rbv5 rbv5" |
583 "(op = ===> alpha5) rVr5 rVr5" |
570 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
584 "(alpha5 ===> alpha5 ===> alpha5) rAp5 rAp5" |
571 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
585 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
572 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
586 "(alphalts ===> alpha5 ===> alpha5) rLt5 rLt5" |
573 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
587 "(op = ===> alpha5 ===> alphalts ===> alphalts) rLcons rLcons" |
574 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
588 "(op = ===> alpha5 ===> alpha5) permute permute" |
575 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
589 "(op = ===> alphalts ===> alphalts) permute permute" |
576 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
590 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
577 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
591 apply (clarify) apply (rule conjI) |
578 apply (clarify) apply (rule conjI) |
592 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
579 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
593 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
580 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
594 apply (clarify) apply (rule conjI) |
581 apply (clarify) apply (rule conjI) |
595 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
582 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
596 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
583 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
597 done |
584 done |
598 |
585 |
599 lemma |
586 lemma |
600 shows "(alphalts ===> op =) rbv5 rbv5" |
587 shows "(alpha_rlts ===> op =) rbv5 rbv5" |
601 by (simp add: bv_list_rsp) |
588 by (simp add: bv_list_rsp) |
602 |
589 |
603 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
590 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] |
604 |
591 |
605 instantiation trm5 and lts :: pt |
592 instantiation trm5 and lts :: pt |
717 where |
704 where |
718 "rbv6 (rVr6 n) = {}" |
705 "rbv6 (rVr6 n) = {}" |
719 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
706 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
720 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
707 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
721 |
708 |
722 local_setup {* define_raw_fv "Terms.rtrm6" [ |
|
723 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
|
724 print_theorems |
|
725 |
|
726 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
709 setup {* snd o define_raw_perms ["rtrm6"] ["Terms.rtrm6"] *} |
727 print_theorems |
710 print_theorems |
|
711 |
|
712 local_setup {* snd o define_fv_alpha "Terms.rtrm6" [ |
|
713 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv6}, 0)], [(SOME @{term rbv6}, 0)]]]] *} |
|
714 notation alpha_rtrm6 ("_ \<approx>6a _" [100, 100] 100) |
|
715 (* HERE THE RULES DIFFER *) |
|
716 thm alpha_rtrm6.intros |
728 |
717 |
729 inductive |
718 inductive |
730 alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100) |
719 alpha6 :: "rtrm6 \<Rightarrow> rtrm6 \<Rightarrow> bool" ("_ \<approx>6 _" [100, 100] 100) |
731 where |
720 where |
732 a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)" |
721 a1: "a = b \<Longrightarrow> (rVr6 a) \<approx>6 (rVr6 b)" |
739 |
728 |
740 quotient_type |
729 quotient_type |
741 trm6 = rtrm6 / alpha6 |
730 trm6 = rtrm6 / alpha6 |
742 by (auto intro: alpha6_equivps) |
731 by (auto intro: alpha6_equivps) |
743 |
732 |
744 quotient_definition |
733 local_setup {* |
745 "Vr6 :: name \<Rightarrow> trm6" |
734 (fn ctxt => ctxt |
746 is |
735 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
747 "rVr6" |
736 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
748 |
737 |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) |
749 quotient_definition |
738 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) |
750 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6" |
739 |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) |
751 is |
740 *} |
752 "rLm6" |
741 print_theorems |
753 |
|
754 quotient_definition |
|
755 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
756 is |
|
757 "rLt6" |
|
758 |
|
759 quotient_definition |
|
760 "fv_trm6 :: trm6 \<Rightarrow> atom set" |
|
761 is |
|
762 "fv_rtrm6" |
|
763 |
|
764 quotient_definition |
|
765 "bv6 :: trm6 \<Rightarrow> atom set" |
|
766 is |
|
767 "rbv6" |
|
768 |
742 |
769 lemma [quot_respect]: |
743 lemma [quot_respect]: |
770 "(op = ===> alpha6 ===> alpha6) permute permute" |
744 "(op = ===> alpha6 ===> alpha6) permute permute" |
771 apply auto (* will work with eqvt *) |
745 apply auto (* will work with eqvt *) |
772 sorry |
746 sorry |
773 |
747 |
774 (* Definitely not true , see lemma below *) |
748 (* Definitely not true , see lemma below *) |
775 |
|
776 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
749 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
777 apply simp apply clarify |
750 apply simp apply clarify |
778 apply (erule alpha6.induct) |
751 apply (erule alpha6.induct) |
779 oops |
752 oops |
780 |
753 |
873 where |
846 where |
874 "rbv7 (rVr7 n) = {atom n}" |
847 "rbv7 (rVr7 n) = {atom n}" |
875 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
848 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
876 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
849 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
877 |
850 |
878 local_setup {* define_raw_fv "Terms.rtrm7" [ |
|
879 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
|
880 print_theorems |
|
881 |
|
882 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
851 setup {* snd o define_raw_perms ["rtrm7"] ["Terms.rtrm7"] *} |
883 print_theorems |
852 print_theorems |
|
853 |
|
854 local_setup {* snd o define_fv_alpha "Terms.rtrm7" [ |
|
855 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term rbv7}, 0)], [(SOME @{term rbv7}, 0)]]]] *} |
|
856 notation |
|
857 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
|
858 (* HERE THE RULES DIFFER *) |
|
859 thm alpha_rtrm7.intros |
884 |
860 |
885 inductive |
861 inductive |
886 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
862 alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100) |
887 where |
863 where |
888 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
864 a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)" |
889 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
865 | a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s" |
890 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
866 | a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2" |
891 |
|
892 lemma bvfv7: "rbv7 x = fv_rtrm7 x" |
|
893 apply induct |
|
894 apply simp_all |
|
895 done |
|
896 |
867 |
897 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
868 lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7" |
898 apply simp |
869 apply simp |
899 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
870 apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI) |
900 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
871 apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI) |
921 rbv8 |
892 rbv8 |
922 where |
893 where |
923 "rbv8 (Bar0 x) = {}" |
894 "rbv8 (Bar0 x) = {}" |
924 | "rbv8 (Bar1 v x b) = {atom v}" |
895 | "rbv8 (Bar1 v x b) = {atom v}" |
925 |
896 |
926 local_setup {* define_raw_fv "Terms.rfoo8" [ |
|
927 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
|
928 print_theorems |
|
929 |
|
930 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
897 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Terms.rfoo8", "Terms.rbar8"] *} |
931 print_theorems |
898 print_theorems |
|
899 |
|
900 local_setup {* snd o define_fv_alpha "Terms.rfoo8" [ |
|
901 [[[]], [[(SOME @{term rbv8}, 0)], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
|
902 notation |
|
903 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
|
904 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
|
905 (* HERE THE RULE DIFFERS *) |
|
906 thm alpha_rfoo8_alpha_rbar8.intros |
|
907 |
932 |
908 |
933 inductive |
909 inductive |
934 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
910 alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100) |
935 and |
911 and |
936 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
912 alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100) |
975 rbv9 |
954 rbv9 |
976 where |
955 where |
977 "rbv9 (Var9 x) = {}" |
956 "rbv9 (Var9 x) = {}" |
978 | "rbv9 (Lam9 x b) = {atom x}" |
957 | "rbv9 (Lam9 x b) = {atom x}" |
979 |
958 |
980 local_setup {* define_raw_fv "Terms.rlam9" [ |
|
981 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
|
982 print_theorems |
|
983 |
|
984 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
959 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Terms.rlam9", "Terms.rbla9"] *} |
985 print_theorems |
960 print_theorems |
|
961 |
|
962 local_setup {* snd o define_fv_alpha "Terms.rlam9" [ |
|
963 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[(SOME @{term rbv9}, 0)], [(SOME @{term rbv9}, 0)]]]] *} |
|
964 notation |
|
965 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
|
966 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
|
967 (* HERE THE RULES DIFFER *) |
|
968 thm alpha_rlam9_alpha_rbla9.intros |
|
969 |
986 |
970 |
987 inductive |
971 inductive |
988 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
972 alpha9l :: "rlam9 \<Rightarrow> rlam9 \<Rightarrow> bool" ("_ \<approx>9l _" [100, 100] 100) |
989 and |
973 and |
990 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
974 alpha9b :: "rbla9 \<Rightarrow> rbla9 \<Rightarrow> bool" ("_ \<approx>9b _" [100, 100] 100) |
1070 All "name set" "ty" |
1035 All "name set" "ty" |
1071 |
1036 |
1072 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
1037 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *} |
1073 print_theorems |
1038 print_theorems |
1074 |
1039 |
1075 abbreviation |
|
1076 "atoms xs \<equiv> {atom x| x. x \<in> xs}" |
|
1077 |
|
1078 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} |
1040 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *} |
1079 print_theorems |
1041 print_theorems |
1080 |
1042 |
1081 (* |
1043 (* |
1082 doesn't work yet |
1044 Doesnot work yet since we do not refer to fv_ty |
1083 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
1045 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *} |
1084 print_theorems |
1046 print_theorems |
1085 *) |
1047 *) |
1086 |
1048 |
1087 primrec |
1049 primrec |
1088 fv_tyS |
1050 fv_tyS |
1089 where |
1051 where |
1090 "fv_tyS (All xs T) = (fv_ty T - atoms xs)" |
1052 "fv_tyS (All xs T) = (fv_ty T - atom ` xs)" |
1091 |
1053 |
1092 inductive |
1054 inductive |
1093 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
1055 alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100) |
1094 where |
1056 where |
1095 a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2)) |
1057 a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) |
1096 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
1058 \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2" |
1097 |
1059 |
1098 lemma |
1060 lemma |
1099 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
1061 shows "All {a, b} (Fun (Var a) (Var b)) \<approx>tyS All {b, a} (Fun (Var a) (Var b))" |
1100 apply(rule a1) |
1062 apply(rule a1) |