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

--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -20,6 +20,20 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+
+section {* eqvt lemmas *}
+
+lemmas [eqvt] =
+  conj_eqvt Not_eqvt ex_eqvt imp_eqvt
+  imp_eqvt[folded induct_implies_def]
+
+  (* nominal *)
+  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
+
+  (* datatypes *)
+  Pair_eqvt permute_list.simps
+
+
 text {* helper lemmas for the perm_simp *}
 
 definition
@@ -79,14 +93,6 @@
   shows "p \<bullet> False = False"
   unfolding permute_bool_def ..
 
-lemma imp_eqvt[eqvt]:
-  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
-lemma conj_eqvt[eqvt]:
-  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
 lemma disj_eqvt[eqvt]:
   shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
   by (simp add: permute_bool_def)
@@ -104,11 +110,6 @@
   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
-lemma ex_eqvt[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 ex_eqvt2:
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
@@ -211,6 +212,12 @@
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
 
+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 vimage_eqvt[eqvt]:
   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
   unfolding vimage_def
@@ -230,6 +237,15 @@
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
   unfolding finite_permute_iff permute_bool_def ..
 
+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
+
+
 section {* List Operations *}
 
 lemma append_eqvt[eqvt]:
@@ -295,20 +311,6 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_unit)
 
-section {* additional eqvt lemmas *}
-
-lemmas [eqvt] = 
-  imp_eqvt [folded induct_implies_def]
-
-  (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
-
-  (* datatypes *)
-  Pair_eqvt permute_list.simps
-
-  (* sets *)
-  image_eqvt
-
 
 section {* Test cases *}
 

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

--- a/Nominal/Nominal2_FSet.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -36,14 +36,12 @@
 
 end
 
-lemma permute_fset[simp]:
+lemma permute_fset[simp, eqvt]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-declare permute_fset[eqvt]
-
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -113,7 +111,7 @@
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
-  apply (simp add: supp_atom_insert)
+  apply (simp add: supp_of_fin_insert)
   apply (rule conjI)
   apply (unfold fresh_star_def)
   apply simp

--- a/Pearl-jv/Paper.thy	Fri Sep 03 22:35:35 2010 +0800
+++ b/Pearl-jv/Paper.thy	Sat Sep 04 05:43:03 2010 +0800
@@ -44,6 +44,8 @@
 section {* Introduction *}
 
 text {*
+  TODO: write about supp of finite sets
+
   Nominal Isabelle provides a proving infratructure for
   convenient reasoning about programming languages. At its core Nominal
   Isabelle is based on the nominal logic work by Pitts at al