# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1292466335 0
# Node ID f5c7375ab4655177801dfb79ebe65c1a0ec6baba
# Parent  666ffc8a92a9bd763ffb57cbf051fc68c51b93a2
added theorem-rewriter conversion

diff -r 666ffc8a92a9 -r f5c7375ab465 Nominal/nominal_permeq.ML
--- a/Nominal/nominal_permeq.ML	Tue Dec 14 14:23:40 2010 +0000
+++ b/Nominal/nominal_permeq.ML	Thu Dec 16 02:25:35 2010 +0000
@@ -5,6 +5,9 @@
 
 signature NOMINAL_PERMEQ =
 sig
+  val eqvt_rule: Proof.context -> thm list -> string list -> thm -> thm
+  val eqvt_strict_rule: Proof.context -> thm list -> string list -> thm -> thm
+
   val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
   val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
   
@@ -116,7 +119,7 @@
   end
 
 (* main conversion *) 
-fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
+fun main_eqvt_conv ctxt strict_flag user_thms excluded ctrm =
   let
     val first_conv_wrapper = 
       if trace_enabled ctxt 
@@ -137,17 +140,32 @@
 
 (* the eqvt-tactics first eta-normalise goals in 
    order to avoid problems with inductions in the
-   equivaraince command. *)
+   equivariance command. *)
 
 (* raises an error if some permutations cannot be eliminated *)
-fun eqvt_strict_tac ctxt user_thms excluded = 
-  CONVERSION (Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
+fun eqvt_strict_conv ctxt user_thms excluded = 
+  Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt true user_thms excluded)) ctxt
 
 (* prints a warning message if some permutations cannot be eliminated *)
+fun eqvt_conv ctxt user_thms excluded = 
+  Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt false user_thms excluded)) ctxt
+
+
+(* thms rewriters *)
+fun eqvt_strict_rule ctxt user_thms excluded = 
+  Conv.fconv_rule (eqvt_strict_conv ctxt user_thms excluded)
+
+fun eqvt_rule ctxt user_thms excluded = 
+  Conv.fconv_rule (eqvt_conv ctxt user_thms excluded)
+
+(* tactics *)
+fun eqvt_strict_tac ctxt user_thms excluded = 
+  CONVERSION (eqvt_strict_conv ctxt user_thms excluded)
+
 fun eqvt_tac ctxt user_thms excluded = 
-  CONVERSION (Conv.top_conv 
-    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
+  CONVERSION (eqvt_conv ctxt user_thms excluded)
 
 (* setup of the configuration value *)
 val setup =