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> supp(p \<bullet> t)")

   430   apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")

   431   apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)

   433   apply (smt IntI image_iff inf_le1 permute_set_eq_image subsetD)

   432   apply (drule subsetD[OF supp_subst])

   434   apply (drule subsetD[OF supp_subst])

   433   apply auto[1]

   435   apply auto[1]

   434   apply (simp add: fresh_star_def fresh_def)

   436   apply (simp add: fresh_star_def fresh_def)

   435   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")

   437   apply (subgoal_tac "x \<in> supp(p \<bullet> t)")

   442   apply (rotate_tac 2)

   444   apply (rotate_tac 2)

   443   apply (subst (asm) fresh_star_permute_iff[symmetric])

   445   apply (subst (asm) fresh_star_permute_iff[symmetric])

   444   apply (simp add: fresh_star_def fresh_def)

   446   apply (simp add: fresh_star_def fresh_def)

   445   apply blast

   447   apply blast

   446   done

   448   done

   448 

   450 

   449 text {* Some Tests about Alpha-Equality *}

   451 text {* Some Tests about Alpha-Equality *}

   450 

   452 

   451 lemma

   453 lemma

   452   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"

   454   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"