--- a/Nominal-General/Nominal2_Atoms.thy	Fri Apr 23 11:12:38 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Sat Apr 24 09:49:23 2010 +0200
@@ -126,14 +126,59 @@
   apply(simp add: atom_image_cong)
   done
 
+lemma supp_finite_at_set_aux:
+  fixes S::"('a::at) set"
+  assumes a: "finite S"
+  shows "supp S = atom ` S"
+proof
+  show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" 
+    apply(rule supp_is_subset)
+    apply(simp add: supports_def)
+    apply(rule allI)+
+    apply(rule impI)
+    apply(rule swap_fresh_fresh)
+    apply(simp add: fresh_def)
+    apply(simp add: atom_image_supp)
+    apply(subst supp_finite_atom_set)
+    apply(rule finite_imageI)
+    apply(simp add: a)
+    apply(simp)
+    apply(simp add: fresh_def)
+    apply(simp add: atom_image_supp)
+    apply(subst supp_finite_atom_set)
+    apply(rule finite_imageI)
+    apply(simp add: a)
+    apply(simp)
+    apply(rule finite_imageI)
+    apply(simp add: a)
+    done
+next 
+  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S"
+    by (simp add: supp_fun_app)
+  moreover
+  have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}"
+    apply(rule supp_fun_eqvt)
+    apply(perm_simp)
+    apply(simp)
+    done
+  moreover 
+  have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" 
+    apply(subst supp_finite_atom_set)
+    apply(rule finite_imageI)
+    apply(simp add: a)
+    apply(simp)
+    done
+  ultimately 
+  show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp
+qed
+  
+
 lemma supp_at_insert:
   fixes S::"('a::at) set"
   assumes a: "finite S"
   shows "supp (insert a S) = supp a \<union> supp S"
-  using a
-  apply (simp add: supp_finite_at_set)
-  apply (simp add: supp_at_base)
-  done
+  using a by (simp add: supp_finite_at_set supp_at_base)
+
 
 section {* A swapping operation for concrete atoms *}