--- a/Nominal/Ex/Lambda.thy	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Apr 13 13:41:52 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2" 
 begin
 
+
 atom_decl name
 
 nominal_datatype lam =
@@ -9,6 +10,17 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+inductive 
+  triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
+where
+  Var: "triv (Var x) n"
+
+equivariance triv
+nominal_inductive triv avoids Var : "{}::name set"
+apply(auto simp add: fresh_star_def)
+done 
+
+
 text {* height function *}
 
 nominal_primrec
@@ -494,7 +506,6 @@
 
 
 
-
 end
 
 

--- a/Nominal/nominal_dt_alpha.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -47,6 +47,8 @@
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
 struct
 
+open Nominal_Permeq
+
 fun lookup xs x = the (AList.lookup (op=) xs x)
 fun group xs = AList.group (op=) xs
 
@@ -505,7 +507,7 @@
       [ etac exi_neg,
         resolve_tac @{thms alpha_sym_eqvt},
         asm_full_simp_tac (HOL_ss addsimps prod_simps),
-        Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+        eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
         trans_prem_tac pred_names ctxt ] 
   end
 
@@ -560,7 +562,7 @@
           resolve_tac @{thms alpha_trans_eqvt}, 
           atac,
           aatac pred_names ctxt, 
-          Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+          eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
           asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
   end
 			  

--- a/Nominal/nominal_dt_quot.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_quot.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -49,6 +49,8 @@
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
 struct
 
+open Nominal_Permeq
+
 fun lookup xs x = the (AList.lookup (op=) xs x)
 
 
@@ -172,7 +174,7 @@
     val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
   in
     EVERY' [ simp_tac ss1,
-             Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
+             eqvt_tac ctxt (eqvt_strict_config addpres perm_simps),
              simp_tac ss2 ]
   end
 
@@ -299,11 +301,12 @@
             case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
               SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
             | NONE => mk_bn_supp_abs_tac fv_fun
+          val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts)
         in
           EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
                    TRY o supp_abs_tac,
                    TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
-                   TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
+                   TRY o eqvt_tac ctxt eqvt_rconfig, 
                    TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
                    TRY o asm_full_simp_tac (add_ss thms3),
                    TRY o simp_tac (add_ss thms2),
@@ -373,7 +376,7 @@
     val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
     val ss_tac = 
       EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
-              TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
+              TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts),
               TRY o asm_full_simp_tac HOL_basic_ss]
   in
     induct_prove qtys props qinduct (K ss_tac) ctxt'
@@ -519,8 +522,8 @@
      in
        [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
          |> (if rec_flag
-             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
-             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
+             then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)
+             else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ]
      end
 
 
@@ -556,8 +559,8 @@
             val (abs_eqs, peqs) = split_filter is_abs_eq eqs
 
             val fprops' = 
-              map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
-              @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+              map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops
+              @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops
 
             (* for freshness conditions *) 
             val tac1 = SOLVED' (EVERY'

--- a/Nominal/nominal_dt_rawfuns.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -40,6 +40,8 @@
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+open Nominal_Permeq
+
 (* string list      - type variables of a datatype
    binding          - name of the datatype
    mixfix           - its mixfix
@@ -361,7 +363,7 @@
   SUBPROOF (fn {prems, context, ...} => 
     HEADGOAL 
       (simp_tac (HOL_basic_ss addsimps simps)
-       THEN' Nominal_Permeq.eqvt_tac context [] const_names
+       THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names)
        THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
 
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 

--- a/Nominal/nominal_eqvt.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_eqvt.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -5,6 +5,7 @@
     Automatic proofs for equivariance of inductive predicates.
 *)
 
+
 signature NOMINAL_EQVT =
 sig
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
@@ -32,7 +33,6 @@
 (** equivariance tactics **)
 
 val perm_boolE = @{thm permute_boolE}
-val perm_cancel = @{thms permute_minus_cancel(2)}
 
 fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
   let
@@ -41,16 +41,18 @@
     val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
     val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
     val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def}
+    val eqvt_sconfig = 
+          eqvt_strict_config addpres @{thms permute_minus_cancel(2)} addexcls pred_names
   in
-    eqvt_strict_tac ctxt [] pred_names THEN'
+    eqvt_tac ctxt (eqvt_strict_config addexcls pred_names) THEN'
     SUBPROOF (fn {prems, context as ctxt, ...} =>
       let
         val prems' = map (transform_prem2 ctxt pred_names) prems
         val tac1 = resolve_tac prems'
         val tac2 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
+          eqvt_tac ctxt eqvt_sconfig, resolve_tac prems' ]
         val tac3 = EVERY' [ rtac pi_intro_rule, 
-          eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, 
+          eqvt_tac ctxt eqvt_sconfig, simp_tac simps1, 
           simp_tac simps2, resolve_tac prems']
       in
         (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 

--- a/Nominal/nominal_inductive.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_inductive.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -133,8 +133,18 @@
       f x y z u v r s :: map7 f xs ys zs us vs rs ss
 
 (* local abbreviations *)
-fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} []  
-fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} []  
+
+local
+  open Nominal_Permeq
+in
+(* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) 
+
+val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel}
+
+fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig
+fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig  
+
+end
 
 val all_elims = 
   let

--- a/Nominal/nominal_permeq.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_permeq.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -3,14 +3,24 @@
     Author:     Brian Huffman
 *)
 
+infix 4 addpres addposts addexcls
+
 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
+  datatype eqvt_config = 
+    Eqvt_Config of {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list}
 
-  val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
-  val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
-  
+  val eqvt_relaxed_config: eqvt_config 
+  val eqvt_strict_config: eqvt_config
+  val addpres : (eqvt_config * thm list) -> eqvt_config
+  val addposts : (eqvt_config * thm list) -> eqvt_config
+  val addexcls : (eqvt_config * string list) -> eqvt_config
+  val delpres : eqvt_config -> eqvt_config
+  val delposts : eqvt_config -> eqvt_config
+
+  val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
+  val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic
+
   val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
   val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
   val args_parser: (thm list * string list) context_parser
@@ -21,10 +31,10 @@
 
 (* 
 
-- eqvt_tac and eqvt_strict_tac take a list of theorems
-  which are first tried to simplify permutations
+- eqvt_tac and eqvt_rule take a  list of theorems which 
+  are first tried to simplify permutations
 
-  the string list contains constants that should not be
+- the string list contains constants that should not be
   analysed (for example there is no raw eqvt-lemma for
   the constant The); therefore it should not be analysed 
 
@@ -38,6 +48,52 @@
 
 open Nominal_ThmDecls;
 
+datatype eqvt_config = Eqvt_Config of 
+  {strict_mode: bool, pre_thms: thm list, post_thms: thm list, excluded: string list}
+
+fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addpres thms = 
+  Eqvt_Config { strict_mode = strict_mode, 
+                pre_thms = thms @ pre_thms, 
+                post_thms = post_thms, 
+                excluded = excluded }
+
+fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addposts thms = 
+  Eqvt_Config { strict_mode = strict_mode, 
+                pre_thms = pre_thms, 
+                post_thms = thms @ post_thms,
+                excluded = excluded }
+
+fun (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) addexcls excls = 
+  Eqvt_Config { strict_mode = strict_mode, 
+                pre_thms = pre_thms, 
+                post_thms = post_thms,
+                excluded = excls @ excluded }
+
+fun delpres (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = 
+  Eqvt_Config { strict_mode = strict_mode, 
+                pre_thms = [], 
+                post_thms = post_thms,
+                excluded = excluded }
+
+fun delposts (Eqvt_Config {strict_mode, pre_thms, post_thms, excluded}) = 
+  Eqvt_Config { strict_mode = strict_mode, 
+                pre_thms = pre_thms, 
+                post_thms = [],
+                excluded = excluded }
+
+val eqvt_relaxed_config =
+  Eqvt_Config { strict_mode = false, 
+                pre_thms = @{thms eqvt_bound}, 
+                post_thms = @{thms permute_pure},
+                excluded = [] }
+
+val eqvt_strict_config = 
+  Eqvt_Config { strict_mode = true, 
+                pre_thms = @{thms eqvt_bound}, 
+                post_thms = @{thms permute_pure},
+                excluded = [] }
+
+
 (* tracing infrastructure *)
 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
 
@@ -119,53 +175,41 @@
   end
 
 (* main conversion *) 
-fun main_eqvt_conv ctxt strict_flag user_thms excluded ctrm =
+fun main_eqvt_conv ctxt config ctrm =
   let
+    val Eqvt_Config {strict_mode, pre_thms, post_thms, excluded} = config
+
     val first_conv_wrapper = 
       if trace_enabled ctxt 
       then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
       else Conv.first_conv
 
-    val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt
-    val post_thms = map safe_mk_equiv @{thms permute_pure}
+    val all_pre_thms = map safe_mk_equiv (pre_thms @ get_eqvts_raw_thms ctxt)
+    val all_post_thms = map safe_mk_equiv post_thms
   in
     first_conv_wrapper
-      [ Conv.rewrs_conv pre_thms,
+      [ Conv.rewrs_conv all_pre_thms,
         eqvt_apply_conv,
         eqvt_lambda_conv,
-        Conv.rewrs_conv post_thms,
-        progress_info_conv ctxt strict_flag excluded
+        Conv.rewrs_conv all_post_thms,
+        progress_info_conv ctxt strict_mode excluded
       ] ctrm
   end
 
-(* the eqvt-tactics first eta-normalise goals in 
+
+(* the eqvt-conversion first eta-normalises goals in 
    order to avoid problems with inductions in the
    equivariance command. *)
-
-(* raises an error if some permutations cannot be eliminated *)
-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
-
+fun eqvt_conv ctxt config = 
+  Conv.top_conv (fn ctxt => Thm.eta_conversion then_conv (main_eqvt_conv ctxt config)) 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)
+(* thms rewriter *)
+fun eqvt_rule ctxt config = 
+  Conv.fconv_rule (eqvt_conv ctxt config)
 
-(* 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 (eqvt_conv ctxt user_thms excluded)
+(* tactic *)
+fun eqvt_tac ctxt config = 
+  CONVERSION (eqvt_conv ctxt config)
 
 (* setup of the configuration value *)
 val setup =
@@ -183,10 +227,10 @@
 
 val args_parser =  add_thms_parser -- exclude_consts_parser 
 
-fun perm_simp_meth (thms, consts) ctxt = 
-  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
+fun perm_simp_meth (thms, consts) ctxt =
+  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts)))
 
 fun perm_strict_simp_meth (thms, consts) ctxt = 
-  SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
+  SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_strict_config addpres thms addexcls consts)))
 
 end; (* structure *)