425 apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'") |
425 apply (subgoal_tac "(atom ` fset xs \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* \<theta>'") |
426 apply (metis Diff_partition fresh_star_Un) |
426 apply (metis Diff_partition fresh_star_Un) |
427 apply (simp add: fresh_star_Un fresh_star_inter1) |
427 apply (simp add: fresh_star_Un fresh_star_inter1) |
428 apply (simp add: alphas fresh_star_zero) |
428 apply (simp add: alphas fresh_star_zero) |
429 apply auto[1] |
429 apply auto[1] |
|
430 apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
|
431 apply (simp add: inter_eqvt) |
|
432 apply blast |
430 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
433 apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)") |
431 oops |
434 apply (simp add: IntI image_eqI) |
432 (* |
|
433 apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD) |
|
434 apply (drule subsetD[OF supp_subst]) |
435 apply (drule subsetD[OF supp_subst]) |
435 apply auto[1] |
|
436 apply (simp add: fresh_star_def fresh_def) |
436 apply (simp add: fresh_star_def fresh_def) |
|
437 apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)") |
|
438 apply (simp add: ) |
437 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
439 apply (subgoal_tac "x \<in> supp(p \<bullet> t)") |
438 apply (smt IntI inf_le1 inter_eqvt subsetD supp_eqvt) |
440 apply (metis inf1I inter_eqvt mem_def supp_eqvt ) |
439 apply (rotate_tac 6) |
441 apply (rotate_tac 6) |
440 apply (drule sym) |
442 apply (drule sym) |
441 apply (simp add: subst_eqvt) |
443 apply (simp add: subst_eqvt) |
442 apply (drule subsetD[OF supp_subst]) |
444 apply (drule subsetD[OF supp_subst]) |
443 apply auto[1] |
445 apply auto[1] |
444 apply (rotate_tac 2) |
446 apply (rotate_tac 2) |
445 apply (subst (asm) fresh_star_permute_iff[symmetric]) |
447 apply (subst (asm) fresh_star_permute_iff[symmetric]) |
446 apply (simp add: fresh_star_def fresh_def) |
448 apply (simp add: fresh_star_def fresh_def) |
447 apply blast |
449 apply blast |
448 done |
450 done |
449 *) |
451 |
450 |
452 |
451 text {* Some Tests about Alpha-Equality *} |
453 text {* Some Tests about Alpha-Equality *} |
452 |
454 |
453 lemma |
455 lemma |
454 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
456 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |