--- a/Nominal-General/Nominal2_Base.thy	Fri Apr 30 14:21:18 2010 +0100
+++ b/Nominal-General/Nominal2_Base.thy	Fri Apr 30 15:34:26 2010 +0100
@@ -1067,10 +1067,17 @@
   unfolding fresh_def supp_def 
   unfolding MOST_iff_cofinite by simp
 
+lemma supp_subset_fresh:
+  assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
+  shows "supp y \<subseteq> supp x"
+  using a
+  unfolding fresh_def
+  by blast
+
 lemma fresh_fun_app:
   assumes "a \<sharp> f" and "a \<sharp> x" 
   shows "a \<sharp> f x"
-  using assms 
+  using assms
   unfolding fresh_conv_MOST
   unfolding permute_fun_app_eq 
   by (elim MOST_rev_mp, simp)
@@ -1081,22 +1088,22 @@
   unfolding fresh_def
   by auto
 
+text {* support of equivariant functions *}
+
 lemma supp_fun_eqvt:
-  assumes a: "\<forall>p. p \<bullet> f = f"
+  assumes a: "\<And>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"
+  assumes a: "\<And>p. p \<bullet> f = f"
   shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
   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 
-    by auto
+    using supp_fun_app by auto
 qed
 
 

--- a/Nominal-General/Nominal2_Supp.thy	Fri Apr 30 14:21:18 2010 +0100
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Apr 30 15:34:26 2010 +0100
@@ -467,4 +467,85 @@
   qed
 qed
 
+
+section {* Support of Finite Sets of Finitely Supported Elements *}
+
+lemma Union_fresh:
+  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
+  unfolding Union_image_eq[symmetric]
+  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
+  apply(perm_simp)
+  apply(rule refl)
+  apply(assumption)
+  done
+
+lemma Union_supports_set:
+  shows "(\<Union>x \<in> S. supp x) supports S"
+  apply(simp add: supports_def fresh_def[symmetric])
+  apply(rule allI)+
+  apply(rule impI)
+  apply(erule conjE)
+  apply(simp add: permute_set_eq)
+  apply(auto)
+  apply(subgoal_tac "(a \<rightleftharpoons> b) \<bullet> xa = xa")(*A*)
+  apply(simp)
+  apply(rule swap_fresh_fresh)
+  apply(force)
+  apply(force)
+  apply(rule_tac x="x" in exI)
+  apply(simp)
+  apply(rule sym)
+  apply(rule swap_fresh_fresh)
+  apply(auto)
+  done
+
+lemma Union_of_fin_supp_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"   
+  shows "finite (\<Union>x\<in>S. supp x)"
+  using fin by (induct) (auto simp add: finite_supp)
+
+lemma Union_included_in_supp:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
+proof -
+  have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
+    apply(rule supp_finite_atom_set[symmetric])
+    apply(rule Union_of_fin_supp_sets)
+    apply(rule fin)
+    done
+  also have "\<dots> \<subseteq> supp S"
+    apply(rule supp_subset_fresh)
+    apply(simp add: Union_fresh)
+    done
+  finally show ?thesis .
+qed
+
+lemma supp_of_fin_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(supp S) = (\<Union>x\<in>S. supp x)"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set)
+apply(rule Union_of_fin_supp_sets[OF fin])
+apply(rule Union_included_in_supp[OF fin])
+done
+
+lemma supp_of_fin_union:
+  fixes S T::"('a::fs) set"
+  assumes fin1: "finite S"
+  and     fin2: "finite T"
+  shows "supp (S \<union> T) = supp S \<union> supp T"
+  using fin1 fin2
+  by (simp add: supp_of_fin_sets)
+
+lemma supp_of_fin_insert:
+  fixes S::"('a::fs) set"
+  assumes fin:  "finite S"
+  shows "supp (insert x S) = supp x \<union> supp S"
+  using fin
+  by (simp add: supp_of_fin_sets)
+
 end