--- a/Nominal/Nominal2_Base.thy	Mon Jan 10 08:51:51 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Jan 10 11:36:55 2011 +0000
@@ -952,18 +952,6 @@
 instance atom :: fs
 by default (simp add: supp_atom)
 
-section {* Support for finite sets of atoms *}
-
-lemma supp_finite_atom_set:
-  fixes S::"atom set"
-  assumes "finite S"
-  shows "supp S = S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(simp add: swap_set_not_in)
-  apply(rule assms)
-  apply(simp add: swap_set_in)
-done
 
 section {* Type @{typ perm} is finitely-supported. *}
 
@@ -1266,6 +1254,27 @@
 
 section {* Support of Finite Sets of Finitely Supported Elements *}
 
+text {* support and freshness for atom sets *}
+
+lemma supp_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(simp add: swap_set_not_in)
+  apply(rule assms)
+  apply(simp add: swap_set_in)
+done
+
+lemma fresh_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "a \<sharp> S \<longleftrightarrow> a \<notin> S"
+  unfolding fresh_def
+  by (simp add: supp_finite_atom_set[OF assms])
+
+
 lemma Union_fresh:
   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
   unfolding Union_image_eq[symmetric]
@@ -1977,6 +1986,18 @@
 apply(auto)
 done
 
+lemma fresh_finite_set_at_base:
+  fixes a::"'a::at_base"
+  assumes a: "finite S"
+  shows "atom a \<sharp> S \<longleftrightarrow> a \<notin> S"
+  unfolding fresh_def
+  apply(simp add: supp_finite_set_at_base[OF a])
+  apply(subst inj_image_mem_iff)
+  apply(simp add: inj_on_def)
+  apply(simp)
+  done
+
+
 section {* Infrastructure for concrete atom types *}
 
 section {* A swapping operation for concrete atoms *}