diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_permeq.ML --- 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 *)