--- 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 *)