82 | "bv_vs VsNil = []" |
82 | "bv_vs VsNil = []" |
83 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
83 | "bv_vs (VsCons v k t) = (atom v) # bv_vs t" |
84 | "bv_tvs TvsNil = []" |
84 | "bv_tvs TvsNil = []" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
86 | "bv_cvs CvsNil = []" |
86 | "bv_cvs CvsNil = []" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
88 |
88 |
89 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
89 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
90 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
90 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
91 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
91 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
92 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
92 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff |
189 apply(induct vars rule: inducts(10)) |
189 apply(induct vars rule: inducts(10)) |
190 apply(simp_all add:permute_bv eqvts eq_iff) |
190 apply(simp_all add:permute_bv eqvts eq_iff) |
191 done |
191 done |
192 |
192 |
193 lemma alpha_perm_bn: |
193 lemma alpha_perm_bn: |
194 "alpha_bv pat (permute_bv q pat)" |
194 "alpha_bv pt (permute_bv q pt)" |
195 apply(induct pat rule: inducts(9)) |
195 apply(induct pt rule: inducts(9)) |
196 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
196 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
197 done |
197 done |
198 |
198 |
199 lemma ACons_subst: |
199 lemma ACons_subst: |
200 "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
200 "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al" |
201 apply (simp only: eq_iff) |
201 apply (simp only: eq_iff) |
202 apply (simp add: alpha_perm_bn) |
202 apply (simp add: alpha_perm_bn) |
203 apply (rule_tac x="q" in exI) |
203 apply (rule_tac x="q" in exI) |
204 apply (simp add: alphas) |
204 apply (simp add: alphas) |
205 apply (simp add: perm_bv2[symmetric]) |
205 apply (simp add: perm_bv2[symmetric]) |
350 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
350 and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk> |
351 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
351 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
352 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
352 and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
353 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
353 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
354 and a37: "\<And>b. P8 b ANil" |
354 and a37: "\<And>b. P8 b ANil" |
355 and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk> |
355 and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk> |
356 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
356 \<Longrightarrow> P8 b (ACons pt trm assoc_lst)" |
357 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
357 and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk> |
358 \<Longrightarrow> P9 b (Kpat string tvars cvars vars)" |
358 \<Longrightarrow> P9 b (Kpat string tvars cvars vars)" |
359 and a40: "\<And>b. P10 b VsNil" |
359 and a40: "\<And>b. P10 b VsNil" |
360 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
360 and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)" |
361 and a42: "\<And>b. P11 b TvsNil" |
361 and a42: "\<And>b. P11 b TvsNil" |
370 P4 (d :: 'd :: pt) ty_lst \<and> |
370 P4 (d :: 'd :: pt) ty_lst \<and> |
371 P5 (e :: 'e :: {pt,fs}) co \<and> |
371 P5 (e :: 'e :: {pt,fs}) co \<and> |
372 P6 (f :: 'f :: pt) co_lst \<and> |
372 P6 (f :: 'f :: pt) co_lst \<and> |
373 P7 (g :: 'g :: {pt,fs}) trm \<and> |
373 P7 (g :: 'g :: {pt,fs}) trm \<and> |
374 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
374 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
375 P9 (i :: 'i :: pt) pat \<and> |
375 P9 (i :: 'i :: pt) pt \<and> |
376 P10 (j :: 'j :: pt) vars \<and> |
376 P10 (j :: 'j :: pt) vars \<and> |
377 P11 (k :: 'k :: pt) tvars \<and> |
377 P11 (k :: 'k :: pt) tvars \<and> |
378 P12 (l :: 'l :: pt) cvars" |
378 P12 (l :: 'l :: pt) cvars" |
379 proof - |
379 proof - |
380 have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))" |
380 have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))" |
381 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
381 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
382 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
382 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
383 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
383 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
384 |
384 |
385 (* GOAL1 *) |
385 (* GOAL1 *) |
635 apply (simp add: supp_abs) |
635 apply (simp add: supp_abs) |
636 apply (simp add: finite_supp) |
636 apply (simp add: finite_supp) |
637 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
637 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
638 done |
638 done |
639 then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+) |
639 then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+) |
640 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+) |
640 moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+) |
641 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
641 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
642 qed |
642 qed |
643 |
643 |
644 section {* test about equivariance for alpha *} |
644 section {* test about equivariance for alpha *} |
645 |
645 |