100 thm core_haskell.eq_iff |
100 thm core_haskell.eq_iff |
101 thm core_haskell.fv_bn_eqvt |
101 thm core_haskell.fv_bn_eqvt |
102 thm core_haskell.size_eqvt |
102 thm core_haskell.size_eqvt |
103 thm core_haskell.supp |
103 thm core_haskell.supp |
104 |
104 |
105 (* |
|
106 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
|
107 unfolding fresh_star_def Ball_def |
|
108 by auto (simp_all add: fresh_minus_perm) |
|
109 |
|
110 primrec permute_bv_vs_raw |
|
111 where "permute_bv_vs_raw p VsNil_raw = VsNil_raw" |
|
112 | "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)" |
|
113 primrec permute_bv_cvs_raw |
|
114 where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw" |
|
115 | "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)" |
|
116 primrec permute_bv_tvs_raw |
|
117 where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw" |
|
118 | "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)" |
|
119 primrec permute_bv_raw |
|
120 where "permute_bv_raw p (Kpat_raw c l1 l2 l3) = |
|
121 Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)" |
|
122 |
|
123 quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars" |
|
124 is "permute_bv_vs_raw" |
|
125 quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars" |
|
126 is "permute_bv_cvs_raw" |
|
127 quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars" |
|
128 is "permute_bv_tvs_raw" |
|
129 quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat" |
|
130 is "permute_bv_raw" |
|
131 |
|
132 lemma rsp_pre: |
|
133 "alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" |
|
134 "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" |
|
135 "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)" |
|
136 apply (erule_tac [!] alpha_inducts) |
|
137 apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps) |
|
138 done |
|
139 |
|
140 lemma [quot_respect]: |
|
141 "(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw" |
|
142 "(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw" |
|
143 "(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw" |
|
144 "(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw" |
|
145 apply (simp_all add: rsp_pre) |
|
146 apply clarify |
|
147 apply (erule_tac alpha_inducts) |
|
148 apply (simp_all) |
|
149 apply (rule alpha_intros) |
|
150 apply (simp_all add: rsp_pre) |
|
151 done |
|
152 |
|
153 thm permute_bv_raw.simps[no_vars] |
|
154 permute_bv_vs_raw.simps[quot_lifted] |
|
155 permute_bv_cvs_raw.simps[quot_lifted] |
|
156 permute_bv_tvs_raw.simps[quot_lifted] |
|
157 |
|
158 lemma permute_bv_pre: |
|
159 "permute_bv p (Kpat c l1 l2 l3) = |
|
160 Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)" |
|
161 by (lifting permute_bv_raw.simps) |
|
162 |
|
163 lemmas permute_bv[simp] = |
|
164 permute_bv_pre |
|
165 permute_bv_vs_raw.simps[quot_lifted] |
|
166 permute_bv_cvs_raw.simps[quot_lifted] |
|
167 permute_bv_tvs_raw.simps[quot_lifted] |
|
168 |
|
169 lemma perm_bv1: |
|
170 "p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)" |
|
171 "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)" |
|
172 "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)" |
|
173 apply(induct b rule: inducts(12)) |
|
174 apply(simp_all add:permute_bv eqvts) |
|
175 apply(induct c rule: inducts(11)) |
|
176 apply(simp_all add:permute_bv eqvts) |
|
177 apply(induct d rule: inducts(10)) |
|
178 apply(simp_all add:permute_bv eqvts) |
|
179 done |
|
180 |
|
181 lemma perm_bv2: |
|
182 "p \<bullet> bv l = bv (permute_bv p l)" |
|
183 apply(induct l rule: inducts(9)) |
|
184 apply(simp_all add:permute_bv) |
|
185 apply(simp add: perm_bv1[symmetric]) |
|
186 apply(simp add: eqvts) |
|
187 done |
|
188 |
|
189 lemma alpha_perm_bn1: |
|
190 "alpha_bv_tvs tvars (permute_bv_tvs q tvars)" |
|
191 "alpha_bv_cvs cvars (permute_bv_cvs q cvars)" |
|
192 "alpha_bv_vs vars (permute_bv_vs q vars)" |
|
193 apply(induct tvars rule: inducts(11)) |
|
194 apply(simp_all add:permute_bv eqvts eq_iff) |
|
195 apply(induct cvars rule: inducts(12)) |
|
196 apply(simp_all add:permute_bv eqvts eq_iff) |
|
197 apply(induct vars rule: inducts(10)) |
|
198 apply(simp_all add:permute_bv eqvts eq_iff) |
|
199 done |
|
200 |
|
201 lemma alpha_perm_bn: |
|
202 "alpha_bv pt (permute_bv q pt)" |
|
203 apply(induct pt rule: inducts(9)) |
|
204 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
|
205 done |
|
206 |
|
207 lemma ACons_subst: |
|
208 "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al" |
|
209 apply (simp only: eq_iff) |
|
210 apply (simp add: alpha_perm_bn) |
|
211 apply (rule_tac x="q" in exI) |
|
212 apply (simp add: alphas) |
|
213 apply (simp add: perm_bv2[symmetric]) |
|
214 apply (simp add: supp_abs) |
|
215 apply (simp add: fv_supp) |
|
216 apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
217 apply (rule supp_perm_eq[symmetric]) |
|
218 apply (subst supp_finite_atom_set) |
|
219 apply (rule finite_Diff) |
|
220 apply (simp add: finite_supp) |
|
221 apply (assumption) |
|
222 done |
|
223 |
|
224 lemma permute_bv_zero1: |
|
225 "permute_bv_cvs 0 b = b" |
|
226 "permute_bv_tvs 0 c = c" |
|
227 "permute_bv_vs 0 d = d" |
|
228 apply(induct b rule: inducts(12)) |
|
229 apply(simp_all add:permute_bv eqvts) |
|
230 apply(induct c rule: inducts(11)) |
|
231 apply(simp_all add:permute_bv eqvts) |
|
232 apply(induct d rule: inducts(10)) |
|
233 apply(simp_all add:permute_bv eqvts) |
|
234 done |
|
235 |
|
236 lemma permute_bv_zero2: |
|
237 "permute_bv 0 a = a" |
|
238 apply(induct a rule: inducts(9)) |
|
239 apply(simp_all add:permute_bv eqvts permute_bv_zero1) |
|
240 done |
|
241 |
|
242 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x" |
|
243 apply (induct x rule: inducts(11)) |
|
244 apply (simp_all add: eq_iff fresh_star_union) |
|
245 done |
|
246 |
|
247 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x" |
|
248 apply (induct x rule: inducts(12)) |
|
249 apply (rule TrueI)+ |
|
250 apply (simp_all add: eq_iff fresh_star_union) |
|
251 apply (subst supp_perm_eq) |
|
252 apply (simp_all add: fv_supp) |
|
253 done |
|
254 |
|
255 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x" |
|
256 apply (induct x rule: inducts(10)) |
|
257 apply (rule TrueI)+ |
|
258 apply (simp_all add: fresh_star_union eq_iff) |
|
259 apply (subst supp_perm_eq) |
|
260 apply (simp_all add: fv_supp) |
|
261 done |
|
262 |
|
263 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x" |
|
264 apply (induct x rule: inducts(9)) |
|
265 apply (rule TrueI)+ |
|
266 apply (simp_all add: eq_iff fresh_star_union) |
|
267 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) |
|
268 apply (subst supp_perm_eq) |
|
269 apply (simp_all add: fv_supp) |
|
270 done |
|
271 |
|
272 lemma fin1: "finite (fv_bv_tvs x)" |
|
273 apply (induct x rule: inducts(11)) |
|
274 apply (simp_all add: fv_supp finite_supp) |
|
275 done |
|
276 |
|
277 lemma fin2: "finite (fv_bv_cvs x)" |
|
278 apply (induct x rule: inducts(12)) |
|
279 apply (simp_all add: fv_supp finite_supp) |
|
280 done |
|
281 |
|
282 lemma fin3: "finite (fv_bv_vs x)" |
|
283 apply (induct x rule: inducts(10)) |
|
284 apply (simp_all add: fv_supp finite_supp) |
|
285 done |
|
286 |
|
287 lemma fin_fv_bv: "finite (fv_bv x)" |
|
288 apply (induct x rule: inducts(9)) |
|
289 apply (rule TrueI)+ |
|
290 defer |
|
291 apply (rule TrueI)+ |
|
292 apply (simp add: fin1 fin2 fin3) |
|
293 apply (rule finite_supp) |
|
294 done |
|
295 |
|
296 lemma finb1: "finite (set (bv_tvs x))" |
|
297 apply (induct x rule: inducts(11)) |
|
298 apply (simp_all add: fv_supp finite_supp) |
|
299 done |
|
300 |
|
301 lemma finb2: "finite (set (bv_cvs x))" |
|
302 apply (induct x rule: inducts(12)) |
|
303 apply (simp_all add: fv_supp finite_supp) |
|
304 done |
|
305 |
|
306 lemma finb3: "finite (set (bv_vs x))" |
|
307 apply (induct x rule: inducts(10)) |
|
308 apply (simp_all add: fv_supp finite_supp) |
|
309 done |
|
310 |
|
311 lemma fin_bv: "finite (set (bv x))" |
|
312 apply (induct x rule: inducts(9)) |
|
313 apply (simp_all add: finb1 finb2 finb3) |
|
314 done |
|
315 |
|
316 lemma strong_induction_principle: |
105 lemma strong_induction_principle: |
|
106 fixes c::"'a::fs" |
317 assumes a01: "\<And>b. P1 b KStar" |
107 assumes a01: "\<And>b. P1 b KStar" |
318 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
108 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
319 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
109 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
320 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
110 and a04: "\<And>tvar b. P3 b (TVar tvar)" |
321 and a05: "\<And>string b. P3 b (TC string)" |
111 and a05: "\<And>string b. P3 b (TC string)" |
370 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
160 and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk> |
371 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
161 \<Longrightarrow> P11 b (TvsCons tvar tkind tvars)" |
372 and a44: "\<And>b. P12 b CvsNil" |
162 and a44: "\<And>b. P12 b CvsNil" |
373 and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk> |
163 and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk> |
374 \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)" |
164 \<Longrightarrow> P12 b (CvsCons tvar ckind cvars)" |
375 shows "P1 (a :: 'a :: pt) tkind \<and> |
165 shows "P1 c tkind" |
376 P2 (b :: 'b :: pt) ckind \<and> |
166 "P2 c ckind" |
377 P3 (c :: 'c :: {pt,fs}) ty \<and> |
167 "P3 c ty" |
378 P4 (d :: 'd :: pt) ty_lst \<and> |
168 "P4 c ty_lst" |
379 P5 (e :: 'e :: {pt,fs}) co \<and> |
169 "P5 c co" |
380 P6 (f :: 'f :: pt) co_lst \<and> |
170 "P6 c co_lst" |
381 P7 (g :: 'g :: {pt,fs}) trm \<and> |
171 "P7 c trm" |
382 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
172 "P8 c assoc_lst" |
383 P9 (i :: 'i :: pt) pt \<and> |
173 "P9 c pt" |
384 P10 (j :: 'j :: pt) vars \<and> |
174 "P10 c vars" |
385 P11 (k :: 'k :: pt) tvars \<and> |
175 "P11 c tvars" |
386 P12 (l :: 'l :: pt) cvars" |
176 "P12 c cvars" |
387 proof - |
177 oops |
388 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)))" |
|
389 apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts) |
|
390 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
|
391 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
|
392 |
|
393 --"GOAL1" |
|
394 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
|
395 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
|
396 apply clarify |
|
397 apply (simp only: perm) |
|
398 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
|
399 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
|
400 apply (simp add: eq_iff) |
|
401 apply (rule_tac x="-pa" in exI) |
|
402 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
403 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
404 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
405 apply (simp add: eqvts) |
|
406 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
407 apply (rule conjI) |
|
408 apply (rule supp_perm_eq) |
|
409 apply (simp add: eqvts) |
|
410 apply (subst supp_finite_atom_set) |
|
411 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
412 apply (simp add: eqvts) |
|
413 apply (subst supp_perm_eq) |
|
414 apply (subst supp_finite_atom_set) |
|
415 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
416 apply assumption |
|
417 apply (simp add: fresh_star_minus_perm) |
|
418 apply (rule a08) |
|
419 apply simp |
|
420 apply(rotate_tac 1) |
|
421 apply(erule_tac x="(pa + p)" in allE) |
|
422 apply simp |
|
423 apply (simp add: eqvts eqvts_raw) |
|
424 apply (rule at_set_avoiding2_atom) |
|
425 apply (simp add: finite_supp) |
|
426 apply (simp add: finite_supp) |
|
427 apply (simp add: fresh_def) |
|
428 apply (simp only: supp_abs eqvts) |
|
429 apply blast |
|
430 |
|
431 --"GOAL2" |
|
432 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and> |
|
433 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)") |
|
434 apply clarify |
|
435 apply (simp only: perm) |
|
436 apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)" |
|
437 and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
|
438 apply (simp add: eq_iff) |
|
439 apply (rule_tac x="-pa" in exI) |
|
440 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
441 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
|
442 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
|
443 apply (simp add: eqvts) |
|
444 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
445 apply (rule conjI) |
|
446 apply (rule supp_perm_eq) |
|
447 apply (simp add: eqvts) |
|
448 apply (subst supp_finite_atom_set) |
|
449 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
450 apply (simp add: eqvts) |
|
451 apply (subst supp_perm_eq) |
|
452 apply (subst supp_finite_atom_set) |
|
453 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
454 apply assumption |
|
455 apply (simp add: fresh_star_minus_perm) |
|
456 apply (rule a15) |
|
457 apply simp |
|
458 apply(rotate_tac 1) |
|
459 apply(erule_tac x="(pa + p)" in allE) |
|
460 apply simp |
|
461 apply (simp add: eqvts eqvts_raw) |
|
462 apply (rule at_set_avoiding2_atom) |
|
463 apply (simp add: finite_supp) |
|
464 apply (simp add: finite_supp) |
|
465 apply (simp add: fresh_def) |
|
466 apply (simp only: supp_abs eqvts) |
|
467 apply blast |
|
468 |
|
469 |
|
470 --"GOAL3 a copy-and-paste of Goal2 with consts and variable names changed" |
|
471 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
|
472 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
|
473 apply clarify |
|
474 apply (simp only: perm) |
|
475 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
|
476 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
|
477 apply (simp add: eq_iff) |
|
478 apply (rule_tac x="-pa" in exI) |
|
479 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
480 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
481 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
|
482 apply (simp add: eqvts) |
|
483 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
484 apply (rule conjI) |
|
485 apply (rule supp_perm_eq) |
|
486 apply (simp add: eqvts) |
|
487 apply (subst supp_finite_atom_set) |
|
488 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
489 apply (simp add: eqvts) |
|
490 apply (subst supp_perm_eq) |
|
491 apply (subst supp_finite_atom_set) |
|
492 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
493 apply assumption |
|
494 apply (simp add: fresh_star_minus_perm) |
|
495 apply (rule a29) |
|
496 apply simp |
|
497 apply(rotate_tac 1) |
|
498 apply(erule_tac x="(pa + p)" in allE) |
|
499 apply simp |
|
500 apply (simp add: eqvts eqvts_raw) |
|
501 apply (rule at_set_avoiding2_atom) |
|
502 apply (simp add: finite_supp) |
|
503 apply (simp add: finite_supp) |
|
504 apply (simp add: fresh_def) |
|
505 apply (simp only: supp_abs eqvts) |
|
506 apply blast |
|
507 |
|
508 --"GOAL4 a copy-and-paste" |
|
509 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and> |
|
510 supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)") |
|
511 apply clarify |
|
512 apply (simp only: perm) |
|
513 apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)" |
|
514 and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst) |
|
515 apply (simp add: eq_iff) |
|
516 apply (rule_tac x="-pa" in exI) |
|
517 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
518 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
|
519 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
|
520 apply (simp add: eqvts) |
|
521 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
522 apply (rule conjI) |
|
523 apply (rule supp_perm_eq) |
|
524 apply (simp add: eqvts) |
|
525 apply (subst supp_finite_atom_set) |
|
526 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
527 apply (simp add: eqvts) |
|
528 apply (subst supp_perm_eq) |
|
529 apply (subst supp_finite_atom_set) |
|
530 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
531 apply assumption |
|
532 apply (simp add: fresh_star_minus_perm) |
|
533 apply (rule a30) |
|
534 apply simp |
|
535 apply(rotate_tac 1) |
|
536 apply(erule_tac x="(pa + p)" in allE) |
|
537 apply simp |
|
538 apply (simp add: eqvts eqvts_raw) |
|
539 apply (rule at_set_avoiding2_atom) |
|
540 apply (simp add: finite_supp) |
|
541 apply (simp add: finite_supp) |
|
542 apply (simp add: fresh_def) |
|
543 apply (simp only: supp_abs eqvts) |
|
544 apply blast |
|
545 |
|
546 |
|
547 --"GOAL5 a copy-and-paste" |
|
548 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
|
549 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)") |
|
550 apply clarify |
|
551 apply (simp only: perm) |
|
552 apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)" |
|
553 and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst) |
|
554 apply (simp add: eq_iff) |
|
555 apply (rule_tac x="-pa" in exI) |
|
556 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
557 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
|
558 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
|
559 apply (simp add: eqvts) |
|
560 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
561 apply (rule conjI) |
|
562 apply (rule supp_perm_eq) |
|
563 apply (simp add: eqvts) |
|
564 apply (subst supp_finite_atom_set) |
|
565 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
566 apply (simp add: eqvts) |
|
567 apply (subst supp_perm_eq) |
|
568 apply (subst supp_finite_atom_set) |
|
569 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
570 apply assumption |
|
571 apply (simp add: fresh_star_minus_perm) |
|
572 apply (rule a32) |
|
573 apply simp |
|
574 apply(rotate_tac 1) |
|
575 apply(erule_tac x="(pa + p)" in allE) |
|
576 apply simp |
|
577 apply (simp add: eqvts eqvts_raw) |
|
578 apply (rule at_set_avoiding2_atom) |
|
579 apply (simp add: finite_supp) |
|
580 apply (simp add: finite_supp) |
|
581 apply (simp add: fresh_def) |
|
582 apply (simp only: supp_abs eqvts) |
|
583 apply blast |
|
584 |
|
585 |
|
586 --"GOAL6 a copy-and-paste" |
|
587 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and> |
|
588 supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)") |
|
589 apply clarify |
|
590 apply (simp only: perm) |
|
591 apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)" |
|
592 and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst) |
|
593 apply (simp add: eq_iff) |
|
594 apply (rule_tac x="-pa" in exI) |
|
595 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
|
596 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
|
597 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
|
598 apply (simp add: eqvts) |
|
599 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
|
600 apply (rule conjI) |
|
601 apply (rule supp_perm_eq) |
|
602 apply (simp add: eqvts) |
|
603 apply (subst supp_finite_atom_set) |
|
604 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
605 apply (simp add: eqvts) |
|
606 apply (subst supp_perm_eq) |
|
607 apply (subst supp_finite_atom_set) |
|
608 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
|
609 apply assumption |
|
610 apply (simp add: fresh_star_minus_perm) |
|
611 apply (rule a34) |
|
612 apply simp |
|
613 apply simp |
|
614 apply(rotate_tac 2) |
|
615 apply(erule_tac x="(pa + p)" in allE) |
|
616 apply simp |
|
617 apply (simp add: eqvts eqvts_raw) |
|
618 apply (rule at_set_avoiding2_atom) |
|
619 apply (simp add: finite_supp) |
|
620 apply (simp add: finite_supp) |
|
621 apply (simp add: fresh_def) |
|
622 apply (simp only: supp_abs eqvts) |
|
623 apply blast |
|
624 |
|
625 --"MAIN ACons Goal" |
|
626 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and> |
|
627 supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)") |
|
628 apply clarify |
|
629 apply (simp only: perm eqvts) |
|
630 apply (subst ACons_subst) |
|
631 apply assumption |
|
632 apply (rule a38) |
|
633 apply simp |
|
634 apply(rotate_tac 1) |
|
635 apply(erule_tac x="(pa + p)" in allE) |
|
636 apply simp |
|
637 apply simp |
|
638 apply (simp add: perm_bv2[symmetric]) |
|
639 apply (simp add: eqvts eqvts_raw) |
|
640 apply (rule at_set_avoiding2) |
|
641 apply (simp add: fin_bv) |
|
642 apply (simp add: finite_supp) |
|
643 apply (simp add: supp_abs) |
|
644 apply (simp add: finite_supp) |
|
645 apply (simp add: fresh_star_def fresh_def supp_abs eqvts) |
|
646 done |
|
647 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+) |
|
648 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+) |
|
649 ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2) |
|
650 qed |
|
651 *) |
|
652 |
|
653 section {* test about equivariance for alpha *} |
|
654 |
|
655 (* this should not be an equivariance rule *) |
|
656 (* for the moment, we force it to be *) |
|
657 |
|
658 (*declare permute_pure[eqvt]*) |
|
659 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *) |
|
660 |
|
661 thm eqvts |
|
662 thm eqvts_raw |
|
663 |
|
664 |
178 |
665 end |
179 end |
666 |
180 |