(* 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 -> theory+ −
end;+ −
+ −
(* + −
+ −
- 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 =+ −
struct+ −
+ −
open 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_eqvt+ −
+ −
fun 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]))+ −
end+ −
+ −
fun trace_conv ctxt conv ctrm =+ −
let+ −
val result = conv ctrm+ −
in+ −
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 ctrm+ −
end+ −
+ −
(* 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+ −
] ctrm+ −
end+ −
+ −
(* 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 **)+ −
fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan+ −
+ −
val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- + −
Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) [];+ −
+ −
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 *)+ −