diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy	Mon Apr 26 10:01:13 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
@@ -835,6 +844,24 @@
 instance atom :: fs
 by default (simp add: supp_atom)
 
+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
+
+lemma supp_atom_insert:
+  fixes S::"atom set"
+  assumes a: "finite S"
+  shows "supp (insert a S) = supp a \<union> supp S"
+  using a by (simp add: supp_finite_atom_set supp_atom)
 
 section {* Type @{typ perm} is finitely-supported. *}
 
@@ -1054,32 +1081,18 @@
   unfolding fresh_def
   by auto
 
-(* alternative proof *)
-lemma 
-  shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
-proof (rule subsetCI)
-  fix a::"atom"
-  assume a: "a \<in> supp (f x)"
-  assume b: "a \<notin> supp f \<union> supp x"
-  then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 
-    unfolding supp_def by auto
-  then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp
-  moreover 
-  have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"
-    by auto
-  ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"
-    using finite_subset by auto
-  then have "a \<notin> supp (f x)" unfolding supp_def
-    by (simp add: permute_fun_app_eq)
-  with a show "False" by simp
-qed
-    
+lemma supp_fun_eqvt:
+  assumes a: "\<forall>p. p \<bullet> f = f"
+  shows "supp f = {}"
+  unfolding supp_def 
+  using a by simp
+
+
 lemma fresh_fun_eqvt_app:
   assumes a: "\<forall>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
-  from a have "supp f = {}"
-    unfolding supp_def by simp
+  from a have "supp f = {}" by (simp add: supp_fun_eqvt)
   then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
     unfolding fresh_def
     using supp_fun_app