diff -r 9abc4a70540c -r 5f6fefdbf055 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Mon Feb 28 15:21:10 2011 +0000
@@ -8,8 +8,12 @@
 imports Main 
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
-uses ("nominal_library.ML")
+uses ("nominal_basics.ML")
+     ("nominal_thmdecls.ML")
+     ("nominal_permeq.ML")
+     ("nominal_library.ML")
      ("nominal_atoms.ML")
+     ("nominal_eqvt.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -437,38 +441,6 @@
 
 end
 
-lemma Not_eqvt:
-  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 all_eqvt:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma ex1_eqvt:
-  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
-  unfolding Ex1_def
-  apply(simp add: ex_eqvt)
-  unfolding permute_fun_def 
-  apply(simp add: conj_eqvt all_eqvt)
-  unfolding permute_fun_def
-  apply(simp add: imp_eqvt permute_bool_def)
-  done
-
 lemma permute_boolE:
   fixes P::"bool"
   shows "p \<bullet> P \<Longrightarrow> P"
@@ -541,11 +513,6 @@
   unfolding mem_def permute_fun_def permute_bool_def
   by simp
 
-lemma mem_eqvt:
-  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (simp add: permute_fun_app_eq)
-
 lemma empty_eqvt:
   shows "p \<bullet> {} = {}"
   unfolding empty_def Collect_def
@@ -555,22 +522,6 @@
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
   unfolding permute_set_eq_image image_insert ..
 
-lemma Collect_eqvt:
-  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
-  unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt:
-  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
-  unfolding Int_def
-  apply(simp add: Collect_eqvt)
-  apply(simp add: permute_fun_def)
-  apply(simp add: conj_eqvt)
-  apply(simp add: mem_eqvt)
-  apply(simp add: permute_fun_def)
-  done
-
-
-
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -635,6 +586,8 @@
   shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
   by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
 
+
+
 subsection {* Permutations for options *}
 
 instantiation option :: (pt) pt
@@ -654,6 +607,8 @@
 
 subsection {* Permutations for fsets *}
 
+
+
 lemma permute_fset_rsp[quot_respect]:
   shows "(op = ===> list_eq ===> list_eq) permute permute"
   unfolding fun_rel_def
@@ -682,7 +637,9 @@
   and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-
+lemma fset_eqvt: 
+  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
+  by (lifting set_eqvt)
 
 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
 
@@ -762,6 +719,277 @@
 instance int :: pure
 proof qed (rule permute_int_def)
 
+
+
+subsection {* Basic functions about permutations *}
+
+use "nominal_basics.ML"
+
+
+subsection {* Equivariance infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+lemmas [eqvt] =
+  (* permutations *)
+  uminus_eqvt add_perm_eqvt swap_eqvt 
+
+  (* datatypes *)
+  Pair_eqvt 
+  permute_list.simps 
+  permute_option.simps 
+  permute_sum.simps
+
+  (* sets *)
+  empty_eqvt insert_eqvt set_eqvt 
+
+  (* fsets *)
+  permute_fset fset_eqvt
+
+
+
+subsection {* perm_simp infrastructure *}
+
+definition
+  "unpermute p = permute (- p)"
+
+lemma eqvt_apply:
+  fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
+  and x :: "'a::pt"
+  shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+  unfolding permute_fun_def by simp
+
+lemma eqvt_lambda:
+  fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+  unfolding permute_fun_def unpermute_def by simp
+
+lemma eqvt_bound:
+  shows "p \<bullet> unpermute p x \<equiv> x"
+  unfolding unpermute_def by simp
+
+text {* provides perm_simp methods *}
+
+use "nominal_permeq.ML"
+setup Nominal_Permeq.setup
+
+method_setup perm_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
+
+method_setup perm_strict_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+(* the normal version of this lemma would cause loops *)
+lemma permute_eqvt_raw[eqvt_raw]:
+  shows "p \<bullet> permute \<equiv> permute"
+apply(simp add: fun_eq_iff permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+subsubsection {* Equivariance of Logical Operators *}
+
+lemma eq_eqvt [eqvt]:
+  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+  unfolding permute_eq_iff permute_bool_def ..
+
+lemma Not_eqvt [eqvt]:
+  shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
+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 imp_eqvt [eqvt]:
+  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+declare imp_eqvt[folded induct_implies_def, eqvt]
+
+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 all_eqvt [eqvt]:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
+lemma ex1_eqvt [eqvt]:
+  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+  unfolding Ex1_def
+  by (perm_simp) (rule refl)
+
+lemma mem_eqvt [eqvt]:
+  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+  unfolding mem_def
+  by (simp add: permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+  unfolding Collect_def permute_fun_def ..
+
+
+
+lemma inter_eqvt [eqvt]:
+  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+  unfolding Int_def
+  by (perm_simp) (rule refl)
+
+lemma image_eqvt [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 if_eqvt [eqvt]:
+  shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+  by (simp add: permute_fun_def permute_bool_def)
+
+lemma True_eqvt [eqvt]:
+  shows "p \<bullet> True = True"
+  unfolding permute_bool_def ..
+
+lemma False_eqvt [eqvt]:
+  shows "p \<bullet> False = False"
+  unfolding 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)
+
+lemma all_eqvt2:
+  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_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)
+
+lemma ex1_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)
+
+lemma the_eqvt:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+  apply(rule the1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule theI'[OF unique])
+  done
+
+lemma the_eqvt2:
+  assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+  apply(rule the1_equality [symmetric])
+  apply(simp add: ex1_eqvt2[symmetric])
+  apply(simp add: permute_bool_def unique)
+  apply(simp add: permute_bool_def)
+  apply(rule theI'[OF unique])
+  done
+
+subsubsection {* Equivariance Set Operations *}
+
+lemma Bex_eqvt[eqvt]:
+  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Bex_def
+  by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Ball_def
+  by (perm_simp) (rule refl)
+
+lemma UNIV_eqvt[eqvt]:
+  shows "p \<bullet> UNIV = UNIV"
+  unfolding UNIV_def
+  by (perm_simp) (rule refl)
+
+lemma union_eqvt[eqvt]:
+  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+  unfolding Un_def
+  by (perm_simp) (rule refl)
+
+lemma Diff_eqvt[eqvt]:
+  fixes A B :: "'a::pt set"
+  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+  unfolding set_diff_eq
+  by (perm_simp) (rule refl)
+
+lemma Compl_eqvt[eqvt]:
+  fixes A :: "'a::pt set"
+  shows "p \<bullet> (- A) = - (p \<bullet> A)"
+  unfolding Compl_eq_Diff_UNIV
+  by (perm_simp) (rule refl)
+
+lemma subset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+  unfolding subset_eq
+  by (perm_simp) (rule refl)
+
+lemma psubset_eqvt[eqvt]:
+  shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+  unfolding psubset_eq
+  by (perm_simp) (rule refl)
+
+lemma vimage_eqvt[eqvt]:
+  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+  unfolding vimage_def
+  by (perm_simp) (rule refl)
+
+lemma Union_eqvt[eqvt]:
+  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+  unfolding Union_eq 
+  by (perm_simp) (rule refl)
+
+lemma Sigma_eqvt:
+  shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
+unfolding Sigma_def
+unfolding UNION_eq_Union_image
+by (perm_simp) (rule refl)
+
+lemma finite_permute_iff:
+  shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+  unfolding permute_set_eq_vimage
+  using bij_permute by (rule finite_vimage_iff)
+
+lemma finite_eqvt[eqvt]:
+  shows "p \<bullet> finite A = finite (p \<bullet> A)"
+  unfolding finite_permute_iff permute_bool_def ..
+
+
+subsubsection {* Product Operations *}
+
+lemma fst_eqvt[eqvt]:
+  "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
+
+lemma snd_eqvt[eqvt]:
+  "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
+
+lemma split_eqvt[eqvt]: 
+  shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+  unfolding split_def
+  by (perm_simp) (rule refl)
+
+
+
+
 subsection {* Supp, Freshness and Supports *}
 
 context pt
@@ -843,12 +1071,12 @@
   finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
 qed
 
-lemma fresh_eqvt:
+lemma fresh_eqvt [eqvt]:
   shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
   unfolding permute_bool_def
   by (simp add: fresh_permute_iff)
 
-lemma supp_eqvt:
+lemma supp_eqvt [eqvt]:
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
   unfolding supp_conv_fresh
   unfolding Collect_def
@@ -970,7 +1198,6 @@
   "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
 
 
-
 section {* Finitely-supported types *}
 
 class fs = pt +
@@ -1246,6 +1473,58 @@
   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
 
 
+subsubsection {* List Operations *}
+
+lemma append_eqvt[eqvt]:
+  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+  by (induct xs) auto
+
+lemma rev_eqvt[eqvt]:
+  shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+  by (induct xs) (simp_all add: append_eqvt)
+
+lemma supp_rev:
+  shows "supp (rev xs) = supp xs"
+  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+
+lemma fresh_rev:
+  shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+
+lemma map_eqvt[eqvt]: 
+  shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+  by (induct xs) (auto)
+
+lemma supp_removeAll:
+  fixes x::"atom"
+  shows "supp (removeAll x xs) = supp xs - {x}"
+  by (induct xs)
+     (auto simp add: supp_Nil supp_Cons supp_atom)
+
+lemma filter_eqvt[eqvt]:
+  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt[eqvt]:
+  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
+lemma length_eqvt[eqvt]:
+  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
+
 instance list :: (fs) fs
 apply default
 apply (induct_tac x)
@@ -1266,13 +1545,6 @@
   unfolding fresh_def supp_def 
   unfolding MOST_iff_cofinite by simp
 
-lemma supp_subset_fresh:
-  assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
-  shows "supp y \<subseteq> supp x"
-  using a
-  unfolding fresh_def
-  by blast
-
 lemma fresh_fun_app:
   assumes "a \<sharp> f" and "a \<sharp> x" 
   shows "a \<sharp> f x"
@@ -1316,6 +1588,16 @@
     using supp_fun_app by auto
 qed
 
+lemma supp_fun_app_eqvt:
+  assumes a: "eqvt f"
+  shows "supp (f x) \<subseteq> supp x"
+proof -
+  from a have "supp f = {}" by (simp add: supp_fun_eqvt)
+  then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
+qed
+
+
+
 text {* equivariance of a function at a given argument *}
 
 definition
@@ -1353,7 +1635,8 @@
 using supp_eqvt_at[OF asm fin]
 by auto
 
-text {* helper functions for nominal_functions *}
+
+subsection {* helper functions for nominal_functions *}
 
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
@@ -1445,27 +1728,6 @@
   unfolding fresh_def
   by (auto simp add: supp_finite_atom_set assms)
 
-
-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)
-  unfolding eqvt_def
-  unfolding permute_fun_def
-  apply(simp)
-  unfolding UNION_def 
-  unfolding Collect_def 
-  unfolding Bex_def 
-  apply(simp add: ex_eqvt)
-  unfolding permute_fun_def
-  apply(simp add: conj_eqvt)
-  apply(simp add: mem_eqvt)
-  apply(simp add: supp_eqvt) 
-  unfolding permute_fun_def
-  apply(simp)
-  apply(assumption)
-  done
-
 lemma Union_supports_set:
   shows "(\<Union>x \<in> S. supp x) supports S"
 proof -
@@ -1489,12 +1751,14 @@
   assumes fin: "finite S"
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
+  have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
+    unfolding eqvt_def
+    by (perm_simp) (simp)
   have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
-    by (rule supp_finite_atom_set[symmetric])
-       (rule Union_of_finite_supp_sets[OF fin])
-  also have "\<dots> \<subseteq> supp S"
-    by (rule supp_subset_fresh)
-       (simp add: Union_fresh)
+    by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
+  also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
+  also have "\<dots> \<subseteq> supp S" using eqvt
+    by (rule supp_fun_app_eqvt)
   finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
 qed
 
@@ -1564,10 +1828,6 @@
 
 subsection {* Type @{typ "'a fset"} is finitely supported *}
 
-lemma fset_eqvt: 
-  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
-  by (lifting set_eqvt)
-
 lemma supp_fset [simp]:
   shows "supp (fset S) = supp S"
   unfolding supp_def
@@ -1610,6 +1870,30 @@
   done
 
 
+lemma in_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+by (induct S) (simp_all)
+
+lemma supp_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "supp (S |\<union>| T) = supp S \<union> supp T"
+by (induct S) (auto)
+
+lemma fresh_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+unfolding fresh_def
+by (simp add: supp_union_fset)
+
+lemma map_fset_eqvt[eqvt]: 
+  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+  by (lifting map_eqvt)
+
 section {* Freshness and Fresh-Star *}
 
 lemma fresh_Unit_elim: 
@@ -1751,15 +2035,10 @@
   unfolding fresh_star_def
   by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
 
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt [eqvt]:
   shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
 unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
+by (perm_simp) (rule refl)
 
 
 section {* Induction principle for permutations *}
@@ -2191,6 +2470,8 @@
   assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
   assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
 
+declare atom_eqvt[eqvt]
+
 class at = at_base +
   assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
 
@@ -2300,6 +2581,7 @@
 where
   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
 
+
 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
   unfolding flip_def by (rule swap_self)
 
@@ -2318,7 +2600,7 @@
 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
   by (simp add: flip_commute)
 
-lemma flip_eqvt: 
+lemma flip_eqvt [eqvt]: 
   fixes a b c::"'a::at_base"
   shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
   unfolding flip_def
@@ -2638,5 +2920,10 @@
 use "nominal_atoms.ML"
 
 
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+
 
 end