201 lemma [quot_respect]: |
201 lemma [quot_respect]: |
202 "(alpha1 ===> op =) rfv_trm1 rfv_trm1" |
202 "(alpha1 ===> op =) rfv_trm1 rfv_trm1" |
203 apply (simp add: alpha_rfv1) |
203 apply (simp add: alpha_rfv1) |
204 done |
204 done |
205 |
205 |
206 lemma trm1_bp_induct: " |
206 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
207 \<lbrakk>\<And>name. P1 (Vr1 name); |
207 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
208 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
209 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
210 \<And>bp rtrm11 rtrm12. |
|
211 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
212 P2 BUnit; \<And>name. P2 (BVr name); |
|
213 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
214 \<Longrightarrow> P1 rtrma \<and> P2 bpa" |
|
215 apply (lifting rtrm1_bp.induct) |
|
216 done |
|
217 |
|
218 lemma trm1_bp_inducts: " |
|
219 \<lbrakk>\<And>name. P1 (Vr1 name); |
|
220 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
221 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
222 \<And>bp rtrm11 rtrm12. |
|
223 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
224 P2 BUnit; \<And>name. P2 (BVr name); |
|
225 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
226 \<Longrightarrow> P1 rtrma" |
|
227 "\<lbrakk>\<And>name. P1 (Vr1 name); |
|
228 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
229 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
230 \<And>bp rtrm11 rtrm12. |
|
231 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
232 P2 BUnit; \<And>name. P2 (BVr name); |
|
233 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
234 \<Longrightarrow> P2 bpa" |
|
235 by (lifting rtrm1_bp.inducts) |
|
236 |
208 |
237 instantiation trm1 and bp :: pt |
209 instantiation trm1 and bp :: pt |
238 begin |
210 begin |
239 |
211 |
240 quotient_definition |
212 quotient_definition |
241 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
213 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
242 as |
214 as |
243 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
215 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
244 |
216 |
245 lemma permute_trm1 [simp]: |
|
246 shows "pi \<bullet> Vr1 a = Vr1 (pi \<bullet> a)" |
|
247 and "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)" |
|
248 and "pi \<bullet> Lm1 a t = Lm1 (pi \<bullet> a) (pi \<bullet> t)" |
|
249 and "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)" |
|
250 apply - |
|
251 apply(lifting permute_rtrm1_permute_bp.simps(1)) |
|
252 apply(lifting permute_rtrm1_permute_bp.simps(2)) |
|
253 apply(lifting permute_rtrm1_permute_bp.simps(3)) |
|
254 apply(lifting permute_rtrm1_permute_bp.simps(4)) |
|
255 done |
|
256 instance |
217 instance |
257 apply default |
218 apply default |
258 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
219 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
259 apply(simp_all) |
220 apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted]) |
260 done |
221 done |
261 |
222 |
262 end |
223 end |
263 |
224 |
264 lemma fv_trm1: |
225 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
265 "fv_trm1 (Vr1 x) = {atom x}" |
226 |
266 "fv_trm1 (Ap1 t1 t2) = fv_trm1 t1 \<union> fv_trm1 t2" |
227 lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted] |
267 "fv_trm1 (Lm1 x t) = fv_trm1 t - {atom x}" |
228 |
268 "fv_trm1 (Lt1 bp t1 t2) = fv_trm1 t1 \<union> (fv_trm1 t2 - bv1 bp)" |
229 lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted] |
269 apply - |
230 |
270 apply (lifting rfv_trm1_rfv_bp.simps(1)) |
231 lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
271 apply (lifting rfv_trm1_rfv_bp.simps(2)) |
|
272 apply (lifting rfv_trm1_rfv_bp.simps(3)) |
|
273 apply (lifting rfv_trm1_rfv_bp.simps(4)) |
|
274 done |
|
275 |
|
276 lemma fv_trm1_eqvt: |
|
277 shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)" |
|
278 apply(lifting rfv_trm1_eqvt) |
|
279 done |
|
280 |
|
281 lemma alpha1_INJ: |
|
282 "(Vr1 a = Vr1 b) = (a = b)" |
|
283 "(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)" |
|
284 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
|
285 "(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))" |
|
286 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
|
287 done |
|
288 |
232 |
289 lemma lm1_supp_pre: |
233 lemma lm1_supp_pre: |
290 shows "(supp (atom x, t)) supports (Lm1 x t) " |
234 shows "(supp (atom x, t)) supports (Lm1 x t) " |
291 apply(simp add: supports_def) |
235 apply(simp add: supports_def) |
292 apply(fold fresh_def) |
236 apply(fold fresh_def) |
837 |
783 |
838 quotient_definition |
784 quotient_definition |
839 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
785 "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts" |
840 as |
786 as |
841 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
787 "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts" |
842 |
|
843 lemma permute_trm5_lts: |
|
844 "pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)" |
|
845 "pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)" |
|
846 "pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)" |
|
847 "pi \<bullet> Lnil = Lnil" |
|
848 "pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)" |
|
849 by (lifting permute_rtrm5_permute_rlts.simps) |
|
850 |
788 |
851 lemma trm5_lts_zero: |
789 lemma trm5_lts_zero: |
852 "0 \<bullet> (x\<Colon>trm5) = x" |
790 "0 \<bullet> (x\<Colon>trm5) = x" |
853 "0 \<bullet> (y\<Colon>lts) = y" |
791 "0 \<bullet> (y\<Colon>lts) = y" |
854 sorry |
792 apply(induct x and y rule: trm5_lts_inducts) |
|
793 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
794 done |
855 |
795 |
856 lemma trm5_lts_plus: |
796 lemma trm5_lts_plus: |
857 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
797 "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x" |
858 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
798 "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y" |
859 sorry |
799 apply(induct x and y rule: trm5_lts_inducts) |
|
800 apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) |
|
801 done |
860 |
802 |
861 instance |
803 instance |
862 apply default |
804 apply default |
863 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
805 apply (simp_all add: trm5_lts_zero trm5_lts_plus) |
864 done |
806 done |
865 |
807 |
866 end |
808 end |
867 |
809 |
868 lemma alpha5_INJ: |
810 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] |
869 "((Vr5 a) = (Vr5 b)) = (a = b)" |
811 |
870 "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)" |
812 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
871 "(Lt5 l1 t1 = Lt5 l2 t2) = |
813 |
872 ((\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2))) \<and> |
814 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
873 (\<exists>pi. ((bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2))))" |
815 |
874 "Lnil = Lnil" |
816 lemmas fv_trm5_lts[simp] = rfv_trm5_rfv_lts.simps[quot_lifted] |
875 "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (n1 = n2 \<and> ls1 = ls2 \<and> t1 = t2)" |
|
876 unfolding alpha_gen |
|
877 apply(lifting alpha5_inj[unfolded alpha_gen]) |
|
878 done |
|
879 |
|
880 lemma bv5[simp]: |
|
881 "bv5 Lnil = {}" |
|
882 "bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl" |
|
883 by (lifting rbv5.simps) |
|
884 |
|
885 lemma fv_trm5_lts[simp]: |
|
886 "fv_trm5 (Vr5 n) = {atom n}" |
|
887 "fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s" |
|
888 "fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)" |
|
889 "fv_lts Lnil = {}" |
|
890 "fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl" |
|
891 by (lifting rfv_trm5_rfv_lts.simps) |
|
892 |
817 |
893 lemma lets_ok: |
818 lemma lets_ok: |
894 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
819 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
895 apply (subst alpha5_INJ) |
820 apply (subst alpha5_INJ) |
896 apply (rule conjI) |
821 apply (rule conjI) |