--- a/Nominal-General/Nominal2_Atoms.thy	Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy	Mon Apr 26 10:01:13 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,107 @@
   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_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 by (simp add: supp_finite_at_set supp_at_base)
+
 
 section {* A swapping operation for concrete atoms *}