2827   and "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"

  2827   and "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"

  2828   unfolding fresh_def 

  2828   unfolding fresh_def 

  2829   apply(simp_all add: supp_at_base)

  2829   apply(simp_all add: supp_at_base)

  2830   apply(metis)

  2830   apply(metis)

  2831   done

  2831   done

  2834   fixes b::"'a::at_base"

  2841   fixes b::"'a::at_base"

  2835   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"

  2842   shows "a \<sharp> atom b \<longleftrightarrow> a \<sharp> b"

  2836   by (simp add: fresh_def supp_at_base supp_atom)

  2843   by (simp add: fresh_def supp_at_base supp_atom)

  2837 

  2844 

  2838 lemma fresh_star_atom_at_base: 

  2845 lemma fresh_star_atom_at_base: 

  2842 

  2849 

  2843 lemma if_fresh_at_base [simp]:

  2850 lemma if_fresh_at_base [simp]:

  2844   shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s"

  2851   shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s"

  2845   and   "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s"

  2852   and   "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s"

  2846 by (simp_all add: fresh_at_base)

  2853 by (simp_all add: fresh_at_base)

  2847 

  2855 

  2848 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>

  2856 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm =>

  2849   let

  2857   let

  2850     fun first_is_neg lhs rhs [] = NONE

  2858     fun first_is_neg lhs rhs [] = NONE

  2851       | first_is_neg lhs rhs (thm::thms) =

  2859       | first_is_neg lhs rhs (thm::thms) =