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