85 | "bv_tvck TVCKNil = {}" |
85 | "bv_tvck TVCKNil = {}" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
87 |
87 |
88 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 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) |
89 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 supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
|
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
|
91 |
|
92 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
|
93 unfolding fresh_star_def Ball_def |
|
94 by auto (simp_all add: fresh_minus_perm) |
90 |
95 |
91 lemma |
96 lemma |
92 assumes a01: "\<And>b. P1 b KStar" |
97 assumes a01: "\<And>b. P1 b KStar" |
93 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
98 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
94 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
99 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
143 and a44: "\<And>b. P12 b TVCKNil" |
148 and a44: "\<And>b. P12 b TVCKNil" |
144 and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk> |
149 and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk> |
145 \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)" |
150 \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)" |
146 shows "P1 (a :: 'a :: pt) tkind \<and> |
151 shows "P1 (a :: 'a :: pt) tkind \<and> |
147 P2 (b :: 'b :: pt) ckind \<and> |
152 P2 (b :: 'b :: pt) ckind \<and> |
148 P3 (c :: 'c :: pt) ty \<and> |
153 P3 (c :: 'c :: {pt,fs}) ty \<and> |
149 P4 (d :: 'd :: pt) ty_lst \<and> |
154 P4 (d :: 'd :: pt) ty_lst \<and> |
150 P5 (e :: 'e :: pt) co \<and> |
155 P5 (e :: 'e :: pt) co \<and> |
151 P6 (f :: 'f :: pt) co_lst \<and> |
156 P6 (f :: 'f :: pt) co_lst \<and> |
152 P7 (g :: 'g :: pt) trm \<and> |
157 P7 (g :: 'g :: pt) trm \<and> |
153 P8 (h :: 'h :: pt) assoc_lst \<and> |
158 P8 (h :: 'h :: pt) assoc_lst \<and> |
158 proof - |
163 proof - |
159 have a: "(\<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> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
164 have a: "(\<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> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
160 apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
165 apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
161 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
166 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
162 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
167 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
|
168 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
|
169 prefer 2 |
|
170 apply (rule at_set_avoiding2_atom) |
|
171 apply (simp add: finite_supp) |
|
172 apply (simp add: finite_supp) |
|
173 apply (simp add: fresh_def) |
|
174 apply (simp only: supp_Abs eqvts) |
|
175 apply blast |
|
176 apply clarify |
|
177 apply (simp only: perm) |
|
178 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
|
179 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff) |
|
180 apply (rule_tac x="-pa" in exI) |
|
181 apply (simp add: alphas) |
|
182 prefer 2 |
|
183 apply (rule a08) |
|
184 apply simp |
|
185 apply(rotate_tac 1) |
|
186 apply(erule_tac x="(pa + p)" in allE) |
|
187 apply simp |
|
188 apply (simp add: eqvts eqvts_raw) |
|
189 apply (simp add: eqvts eqvts_raw supp_Abs) |
|
190 apply (rule conjI) |
|
191 apply (simp add: eqvts[symmetric]) |
|
192 apply (simp add: fv_supp) |
|
193 apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}" |
|
194 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
195 apply (simp add: eqvts) |
|
196 apply (rule supp_perm_eq) |
|
197 apply (simp add: eqvts) |
|
198 apply (subst supp_finite_atom_set) |
|
199 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
200 apply (simp add: eqvts) |
|
201 apply (simp add: eqvts) |
|
202 apply (simp add: fv_supp) |
|
203 apply (simp add: eqvts[symmetric]) |
|
204 apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}" |
|
205 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
206 apply (simp add: eqvts) |
|
207 apply (subst supp_perm_eq) |
|
208 apply (subst supp_finite_atom_set) |
|
209 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
210 apply (simp add: eqvts) |
|
211 apply assumption |
|
212 apply (simp add: fresh_star_minus_perm) |
163 sorry |
213 sorry |
|
214 |
164 have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
215 have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
165 have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
216 have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
166 have g3: "P3 c (0 \<bullet> ty) \<and> |
217 have g3: "P3 c (0 \<bullet> ty) \<and> |
167 P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
218 P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
168 P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |
219 P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |