diff -r 6471e252f14e -r 78fdc6b36a1c Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -223,6 +223,13 @@
   shows "a \<sharp> ()"
   by (simp add: fresh_def supp_unit)
 
+lemma permute_eqvt_raw:
+  shows "p \<bullet> permute = permute"
+apply(simp add: expand_fun_eq permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
 section {* Equivariance automation *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
@@ -237,9 +244,7 @@
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
-  (*permute_eqvt commented out since it loops *)
   supp_eqvt fresh_eqvt
-  permute_pure
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
@@ -251,6 +256,9 @@
 
   atom_eqvt add_perm_eqvt
 
+lemmas [eqvt_raw] =
+  permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) 
+
 thm eqvts
 thm eqvts_raw
 
@@ -274,31 +282,93 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
+ML {* @{const Trueprop} *}
+
 use "nominal_permeq.ML"
-
+setup Nominal_Permeq.setup
 
-lemma "p \<bullet> (A \<longrightarrow> B = C)"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) 
+method_setup perm_simp =
+ {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *}
+ {* pushes permutations inside *}
+
+declare [[trace_eqvt = true]]
+
+lemma 
+  fixes B::"'a::pt"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (A \<longrightarrow> B = C)"
+apply (perm_simp) 
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
+apply (perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  fixes p q::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes p q r::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes p r::"perm"
+  shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
+apply (perm_simp)
 oops
 
-lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes p q r::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
 oops
 
-lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
-apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+lemma 
+  fixes C D::"bool"
+  shows "B (p \<bullet> (C = D))"
+apply(perm_simp)
+oops
+
+declare [[trace_eqvt = false]]
+
+text {* Problem: there is no raw eqvt-rule for The *}
+lemma "p \<bullet> (THE x. P x) = foo"
+apply(perm_simp)
 oops