--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -1162,6 +1162,44 @@
   thus ?thesis ..
 qed
 
+lemma image_eqvt:
+  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+  unfolding permute_set_eq_image
+  unfolding permute_fun_def [where f=f]
+  by (simp add: image_image)
+
+lemma atom_image_cong:
+  shows "(atom ` X = atom ` Y) = (X = Y)"
+  apply(rule inj_image_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
+lemma atom_image_supp:
+  shows "supp S = supp (atom ` S)"
+  apply(simp add: supp_def)
+  apply(simp add: image_eqvt)
+  apply(subst (2) permute_fun_def)
+  apply(simp add: atom_eqvt)
+  apply(simp add: atom_image_cong)
+  done
+
+lemma supp_finite_at_set:
+  assumes a: "finite S"
+  shows "supp S = atom ` S"
+proof -
+  have fin: "finite (atom ` S)" 
+    using a by (simp add: finite_imageI) 
+  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
+  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
+  finally show "supp S = atom ` S" by simp
+qed
+
+lemma supp_at_insert:
+  fixes a::"'a::at_base"
+  assumes a: "finite S"
+  shows "supp (insert a S) = supp a \<union> supp S"
+  using a by (simp add: supp_finite_at_set supp_at_base)
+
 section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"