69 | TVTKCons "tvar" "tkind" "tvtk_lst" |
69 | TVTKCons "tvar" "tkind" "tvtk_lst" |
70 and tvck_lst = |
70 and tvck_lst = |
71 TVCKNil |
71 TVCKNil |
72 | TVCKCons "tvar" "ckind" "tvck_lst" |
72 | TVCKCons "tvar" "ckind" "tvck_lst" |
73 binder |
73 binder |
74 bv :: "pat \<Rightarrow> atom set" |
74 bv :: "pat \<Rightarrow> atom list" |
75 and bv_vt :: "vt_lst \<Rightarrow> atom set" |
75 and bv_vt :: "vt_lst \<Rightarrow> atom list" |
76 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set" |
76 and bv_tvtk :: "tvtk_lst \<Rightarrow> atom list" |
77 and bv_tvck :: "tvck_lst \<Rightarrow> atom set" |
77 and bv_tvck :: "tvck_lst \<Rightarrow> atom list" |
78 where |
78 where |
79 "bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)" |
79 "bv (K s tvts tvcs vs) = append (bv_tvtk tvts) (append (bv_tvck tvcs) (bv_vt vs))" |
80 | "bv_vt VTNil = {}" |
80 | "bv_vt VTNil = []" |
81 | "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t" |
81 | "bv_vt (VTCons v k t) = (atom v) # bv_vt t" |
82 | "bv_tvtk TVTKNil = {}" |
82 | "bv_tvtk TVTKNil = []" |
83 | "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t" |
83 | "bv_tvtk (TVTKCons v k t) = (atom v) # bv_tvtk t" |
84 | "bv_tvck TVCKNil = {}" |
84 | "bv_tvck TVCKNil = []" |
85 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
85 | "bv_tvck (TVCKCons v k t) = (atom v) # bv_tvck t" |
86 |
86 |
87 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
87 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
88 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
88 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
89 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
89 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
90 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff |
90 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff |
199 apply(induct pat rule: inducts(9)) |
199 apply(induct pat rule: inducts(9)) |
200 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
200 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
201 done |
201 done |
202 |
202 |
203 lemma ACons_subst: |
203 lemma ACons_subst: |
204 "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
204 "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
205 apply (simp only: eq_iff) |
205 apply (simp only: eq_iff) |
206 apply (rule_tac x="q" in exI) |
206 apply (rule_tac x="q" in exI) |
207 apply (simp add: alphas) |
207 apply (simp add: alphas) |
208 apply (simp add: perm_bv2[symmetric]) |
208 apply (simp add: perm_bv2[symmetric]) |
209 apply (simp add: eqvts[symmetric]) |
209 apply (simp add: eqvts[symmetric]) |
293 apply (induct x rule: inducts(9)) |
293 apply (induct x rule: inducts(9)) |
294 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
294 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
295 apply (simp add: fin1 fin2 fin3) |
295 apply (simp add: fin1 fin2 fin3) |
296 done |
296 done |
297 |
297 |
298 lemma finb1: "finite (bv_tvtk x)" |
298 lemma finb1: "finite (set (bv_tvtk x))" |
299 apply (induct x rule: inducts(11)) |
299 apply (induct x rule: inducts(11)) |
300 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
300 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
301 apply (simp_all add: fv_supp finite_supp) |
301 apply (simp_all add: fv_supp finite_supp) |
302 done |
302 done |
303 |
303 |
304 lemma finb2: "finite (bv_tvck x)" |
304 lemma finb2: "finite (set (bv_tvck x))" |
305 apply (induct x rule: inducts(12)) |
305 apply (induct x rule: inducts(12)) |
306 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
306 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
307 apply (simp_all add: fv_supp finite_supp) |
307 apply (simp_all add: fv_supp finite_supp) |
308 done |
308 done |
309 |
309 |
310 lemma finb3: "finite (bv_vt x)" |
310 lemma finb3: "finite (set (bv_vt x))" |
311 apply (induct x rule: inducts(10)) |
311 apply (induct x rule: inducts(10)) |
312 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
312 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
313 apply (simp_all add: fv_supp finite_supp) |
313 apply (simp_all add: fv_supp finite_supp) |
314 done |
314 done |
315 |
315 |
316 lemma fin_bv: "finite (bv x)" |
316 lemma fin_bv: "finite (set (bv x))" |
317 apply (induct x rule: inducts(9)) |
317 apply (induct x rule: inducts(9)) |
318 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
318 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
319 apply (simp add: finb1 finb2 finb3) |
319 apply (simp add: finb1 finb2 finb3) |
320 done |
320 done |
321 |
|
322 lemma "bv x \<sharp>* fv_bv x" |
|
323 apply (induct x rule: inducts(9)) |
|
324 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
325 apply (simp) |
|
326 oops |
|
327 |
321 |
328 lemma strong_inudction_principle: |
322 lemma strong_inudction_principle: |
329 assumes a01: "\<And>b. P1 b KStar" |
323 assumes a01: "\<And>b. P1 b KStar" |
330 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
324 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
331 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
325 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
366 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> |
360 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> |
367 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
361 \<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
368 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)" |
362 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)" |
369 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
363 and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
370 and a37: "\<And>b. P8 b ANil" |
364 and a37: "\<And>b. P8 b ANil" |
371 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; bv(pat) \<sharp>* b\<rbrakk> |
365 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> |
372 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
366 \<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
373 and a39: "\<And>string tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk> |
367 and a39: "\<And>string tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk> |
374 \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)" |
368 \<Longrightarrow> P9 b (K string tvtk_lst tvck_lst vt_lst)" |
375 and a40: "\<And>b. P10 b VTNil" |
369 and a40: "\<And>b. P10 b VTNil" |
376 and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)" |
370 and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)" |
641 apply (simp add: fresh_def) |
635 apply (simp add: fresh_def) |
642 apply (simp only: supp_abs eqvts) |
636 apply (simp only: supp_abs eqvts) |
643 apply blast |
637 apply blast |
644 |
638 |
645 (* MAIN ACons Goal *) |
639 (* MAIN ACons Goal *) |
646 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and> |
640 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and> |
647 supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
641 supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
648 apply clarify |
642 apply clarify |
649 apply (simp only: perm eqvts) |
643 apply (simp only: perm eqvts) |
650 apply (subst ACons_subst) |
644 apply (subst ACons_subst) |
651 apply assumption |
645 apply assumption |
652 apply (rule a38) |
646 apply (rule a38) |
659 apply (simp add: eqvts eqvts_raw) |
653 apply (simp add: eqvts eqvts_raw) |
660 apply (rule at_set_avoiding2) |
654 apply (rule at_set_avoiding2) |
661 apply (simp add: fin_bv) |
655 apply (simp add: fin_bv) |
662 apply (simp add: finite_supp) |
656 apply (simp add: finite_supp) |
663 apply (simp add: supp_abs) |
657 apply (simp add: supp_abs) |
664 apply (rule finite_Diff) |
|
665 apply (simp add: finite_supp) |
658 apply (simp add: finite_supp) |
666 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
659 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
667 done |
660 done |
668 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+) |
661 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+) |
669 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+) |
662 moreover have "P9 i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vt 0 (0 \<bullet> vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \<bullet> tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \<bullet> tvck_lst))" using a1 a2 a3 a4 by (blast+) |