--- 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