119 |
119 |
120 lemma alpha1_eqvt: |
120 lemma alpha1_eqvt: |
121 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
121 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
122 apply (induct t s rule: alpha1.inducts) |
122 apply (induct t s rule: alpha1.inducts) |
123 apply (simp_all add:eqvts alpha1_inj) |
123 apply (simp_all add:eqvts alpha1_inj) |
124 sorry |
124 apply (erule exE) |
|
125 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
126 apply (simp add: alpha_gen) |
|
127 apply(erule conjE)+ |
|
128 apply(rule conjI) |
|
129 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
130 apply(simp add: atom_eqvt eqvts) |
|
131 apply(rule conjI) |
|
132 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
133 apply(simp add: eqvts atom_eqvt) |
|
134 apply(simp add: permute_eqvt[symmetric]) |
|
135 apply (erule exE) |
|
136 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
137 apply (simp add: alpha_gen) |
|
138 apply(erule conjE)+ |
|
139 apply(rule conjI) |
|
140 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
141 apply(simp add: atom_eqvt eqvts) |
|
142 apply(rule conjI) |
|
143 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
144 apply(simp add: eqvts atom_eqvt) |
|
145 apply(simp add: permute_eqvt[symmetric]) |
|
146 done |
125 |
147 |
126 lemma alpha1_equivp: "equivp alpha1" |
148 lemma alpha1_equivp: "equivp alpha1" |
127 sorry |
149 sorry |
128 |
150 |
129 quotient_type trm1 = rtrm1 / alpha1 |
151 quotient_type trm1 = rtrm1 / alpha1 |
329 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
351 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)") |
330 apply(simp add: supp_Abs fv_trm1) |
352 apply(simp add: supp_Abs fv_trm1) |
331 apply(simp (no_asm) add: supp_def) |
353 apply(simp (no_asm) add: supp_def) |
332 apply(simp add: alpha1_INJ) |
354 apply(simp add: alpha1_INJ) |
333 apply(simp add: Abs_eq_iff) |
355 apply(simp add: Abs_eq_iff) |
334 apply(simp add: alpha_gen.simps) |
356 apply(simp add: alpha_gen) |
335 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
357 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt) |
336 apply(simp add: Collect_imp_eq Collect_neg_eq) |
358 apply(simp add: Collect_imp_eq Collect_neg_eq) |
337 done |
359 done |
338 |
360 |
339 lemma trm1_supp: |
361 lemma trm1_supp: |
347 assumes "\<And>name b. P b (Vr1 name)" |
369 assumes "\<And>name b. P b (Vr1 name)" |
348 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
370 and "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)" |
349 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
371 and "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)" |
350 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
372 and "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)" |
351 shows "P a rtrma" |
373 shows "P a rtrma" |
352 |
374 sorry |
353 |
375 |
354 section {*** lets with single assignments ***} |
376 section {*** lets with single assignments ***} |
355 |
377 |
356 datatype trm2 = |
378 datatype trm2 = |
357 Vr2 "name" |
379 Vr2 "name" |
626 qtrm4list = "trm4 list" / alpha4list |
648 qtrm4list = "trm4 list" / alpha4list |
627 by (simp_all add: alpha4_equivp alpha4list_equivp) |
649 by (simp_all add: alpha4_equivp alpha4list_equivp) |
628 |
650 |
629 |
651 |
630 |
652 |
|
653 |
|
654 |
|
655 |
|
656 |
|
657 |
|
658 datatype rtrm5 = |
|
659 rVr5 "name" |
|
660 | rAp5 "rtrm5" "rtrm5" |
|
661 | rLt5 "rlts" "rtrm5" |
|
662 and rlts = |
|
663 rLnil |
|
664 | rLcons "name" "rtrm5" "rlts" |
|
665 |
|
666 primrec |
|
667 bv5 |
|
668 where |
|
669 "bv5 rLnil = {}" |
|
670 | "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)" |
|
671 |
|
672 primrec |
|
673 rfv_trm5 and rfv_lts |
|
674 where |
|
675 "rfv_trm5 (rVr5 n) = {atom n}" |
|
676 | "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)" |
|
677 | "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)" |
|
678 | "rfv_lts (rLnil) = {}" |
|
679 | "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)" |
|
680 |
|
681 instantiation |
|
682 rtrm5 and rlts :: pt |
|
683 begin |
|
684 |
|
685 primrec |
|
686 permute_rtrm5 and permute_rlts |
|
687 where |
|
688 "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)" |
|
689 | "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)" |
|
690 | "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)" |
|
691 | "permute_rlts pi (rLnil) = rLnil" |
|
692 | "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)" |
|
693 |
|
694 lemma pt_rtrm5_zero: |
|
695 fixes t::rtrm5 |
|
696 and l::rlts |
|
697 shows "0 \<bullet> t = t" |
|
698 and "0 \<bullet> l = l" |
|
699 apply(induct t and l rule: rtrm5_rlts.inducts) |
|
700 apply(simp_all) |
|
701 done |
|
702 |
|
703 lemma pt_rtrm5_plus: |
|
704 fixes t::rtrm5 |
|
705 and l::rlts |
|
706 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
707 and "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)" |
|
708 apply(induct t and l rule: rtrm5_rlts.inducts) |
|
709 apply(simp_all) |
|
710 done |
|
711 |
|
712 instance |
|
713 apply default |
|
714 apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus) |
|
715 done |
|
716 |
631 end |
717 end |
|
718 |
|
719 inductive |
|
720 alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100) |
|
721 and |
|
722 alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100) |
|
723 where |
|
724 a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)" |
|
725 | a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2" |
|
726 | a3: "\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and> |
|
727 (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and> |
|
728 (pi \<bullet> (bv5 l1) = bv5 l2)) |
|
729 \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2" |
|
730 | a4: "rLnil \<approx>l rLnil" |
|
731 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2" |
|
732 |
|
733 thm a3[simplified alpha_gen] |
|
734 end |