--- a/Nominal-General/Nominal2_Supp.thy	Sun Apr 18 18:01:22 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Mon Apr 19 09:25:31 2010 +0200
@@ -141,20 +141,38 @@
   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
   unfolding fresh_star_def fresh_def by blast
 
+lemma at_set_avoiding2:
+  assumes "finite xs"
+  and     "finite (supp c)" "finite (supp x)"
+  and     "xs \<sharp>* x"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
+
+lemma at_set_avoiding2_atom:
+  assumes "finite (supp c)" "finite (supp x)"
+  and     b: "xa \<sharp> x"
+  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
+  have c: "(p \<bullet> xa) \<sharp> c" using p1
+    unfolding fresh_star_def Ball_def 
+    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
+  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+  then show ?thesis by blast
+qed
 
 section {* The freshness lemma according to Andrew Pitts *}
 
-lemma fresh_conv_MOST: 
-  shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
-  unfolding fresh_def supp_def MOST_iff_cofinite by simp
-
-lemma fresh_apply:
-  assumes "a \<sharp> f" and "a \<sharp> x" 
-  shows "a \<sharp> f x"
-  using assms unfolding fresh_conv_MOST
-  unfolding permute_fun_app_eq [where f=f]
-  by (elim MOST_rev_mp, simp)
-
 lemma freshness_lemma:
   fixes h :: "'a::at \<Rightarrow> 'b::pt"
   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
@@ -173,7 +191,8 @@
     next
       assume "a \<noteq> b"
       hence "atom a \<sharp> b" by (simp add: fresh_at_base)
-      with a3 have "atom a \<sharp> h b" by (rule fresh_apply)
+      with a3 have "atom a \<sharp> h b" 
+	by (rule fresh_fun_app)
       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
         by (rule swap_fresh_fresh)
       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
@@ -358,7 +377,7 @@
   using not_fresh_nat_of [unfolded fresh_def] by auto
 
 
-section {* Support for sets of atoms *}
+section {* Support for finite sets of atoms *}
 
 lemma supp_finite_atom_set:
   fixes S::"atom set"
@@ -447,36 +466,4 @@
   qed
 qed
 
-section {* at_set_avoiding2 *}
-
-lemma at_set_avoiding2:
-  assumes "finite xs"
-  and     "finite (supp c)" "finite (supp x)"
-  and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
-using assms
-apply(erule_tac c="(c, x)" in at_set_avoiding)
-apply(simp add: supp_Pair)
-apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
-done
-
-lemma at_set_avoiding2_atom:
-  assumes "finite (supp c)" "finite (supp x)"
-  and     b: "xa \<sharp> x"
-  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
-proof -
-  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
-  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
-    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
-  have c: "(p \<bullet> xa) \<sharp> c" using p1
-    unfolding fresh_star_def Ball_def 
-    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
-  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
-  then show ?thesis by blast
-qed
-
 end