--- a/Nominal-General/Nominal2_Supp.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Nominal-General/Nominal2_Supp.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -474,81 +474,4 @@
 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"
-proof -
-  { fix a b
-    have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
-      unfolding permute_set_eq by force
-  }
-  then show "(\<Union>x \<in> S. supp x) supports S"
-    unfolding supports_def 
-    by (simp add: fresh_def[symmetric] swap_fresh_fresh)
-qed
-
-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)"
-    by (rule supp_finite_atom_set[symmetric])
-       (rule Union_of_fin_supp_sets[OF fin])
-  also have "\<dots> \<subseteq> supp S"
-    by (rule supp_subset_fresh)
-       (simp add: Union_fresh)
-  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
-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)
-
-lemma supp_set:
-  fixes xs :: "('a::fs) list"
-  shows "supp (set xs) = supp xs"
-apply(induct xs)
-apply(simp add: supp_set_empty supp_Nil)
-apply(simp add: supp_Cons supp_of_fin_insert)
-done
-
 end