--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 17:42:57 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Wed Apr 21 21:29:09 2010 +0200
@@ -29,6 +29,11 @@
 where
   "sort_of (Atom s i) = s"
 
+primrec
+  nat_of :: "atom \<Rightarrow> nat"
+where
+  "nat_of (Atom s n) = n"
+
 
 text {* There are infinitely many atoms of each sort. *}
 lemma INFM_sort_of_eq: 
@@ -63,6 +68,11 @@
   then show ?thesis ..
 qed
 
+lemma atom_components_eq_iff:
+  fixes a b :: atom
+  shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
+  by (induct a, induct b, simp)
+
 section {* Sort-Respecting Permutations *}
 
 typedef perm =
@@ -459,7 +469,6 @@
   unfolding permute_set_eq
   using a by (auto simp add: swap_atom)
 
-
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -800,6 +809,22 @@
   qed
 qed
 
+section {* Support for finite sets of atoms *}
+
+
+lemma supp_finite_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(simp add: swap_set_not_in)
+  apply(rule assms)
+  apply(simp add: swap_set_in)
+done
+
+
+
 section {* Finitely-supported types *}
 
 class fs = pt +