151 inductive |
151 inductive |
152 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
152 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
153 where |
153 where |
154 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
154 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
155 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
155 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
156 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
156 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s) |
157 \<Longrightarrow> rLam a t \<approx> rLam b s" |
157 \<Longrightarrow> rLam a t \<approx> rLam b s" |
|
158 |
|
159 lemma a3_inverse: |
|
160 assumes "rLam a t \<approx> rLam b s" |
|
161 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)" |
|
162 using assms |
|
163 apply(erule_tac alpha.cases) |
|
164 apply(auto) |
|
165 done |
158 |
166 |
159 text {* should be automatic with new version of eqvt-machinery *} |
167 text {* should be automatic with new version of eqvt-machinery *} |
160 lemma alpha_eqvt: |
168 lemma alpha_eqvt: |
161 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
169 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
162 apply(induct rule: alpha.induct) |
170 apply(induct rule: alpha.induct) |
172 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
180 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
173 apply(simp add: eqvts atom_eqvt) |
181 apply(simp add: eqvts atom_eqvt) |
174 apply(rule conjI) |
182 apply(rule conjI) |
175 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
183 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
176 apply(simp add: eqvts atom_eqvt) |
184 apply(simp add: eqvts atom_eqvt) |
177 apply(rule conjI) |
|
178 apply(subst permute_eqvt[symmetric]) |
|
179 apply(simp) |
|
180 apply(subst permute_eqvt[symmetric]) |
185 apply(subst permute_eqvt[symmetric]) |
181 apply(simp) |
186 apply(simp) |
182 done |
187 done |
183 |
188 |
184 lemma alpha_refl: |
189 lemma alpha_refl: |
229 apply(rule a3) |
231 apply(rule a3) |
230 apply(rule_tac x="pia + pi" in exI) |
232 apply(rule_tac x="pia + pi" in exI) |
231 apply(simp add: fresh_star_plus) |
233 apply(simp add: fresh_star_plus) |
232 apply(drule_tac x="- pia \<bullet> sa" in spec) |
234 apply(drule_tac x="- pia \<bullet> sa" in spec) |
233 apply(drule mp) |
235 apply(drule mp) |
234 apply(rotate_tac 8) |
236 apply(rotate_tac 7) |
235 apply(drule_tac pi="- pia" in alpha_eqvt) |
237 apply(drule_tac pi="- pia" in alpha_eqvt) |
236 apply(simp) |
238 apply(simp) |
237 apply(rotate_tac 11) |
239 apply(rotate_tac 9) |
238 apply(drule_tac pi="pia" in alpha_eqvt) |
240 apply(drule_tac pi="pia" in alpha_eqvt) |
239 apply(simp) |
241 apply(simp) |
240 done |
242 done |
241 |
243 |
242 lemma alpha_equivp: |
244 lemma alpha_equivp: |
438 lemma a2: |
435 lemma a2: |
439 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
436 "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc" |
440 by (lifting a2) |
437 by (lifting a2) |
441 |
438 |
442 lemma a3: |
439 lemma a3: |
443 "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s \<and> (pi \<bullet> a) = b)\<rbrakk> |
440 "\<lbrakk>\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)\<rbrakk> |
444 \<Longrightarrow> Lam a t = Lam b s" |
441 \<Longrightarrow> Lam a t = Lam b s" |
445 apply (lifting a3) |
442 apply (lifting a3) |
446 done |
443 done |
|
444 |
|
445 lemma a3_inv: |
|
446 assumes "Lam a t = Lam b s" |
|
447 shows "\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s)" |
|
448 using assms |
|
449 apply(lifting a3_inverse) |
|
450 done |
447 |
451 |
448 lemma alpha_cases: |
452 lemma alpha_cases: |
449 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
453 "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P; |
450 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
454 \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P; |
451 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
455 \<And>t a s b. \<lbrakk>a1 = Lam a t; a2 = Lam b s; |
452 \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> |
456 \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s\<rbrakk> |
453 \<Longrightarrow> P\<rbrakk> |
457 \<Longrightarrow> P\<rbrakk> |
454 \<Longrightarrow> P" |
458 \<Longrightarrow> P" |
455 by (lifting alpha.cases) |
459 by (lifting alpha.cases) |
456 |
460 |
457 (* not sure whether needed *) |
461 (* not sure whether needed *) |
458 lemma alpha_induct: |
462 lemma alpha_induct: |
459 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
463 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
460 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
464 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
461 \<And>t a s b. |
465 \<And>t a s b. |
462 \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
466 \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
463 (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s) \<and> pi \<bullet> a = b\<rbrakk> |
467 (fv t - {atom a}) \<sharp>* pi \<and> ((pi \<bullet> t) = s \<and> qxb (pi \<bullet> t) s)\<rbrakk> |
464 \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
468 \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk> |
465 \<Longrightarrow> qxb qx qxa" |
469 \<Longrightarrow> qxb qx qxa" |
466 by (lifting alpha.induct) |
470 by (lifting alpha.induct) |
467 |
471 |
468 (* should they lift automatically *) |
472 (* should they lift automatically *) |
482 apply(simp_all) |
486 apply(simp_all) |
483 apply(drule alpha.cases) |
487 apply(drule alpha.cases) |
484 apply(simp_all) |
488 apply(simp_all) |
485 apply(rule alpha.a2) |
489 apply(rule alpha.a2) |
486 apply(simp_all) |
490 apply(simp_all) |
|
491 done |
|
492 |
|
493 lemma Lam_pseudo_inject: |
|
494 shows "(Lam a t = Lam b s) = |
|
495 (\<exists>pi. (fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) = s))" |
|
496 apply(rule iffI) |
|
497 apply(rule a3_inv) |
|
498 apply(assumption) |
|
499 apply(rule a3) |
|
500 apply(assumption) |
487 done |
501 done |
488 |
502 |
489 lemma rlam_distinct: |
503 lemma rlam_distinct: |
490 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
504 shows "\<not>(rVar nam \<approx> rApp rlam1' rlam2')" |
491 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
505 and "\<not>(rApp rlam1' rlam2' \<approx> rVar nam)" |
558 apply(simp add: var_supp) |
572 apply(simp add: var_supp) |
559 apply(simp add: app_supp) |
573 apply(simp add: app_supp) |
560 apply(simp add: lam_fsupp1) |
574 apply(simp add: lam_fsupp1) |
561 done |
575 done |
562 |
576 |
563 lemma lam_fresh1: |
577 lemma lam_supp2: |
564 assumes f: "finite (supp t)" |
578 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
565 and a1: "b \<sharp> t" |
579 apply(simp add: supp_def permute_set_eq atom_eqvt) |
566 and a2: "atom a \<noteq> b" |
580 apply(simp add: Lam_pseudo_inject) |
567 shows "b \<sharp> Lam a t" |
581 apply(simp add: abs_eq) |
568 proof - |
|
569 have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry |
|
570 then obtain c where fr1: "c \<noteq> b" |
|
571 and fr2: "c \<noteq> atom a" |
|
572 and fr3: "c \<sharp> t" |
|
573 and fr4: "c \<sharp> Lam a t" |
|
574 and fr5: "sort_of b = sort_of c" |
|
575 apply(auto simp add: fresh_Pair fresh_atom) |
|
576 sorry |
|
577 have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2 |
|
578 by simp |
|
579 from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))" |
|
580 by (simp only: fresh_permute_iff) |
|
581 then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e |
|
582 by simp |
|
583 then show ?thesis using a1 fr3 |
|
584 by (simp only: swap_fresh_fresh) |
|
585 qed |
|
586 |
|
587 lemma lam_fresh2: |
|
588 assumes f: "finite (supp t)" |
|
589 shows "(atom a) \<sharp> Lam a t" |
|
590 sorry |
582 sorry |
591 |
|
592 |
583 |
593 lemma lam_supp: |
584 lemma lam_supp: |
594 shows "supp (Lam x t) = ((supp t) - {atom x})" |
585 shows "supp (Lam x t) = ((supp t) - {atom x})" |
595 apply(default) |
586 apply(simp add: lam_supp2) |
596 apply(simp_all add: supp_conv_fresh) |
587 apply(simp add: supp_Abs) |
597 apply(auto) |
588 done |
598 sorry |
|
599 |
589 |
600 lemma fresh_lam: |
590 lemma fresh_lam: |
601 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
591 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
602 apply(simp add: fresh_def) |
592 apply(simp add: fresh_def) |
603 apply(simp add: lam_supp) |
593 apply(simp add: lam_supp) |