(* Title: nominal_permeq.ML Author: Christian Urban Author: Brian Huffman*)signature NOMINAL_PERMEQ =sig val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic val eqvt_strict_tac: Proof.context -> thm list -> string list -> 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 val trace_eqvt: bool Config.T val setup: theory -> theoryend;(* - eqvt_tac and eqvt_strict_tac take a list of theorems which are first tried to simplify permutations 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 - setting [[trace_eqvt = true]] switches on tracing information *)structure Nominal_Permeq: NOMINAL_PERMEQ =structopen Nominal_ThmDecls;(* tracing infrastructure *)val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);fun trace_enabled ctxt = Config.get ctxt trace_eqvtfun trace_msg ctxt result = let val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))in warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))endfun trace_conv ctxt conv ctrm =let val result = conv ctrmin if Thm.is_reflexive result then result else (trace_msg ctxt result; result)end(* this conversion always fails, but prints out the analysed term *)fun trace_info_conv ctxt ctrm = let val trm = term_of ctrm val _ = case (head_of trm) of @{const "Trueprop"} => () | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)in Conv.no_conv ctrmend(* conversion for applications *)fun eqvt_apply_conv ctrm = case (term_of ctrm) of Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => let val (perm, t) = Thm.dest_comb ctrm val (_, p) = Thm.dest_comb perm val (f, x) = Thm.dest_comb t val a = ctyp_of_term x; val b = ctyp_of_term t; val ty_insts = map SOME [b, a] val term_insts = map SOME [p, f, x] in Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} end | _ => Conv.no_conv ctrm(* conversion for lambdas *)fun eqvt_lambda_conv ctrm = case (term_of ctrm) of Const (@{const_name "permute"}, _) $ _ $ (Abs _) => Conv.rewr_conv @{thm eqvt_lambda} ctrm | _ => Conv.no_conv ctrm(* conversion that raises an error or prints a warning message, if a permutation on a constant or application cannot be analysed *)fun is_excluded excluded (Const (a, _)) = member (op=) excluded a | is_excluded _ _ = false fun progress_info_conv ctxt strict_flag excluded ctrm =let fun msg trm = if is_excluded excluded trm then () else (if strict_flag then error else warning) ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) val _ = case (term_of ctrm) of Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm | _ => () in Conv.all_conv ctrm end(* main conversion *) fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =let 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}in first_conv_wrapper [ Conv.rewrs_conv pre_thms, eqvt_apply_conv, eqvt_lambda_conv, Conv.rewrs_conv post_thms, progress_info_conv ctxt strict_flag excluded ] ctrmend(* the eqvt-tactics first eta-normalise goals in order to avoid problems with inductions in the equivaraince 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)(* prints a warning message if some permutations cannot be eliminated *)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)(* setup of the configuration value *)val setup = trace_eqvt_setup(** methods **)val _ = Keyword.keyword "exclude"val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- (Scan.repeat (Args.const true))) []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_strict_simp_meth (thms, consts) ctxt = SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))end; (* structure *)