--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 21 21:52:30 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Thu Apr 22 05:16:23 2010 +0200
@@ -5,6 +5,7 @@
 *)
 theory Nominal2_Atoms
 imports Nominal2_Base
+        Nominal2_Eqvt
 uses ("nominal_atoms.ML")
 begin
 
@@ -20,6 +21,8 @@
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
 
+declare atom_eqvt[eqvt]
+
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
 
@@ -75,6 +78,62 @@
   thus ?thesis ..
 qed
 
+lemma atom_image_cong:
+  fixes X Y::"('a::at_base) set"
+  shows "(atom ` X = atom ` Y) = (X = Y)"
+  apply(rule inj_image_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
+lemma atom_image_supp:
+  "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:
+  fixes S::"('a::at) set"
+  assumes a: "finite S"
+  shows "supp S = atom ` S"
+  apply(rule finite_supp_unique)
+  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)
+  apply(drule swap_set_in)
+  apply(assumption)
+  apply(simp)
+  apply(simp add: image_eqvt)
+  apply(simp add: permute_fun_def)
+  apply(simp add: atom_eqvt)
+  apply(simp add: atom_image_cong)
+  done
+
+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
 
 section {* A swapping operation for concrete atoms *}