--- a/Nominal/Abs.thy	Thu Mar 11 19:24:07 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 11 19:41:11 2010 +0100
@@ -723,6 +723,30 @@
   "distinct_perms [] = True"
 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
 
+(* support of concrete atom sets *)
+
+atom_decl name
+
+lemma atom_eqvt_raw:
+  fixes p::"perm"
+  shows "(p \<bullet> atom) = atom"
+by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
+
+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
+  fixes as::"name set"
+  shows "supp (atom ` as) = supp as"
+apply(simp add: supp_def)
+apply(simp add: image_eqvt)
+apply(simp add: atom_eqvt_raw)
+apply(simp add: atom_image_cong)
+done
+
 
 
 end