--- a/Nominal-General/Nominal2_Base.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -430,6 +430,19 @@
   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
 by (simp add: permute_bool_def)
 
+lemma conj_eqvt:
+  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma imp_eqvt:
+  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma ex_eqvt:
+  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
 lemma permute_boolE:
   fixes P::"bool"
   shows "p \<bullet> P \<Longrightarrow> P"
@@ -851,6 +864,7 @@
 
 section {* Support for finite sets of atoms *}
 
+
 lemma supp_finite_atom_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -862,12 +876,6 @@
   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. *}
 
 lemma perm_swap_eq:
@@ -1065,6 +1073,7 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
+
 section {* Support and freshness for applications *}
 
 lemma fresh_conv_MOST: 
@@ -1112,6 +1121,78 @@
 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(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt)
+  apply(subst permute_fun_app_eq)
+  back
+  apply(simp add: supp_eqvt)
+  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)
+
+
 section {* Concrete atoms types *}
 
 text {*
@@ -1179,44 +1260,18 @@
   thus ?thesis ..
 qed
 
-lemma image_eqvt:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-  apply(rule inj_image_eq_iff)
-  apply(simp add: inj_on_def)
-  done
-
-lemma atom_image_supp:
-  shows "supp S = supp (atom ` S)"
-  apply(simp add: supp_def)
-  apply(simp add: image_eqvt)
-  apply(subst (2) permute_fun_def)
-  apply(simp add: atom_eqvt)
-  apply(simp add: atom_image_cong)
-  done
-
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
-proof -
-  have fin: "finite (atom ` S)" using a by simp
-  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
-  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
-  finally show "supp S = atom ` S" by simp
-qed
+apply(simp add: supp_of_fin_sets[OF a])
+apply(simp add: supp_at_base)
+apply(auto)
+done
 
-lemma supp_at_base_insert:
-  fixes a::"'a::at_base"
-  assumes a: "finite S"
-  shows "supp (insert a S) = supp a \<union> supp S"
-  using a by (simp add: supp_finite_set_at_base supp_at_base)
 
 section {* library functions for the nominal infrastructure *}
 use "nominal_library.ML"
 
+
+
 end