diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -799,6 +799,21 @@
  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
  {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
 
+simproc_setup perm_simproc ("p \<bullet> t") = {* fn _ => fn ss => fn ctrm =>
+  case term_of (Thm.dest_arg ctrm) of 
+    Free _ => NONE
+  | Var _ => NONE
+  | Const (@{const_name permute}, _) $ _ $ _ => NONE
+  | _ =>
+      let
+        val ctxt = Simplifier.the_context ss
+        val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm
+          handle ERROR _ => Thm.reflexive ctrm
+      in
+        if Thm.is_reflexive thm then NONE else SOME(thm)
+      end
+*}
+
 
 subsubsection {* Equivariance for permutations and swapping *}
 
@@ -876,10 +891,6 @@
   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 Let_eqvt [eqvt]:
-  shows "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-  unfolding Let_def permute_fun_app_eq ..
-
 lemma True_eqvt [eqvt]:
   shows "p \<bullet> True = True"
   unfolding permute_bool_def ..
@@ -920,7 +931,7 @@
   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 only: ex1_eqvt2[symmetric])
   apply(simp add: permute_bool_def unique)
   apply(simp add: permute_bool_def)
   apply(rule theI'[OF unique])
@@ -940,84 +951,76 @@
 
 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)
+  unfolding Int_def by simp
 
 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)
+  unfolding Bex_def by simp
 
 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)
+  unfolding Ball_def by simp
 
 lemma image_eqvt [eqvt]:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding image_def
-  by (perm_simp) (rule refl)
+  unfolding image_def by simp
 
 lemma Image_eqvt [eqvt]:
   shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
-  unfolding Image_def
-  by (perm_simp) (rule refl)
+  unfolding Image_def by simp
 
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
-  unfolding UNIV_def
+  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)
+  unfolding Un_def by simp
 
 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)
+  unfolding set_diff_eq by simp
 
 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)
+  unfolding Compl_eq_Diff_UNIV by simp
 
 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)
+  unfolding subset_eq by simp
 
 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)
+  unfolding psubset_eq by simp
 
 lemma vimage_eqvt [eqvt]:
   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
-  unfolding vimage_def
-  by (perm_simp) (rule refl)
+  unfolding vimage_def by simp
 
 lemma Union_eqvt [eqvt]:
   shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
-  unfolding Union_eq 
-  by (perm_simp) (rule refl)
+  unfolding Union_eq by simp
 
 lemma Inter_eqvt [eqvt]:
   shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
-  unfolding Inter_eq 
-  by (perm_simp) (rule refl)
+  unfolding Inter_eq by simp
+
+thm foldr.simps
 
 lemma foldr_eqvt[eqvt]:
-  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
-  apply (induct b)
-  apply simp_all
-  apply (perm_simp)
-  apply simp
+  "p \<bullet> foldr f xs = foldr (p \<bullet> f) (p \<bullet> xs)"
+  apply(induct xs)
+  apply(simp_all)
+  apply(perm_simp exclude: foldr)
+  apply(simp)
   done
 
+thm eqvts_raw
+
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -1090,12 +1093,12 @@
   fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})"
   shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)"
 unfolding lfp_def
-by (perm_simp) (rule refl)
+by simp
 
 lemma finite_eqvt [eqvt]:
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
 unfolding finite_def
-by (perm_simp) (rule refl)
+by simp
 
 
 subsubsection {* Equivariance for product operations *}
@@ -1111,7 +1114,7 @@
 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)
+  by simp
 
 
 subsubsection {* Equivariance for list operations *}
@@ -1126,7 +1129,7 @@
 
 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)
+  by (induct xs) (simp_all)
 
 lemma removeAll_eqvt [eqvt]:
   shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
@@ -1156,15 +1159,14 @@
 
 lemma option_map_eqvt[eqvt]:
   shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
-  by (cases x) (simp_all, simp add: permute_fun_app_eq)
+  by (cases x) (simp_all)
 
 
 subsubsection {* Equivariance for @{typ "'a fset"} *}
 
 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)
+unfolding in_fset by simp
 
 lemma union_fset_eqvt [eqvt]:
   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
@@ -1174,7 +1176,6 @@
   shows "(p \<bullet> (S |\<inter>| T)) = ((p \<bullet> S) |\<inter>| (p \<bullet> T))"
   apply(descending)
   unfolding list_eq_def inter_list_def
-  apply(perm_simp)
   apply(simp)
   done
 
@@ -1182,7 +1183,6 @@
   shows "(p \<bullet> (S |\<subseteq>| T)) = ((p \<bullet> S) |\<subseteq>| (p \<bullet> T))"
   apply(descending)
   unfolding sub_list_def
-  apply(perm_simp)
   apply(simp)
   done
   
@@ -1254,14 +1254,11 @@
 
 lemma supp_eqvt [eqvt]:
   shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
-  unfolding supp_def
-  by (perm_simp)
-     (simp only: permute_eqvt[symmetric])
+  unfolding supp_def by simp
 
 lemma fresh_eqvt [eqvt]:
   shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
-  unfolding fresh_def
-  by (perm_simp) (rule refl)
+  unfolding fresh_def by simp
 
 lemma fresh_permute_iff:
   shows "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x"
@@ -1751,7 +1748,7 @@
       using assms by (simp add: eqvt_at_def)
     also have "\<dots> = (p + q) \<bullet> (f x)" by simp
     also have "\<dots> = f ((p + q) \<bullet> x)"
-      using assms by (simp add: eqvt_at_def)
+      using assms by (simp only: eqvt_at_def)
     finally have "p \<bullet> (f (q \<bullet> x)) = f (p \<bullet> q \<bullet> x)" by simp } 
   then show "eqvt_at f (q \<bullet> x)" unfolding eqvt_at_def
     by simp
@@ -1978,7 +1975,7 @@
   shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
 proof -
   have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" 
-    unfolding eqvt_def
+    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])
@@ -2334,9 +2331,7 @@
 
 lemma fresh_star_eqvt [eqvt]:
   shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
-unfolding fresh_star_def
-by (perm_simp) (rule refl)
-
+unfolding fresh_star_def by simp
 
 
 section {* Induction principle for permutations *}
@@ -2709,7 +2704,8 @@
 	apply(blast)
 	apply(simp)
 	done
-      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" by (simp add: supp_swap)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
+        unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
 	using ** by (auto simp add: insert_eqvt)
@@ -2777,7 +2773,8 @@
 	apply(blast)
 	apply(simp)
 	done
-      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" by (simp add: supp_swap)
+      then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" 
+        unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
 	using ** by (auto simp add: insert_eqvt)
@@ -2961,7 +2958,7 @@
   fixes a::"'a::at_base"
   shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"
   unfolding atom_eqvt[symmetric]
-  by (simp add: fresh_permute_iff)
+  by (simp only: fresh_permute_iff)
 
 
 section {* Infrastructure for concrete atom types *}