240 P2 (b :: 'b :: pt) ckind \<and> |
240 P2 (b :: 'b :: pt) ckind \<and> |
241 P3 (c :: 'c :: {pt,fs}) ty \<and> |
241 P3 (c :: 'c :: {pt,fs}) ty \<and> |
242 P4 (d :: 'd :: pt) ty_lst \<and> |
242 P4 (d :: 'd :: pt) ty_lst \<and> |
243 P5 (e :: 'e :: {pt,fs}) co \<and> |
243 P5 (e :: 'e :: {pt,fs}) co \<and> |
244 P6 (f :: 'f :: pt) co_lst \<and> |
244 P6 (f :: 'f :: pt) co_lst \<and> |
245 P7 (g :: 'g :: pt) trm \<and> |
245 P7 (g :: 'g :: {pt,fs}) trm \<and> |
246 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
246 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
247 P9 (i :: 'i :: pt) pat \<and> |
247 P9 (i :: 'i :: pt) pat \<and> |
248 P10 (j :: 'j :: pt) vt_lst \<and> |
248 P10 (j :: 'j :: pt) vt_lst \<and> |
249 P11 (k :: 'k :: pt) tvtk_lst \<and> |
249 P11 (k :: 'k :: pt) tvtk_lst \<and> |
250 P12 (l :: 'l :: pt) tvck_lst" |
250 P12 (l :: 'l :: pt) tvck_lst" |
320 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
320 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
321 apply (simp add: eqvts) |
321 apply (simp add: eqvts) |
322 apply assumption |
322 apply assumption |
323 apply (simp add: fresh_star_minus_perm) |
323 apply (simp add: fresh_star_minus_perm) |
324 apply (rule a15) |
324 apply (rule a15) |
|
325 apply simp |
|
326 apply(rotate_tac 1) |
|
327 apply(erule_tac x="(pa + p)" in allE) |
|
328 apply simp |
|
329 apply (simp add: eqvts eqvts_raw) |
|
330 apply (rule at_set_avoiding2_atom) |
|
331 apply (simp add: finite_supp) |
|
332 apply (simp add: finite_supp) |
|
333 apply (simp add: fresh_def) |
|
334 apply (simp only: supp_Abs eqvts) |
|
335 apply blast |
|
336 |
|
337 |
|
338 (* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *) |
|
339 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and> |
|
340 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)") |
|
341 apply clarify |
|
342 apply (simp only: perm) |
|
343 apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)" |
|
344 and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst) |
|
345 apply (simp only: eq_iff) |
|
346 apply (rule_tac x="-pa" in exI) |
|
347 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
|
348 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
349 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
|
350 apply (simp add: eqvts) |
|
351 apply (simp add: eqvts[symmetric]) |
|
352 apply (rule conjI) |
|
353 apply (rule supp_perm_eq) |
|
354 apply (simp add: eqvts) |
|
355 apply (subst supp_finite_atom_set) |
|
356 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
357 apply (simp add: eqvts) |
|
358 apply (simp add: eqvts) |
|
359 apply (subst supp_perm_eq) |
|
360 apply (subst supp_finite_atom_set) |
|
361 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
362 apply (simp add: eqvts) |
|
363 apply assumption |
|
364 apply (simp add: fresh_star_minus_perm) |
|
365 apply (rule a29) |
325 apply simp |
366 apply simp |
326 apply(rotate_tac 1) |
367 apply(rotate_tac 1) |
327 apply(erule_tac x="(pa + p)" in allE) |
368 apply(erule_tac x="(pa + p)" in allE) |
328 apply simp |
369 apply simp |
329 apply (simp add: eqvts eqvts_raw) |
370 apply (simp add: eqvts eqvts_raw) |