(* Title: Pure/meta_simplifier.ML
ID: $Id$
Author: Tobias Nipkow and Stefan Berghofer
Meta-level Simplification.
*)
infix 4
addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
signature BASIC_META_SIMPLIFIER =
sig
val debug_simp: bool ref
val trace_simp: bool ref
val trace_simp_depth_limit: int ref
type rrule
val eq_rrule: rrule * rrule -> bool
type cong
type simpset
type proc
type solver
val mk_solver': string -> (simpset -> int -> tactic) -> solver
val mk_solver: string -> (thm list -> int -> tactic) -> solver
val rep_ss: simpset ->
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
depth: int * bool ref,
context: Proof.context option} *
{congs: (string * cong) list * string list,
procs: proc Net.net,
mk_rews:
{mk: thm -> thm list,
mk_cong: thm -> thm,
mk_sym: thm -> thm option,
mk_eq_True: thm -> thm option,
reorient: theory -> term list -> term -> term -> bool},
termless: term * term -> bool,
subgoal_tac: simpset -> int -> tactic,
loop_tacs: (string * (simpset -> int -> tactic)) list,
solvers: solver list * solver list}
val print_ss: simpset -> unit
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
type simproc
val eq_simproc: simproc * simproc -> bool
val morph_simproc: morphism -> simproc -> simproc
val make_simproc: {name: string, lhss: cterm list,
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
val add_prems: thm list -> simpset -> simpset
val prems_of_ss: simpset -> thm list
val addsimps: simpset * thm list -> simpset
val delsimps: simpset * thm list -> simpset
val addeqcongs: simpset * thm list -> simpset
val deleqcongs: simpset * thm list -> simpset
val addcongs: simpset * thm list -> simpset
val delcongs: simpset * thm list -> simpset
val addsimprocs: simpset * simproc list -> simpset
val delsimprocs: simpset * simproc list -> simpset
val setmksimps: simpset * (thm -> thm list) -> simpset
val setmkcong: simpset * (thm -> thm) -> simpset
val setmksym: simpset * (thm -> thm option) -> simpset
val setmkeqTrue: simpset * (thm -> thm option) -> simpset
val settermless: simpset * (term * term -> bool) -> simpset
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
val setloop': simpset * (simpset -> int -> tactic) -> simpset
val setloop: simpset * (int -> tactic) -> simpset
val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
val addloop: simpset * (string * (int -> tactic)) -> simpset
val delloop: simpset * string -> simpset
val setSSolver: simpset * solver -> simpset
val addSSolver: simpset * solver -> simpset
val setSolver: simpset * solver -> simpset
val addSolver: simpset * solver -> simpset
val rewrite_rule: thm list -> thm -> thm
val rewrite_goals_rule: thm list -> thm -> thm
val rewrite_goals_tac: thm list -> tactic
val rewrite_tac: thm list -> tactic
val rewrite_goal_tac: thm list -> int -> tactic
val rewtac: thm -> tactic
val prune_params_tac: tactic
val fold_rule: thm list -> thm -> thm
val fold_tac: thm list -> tactic
val fold_goals_tac: thm list -> tactic
end;
signature META_SIMPLIFIER =
sig
include BASIC_META_SIMPLIFIER
exception SIMPLIFIER of string * thm
val solver: simpset -> solver -> int -> tactic
val simp_depth_limit_value: Config.value Config.T
val simp_depth_limit: int Config.T
val clear_ss: simpset -> simpset
val simproc_i: theory -> string -> term list
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
val inherit_context: simpset -> simpset -> simpset
val the_context: simpset -> Proof.context
val context: Proof.context -> simpset -> simpset
val theory_context: theory -> simpset -> simpset
val debug_bounds: bool ref
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
val set_solvers: solver list -> simpset -> simpset
val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
val rewrite_thm: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> thm -> thm
val rewrite_goal_rule: bool * bool * bool ->
(simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
val asm_rewrite_goal_tac: bool * bool * bool ->
(simpset -> tactic) -> simpset -> int -> tactic
val norm_hhf: thm -> thm
val norm_hhf_protect: thm -> thm
val rewrite: bool -> thm list -> conv
val simplify: bool -> thm list -> thm -> thm
end;
structure MetaSimplifier: META_SIMPLIFIER =
struct
(** datatype simpset **)
(* rewrite rules *)
type rrule =
{thm: thm, (*the rewrite rule*)
name: string, (*name of theorem from which rewrite rule was extracted*)
lhs: term, (*the left-hand side*)
elhs: cterm, (*the etac-contracted lhs*)
extra: bool, (*extra variables outside of elhs*)
fo: bool, (*use first-order matching*)
perm: bool}; (*the rewrite rule is permutative*)
(*
Remarks:
- elhs is used for matching,
lhs only for preservation of bound variable names;
- fo is set iff
either elhs is first-order (no Var is applied),
in which case fo-matching is complete,
or elhs is not a pattern,
in which case there is nothing better to do;
*)
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
Thm.eq_thm_prop (thm1, thm2);
(* congruences *)
type cong = {thm: thm, lhs: cterm};
fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
Thm.eq_thm_prop (thm1, thm2);
(* simplification sets, procedures, and solvers *)
(*A simpset contains data required during conversion:
rules: discrimination net of rewrite rules;
prems: current premises;
bounds: maximal index of bound variables already used
(for generating new names when rewriting under lambda abstractions);
depth: simp_depth and exceeded flag;
congs: association list of congruence rules and
a list of `weak' congruence constants.
A congruence is `weak' if it avoids normalization of some argument.
procs: discrimination net of simplification procedures
(functions that prove rewrite rules on the fly);
mk_rews:
mk: turn simplification thms into rewrite rules;
mk_cong: prepare congruence rules;
mk_sym: turn == around;
mk_eq_True: turn P into P == True;
termless: relation for ordered rewriting;*)
type mk_rews =
{mk: thm -> thm list,
mk_cong: thm -> thm,
mk_sym: thm -> thm option,
mk_eq_True: thm -> thm option,
reorient: theory -> term list -> term -> term -> bool};
datatype simpset =
Simpset of
{rules: rrule Net.net,
prems: thm list,
bounds: int * ((string * typ) * string) list,
depth: int * bool ref,
context: Proof.context option} *
{congs: (string * cong) list * string list,
procs: proc Net.net,
mk_rews: mk_rews,
termless: term * term -> bool,
subgoal_tac: simpset -> int -> tactic,
loop_tacs: (string * (simpset -> int -> tactic)) list,
solvers: solver list * solver list}
and proc =
Proc of
{name: string,
lhs: cterm,
proc: simpset -> cterm -> thm option,
id: stamp * thm list}
and solver =
Solver of
{name: string,
solver: simpset -> int -> tactic,
id: stamp};
fun rep_ss (Simpset args) = args;
fun make_ss1 (rules, prems, bounds, depth, context) =
{rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
fun map_ss1 f {rules, prems, bounds, depth, context} =
make_ss1 (f (rules, prems, bounds, depth, context));
fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
{congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
fun map_simpset f (Simpset ({rules, prems, bounds, depth, context},
{congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
make_simpset (f ((rules, prems, bounds, depth, context),
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
fun solver_name (Solver {name, ...}) = name;
fun solver ss (Solver {solver = tac, ...}) = tac ss;
fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
(* simp depth *)
val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
val simp_depth_limit = Config.int simp_depth_limit_value;
val trace_simp_depth_limit = ref 1;
fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
if depth > ! trace_simp_depth_limit then
if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
else
(tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
(rules, prems, bounds,
(depth + 1, if depth = ! trace_simp_depth_limit then ref false else exceeded), context));
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
(* diagnostics *)
exception SIMPLIFIER of string * thm;
val debug_simp = ref false;
val trace_simp = ref false;
local
fun prnt ss warn a = if warn then warning a else trace_depth ss a;
fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
let
val names = Term.declare_term_names t Name.context;
val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
in
fun print_term ss warn a thy t = prnt ss warn (a ^ "\n" ^
Sign.string_of_term thy (if ! debug_simp then t else show_bounds ss t));
fun debug warn a ss = if ! debug_simp then prnt ss warn (a ()) else ();
fun trace warn a ss = if ! trace_simp then prnt ss warn (a ()) else ();
fun debug_term warn a ss thy t = if ! debug_simp then print_term ss warn (a ()) thy t else ();
fun trace_term warn a ss thy t = if ! trace_simp then print_term ss warn (a ()) thy t else ();
fun trace_cterm warn a ss ct =
if ! trace_simp then print_term ss warn (a ()) (Thm.theory_of_cterm ct) (Thm.term_of ct)
else ();
fun trace_thm a ss th =
if ! trace_simp then print_term ss false (a ()) (Thm.theory_of_thm th) (Thm.full_prop_of th)
else ();
fun trace_named_thm a ss (th, name) =
if ! trace_simp then
print_term ss false (if name = "" then a () else a () ^ " " ^ quote name ^ ":")
(Thm.theory_of_thm th) (Thm.full_prop_of th)
else ();
fun warn_thm a ss th =
print_term ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
if is_some context then () else warn_thm a ss th;
end;
(* print simpsets *)
fun print_ss ss =
let
val pretty_thms = map Display.pretty_thm;
fun pretty_cong (name, {thm, lhs}) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, Display.pretty_thm thm];
fun pretty_proc (name, lhss) =
Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss;
val smps = map #thm (Net.entries rules);
val prcs = Net.entries procs |>
map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
|> partition_eq (eq_snd eq_procid)
|> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps))
|> Library.sort_wrt fst;
in
[Pretty.big_list "simplification rules:" (pretty_thms smps),
Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
Pretty.big_list "congruences:" (map pretty_cong (fst congs)),
Pretty.strs ("loopers:" :: map (quote o fst) loop_tacs),
Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
|> Pretty.chunks |> Pretty.writeln
end;
(** simpset operations **)
(* context *)
fun eq_bound (x: string, (y, _)) = x = y;
fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
(rules, prems, (count + 1, bound :: bounds), depth, context));
fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
(rules, ths @ prems, bounds, depth, context));
fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
| the_context _ = raise Fail "Simplifier: no proof context in simpset";
fun context ctxt =
map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
val theory_context = context o ProofContext.init;
fun activate_context thy (ss as Simpset ({context = SOME ctxt, ...}, _)) =
context (Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt) ss
| activate_context thy ss =
(warning "Simplifier: no proof context in simpset -- fallback to theory context!";
theory_context thy ss);
(* maintain simp rules *)
(* FIXME: it seems that the conditions on extra variables are too liberal if
prems are nonempty: does solving the prems really guarantee instantiation of
all its Vars? Better: a dynamic check each time a rule is applied.
*)
fun rewrite_rule_extra_vars prems elhs erhs =
let
val elhss = elhs :: prems;
val tvars = fold Term.add_tvars elhss [];
val vars = fold Term.add_vars elhss [];
in
erhs |> Term.exists_type (Term.exists_subtype
(fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
erhs |> Term.exists_subterm
(fn Var v => not (member (op =) vars v) | _ => false)
end;
fun rrule_extra_vars elhs thm =
rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
fun mk_rrule2 {thm, name, lhs, elhs, perm} =
let
val t = term_of elhs;
val fo = Pattern.first_order t orelse not (Pattern.pattern t);
val extra = rrule_extra_vars elhs thm;
in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
fun del_rrule (rrule as {thm, elhs, ...}) ss =
ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
(Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
(trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
let
val rrule2 as {elhs, ...} = mk_rrule2 rrule;
val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
in (rules', prems, bounds, depth, context) end)
handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
fun vperm (Var _, Var _) = true
| vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
| vperm (t, u) = (t = u);
fun var_perm (t, u) =
vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
(*simple test for looping rewrite rules and stupid orientations*)
fun default_reorient thy prems lhs rhs =
rewrite_rule_extra_vars prems lhs rhs
orelse
is_Var (head_of lhs)
orelse
(* turns t = x around, which causes a headache if x is a local variable -
usually it is very useful :-(
is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
andalso not(exists_subterm is_Var lhs)
orelse
*)
exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
orelse
null prems andalso Pattern.matches thy (lhs, rhs)
(*the condition "null prems" is necessary because conditional rewrites
with extra variables in the conditions may terminate although
the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
orelse
is_Const lhs andalso not (is_Const rhs);
fun decomp_simp thm =
let
val {thy, prop, ...} = Thm.rep_thm thm;
val prems = Logic.strip_imp_prems prop;
val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*)
val erhs = Envir.eta_contract (term_of rhs);
val perm =
var_perm (term_of elhs, erhs) andalso
not (term_of elhs aconv erhs) andalso
not (is_Var (term_of elhs));
in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
fun decomp_simp' thm =
let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
else (lhs, rhs)
end;
fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
(case mk_eq_True thm of
NONE => []
| SOME eq_True =>
let
val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
val extra = rrule_extra_vars elhs eq_True;
in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
(*create the rewrite rule and possibly also the eq_True variant,
in case there are extra vars on the rhs*)
fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
if rewrite_rule_extra_vars [] lhs rhs then
mk_eq_True ss (thm2, name) @ [rrule]
else [rrule]
end;
fun mk_rrule ss (thm, name) =
let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
else
(*weak test for loops*)
if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
then mk_eq_True ss (thm, name)
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
end;
fun orient_rrule ss (thm, name) =
let
val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
else if reorient thy prems lhs rhs then
if reorient thy prems rhs lhs
then mk_eq_True ss (thm, name)
else
(case mk_sym thm of
NONE => []
| SOME thm' =>
let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
end;
fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
fun extract_safe_rrules (ss, thm) =
maps (orient_rrule ss) (extract_rews (ss, [thm]));
(* add/del rules explicitly *)
fun comb_simps comb mk_rrule (ss, thms) =
let
val rews = extract_rews (ss, thms);
in fold (fold comb o mk_rrule) rews ss end;
fun ss addsimps thms =
comb_simps insert_rrule (mk_rrule ss) (ss, thms);
fun ss delsimps thms =
comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
(* congs *)
fun cong_name (Const (a, _)) = SOME a
| cong_name (Free (a, _)) = SOME ("Free: " ^ a)
| cong_name _ = NONE;
local
fun is_full_cong_prems [] [] = true
| is_full_cong_prems [] _ = false
| is_full_cong_prems (p :: prems) varpairs =
(case Logic.strip_assums_concl p of
Const ("==", _) $ lhs $ rhs =>
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
is_Var x andalso forall is_Bound xs andalso
not (has_duplicates (op =) xs) andalso xs = ys andalso
member (op =) varpairs (x, y) andalso
is_full_cong_prems prems (remove (op =) (x, y) varpairs)
end
| _ => false);
fun is_full_cong thm =
let
val prems = prems_of thm and concl = concl_of thm;
val (lhs, rhs) = Logic.dest_equals concl;
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
in
f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
is_full_cong_prems prems (xs ~~ ys)
end;
fun add_cong (ss, thm) = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
let
val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
(*val lhs = Envir.eta_contract lhs;*)
val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
val (xs, weak) = congs;
val _ = if AList.defined (op =) xs a
then warning ("Overwriting congruence rule for " ^ quote a)
else ();
val xs' = AList.update (op =) (a, {lhs = lhs, thm = thm}) xs;
val weak' = if is_full_cong thm then weak else a :: weak;
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
fun del_cong (ss, thm) = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
let
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
raise SIMPLIFIER ("Congruence not a meta-equality", thm);
(*val lhs = Envir.eta_contract lhs;*)
val a = the (cong_name (head_of lhs)) handle Option.Option =>
raise SIMPLIFIER ("Congruence must start with a constant", thm);
val (xs, _) = congs;
val xs' = filter_out (fn (x : string, _) => x = a) xs;
val weak' = xs' |> map_filter (fn (a, {thm, ...}: cong) =>
if is_full_cong thm then NONE else SOME a);
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
in
val (op addeqcongs) = Library.foldl add_cong;
val (op deleqcongs) = Library.foldl del_cong;
fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
end;
(* simprocs *)
datatype simproc =
Simproc of
{name: string,
lhss: cterm list,
proc: morphism -> simpset -> cterm -> thm option,
id: stamp * thm list};
fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
Simproc
{name = name,
lhss = map (Morphism.cterm phi) lhss,
proc = Morphism.transform phi proc,
id = (s, Morphism.fact phi ths)};
fun make_simproc {name, lhss, proc, identifier} =
Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
fun mk_simproc name lhss proc =
make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
(* FIXME avoid global thy and Logic.varify *)
fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);
local
fun add_proc (proc as Proc {name, lhs, ...}) ss =
(trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
(congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
handle Net.INSERT =>
(warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
fun del_proc (proc as Proc {name, lhs, ...}) ss =
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
(congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
handle Net.DELETE =>
(warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
fun prep_procs (Simproc {name, lhss, proc, id}) =
lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
in
fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
end;
(* mk_rews *)
local
fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
termless, subgoal_tac, loop_tacs, solvers) =>
let
val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
reorient = reorient'};
in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
in
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
end;
(* termless *)
fun ss settermless termless = ss |>
map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
(* tactics *)
fun ss setsubgoaler subgoal_tac = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
fun ss setloop' tac = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
(congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
fun ss setloop tac = ss setloop' (K tac);
fun ss addloop' (name, tac) = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
(congs, procs, mk_rews, termless, subgoal_tac,
(if AList.defined (op =) loop_tacs name
then warning ("Overwriting looper " ^ quote name)
else (); AList.update (op =) (name, tac) loop_tacs),
solvers));
fun ss addloop (name, tac) = ss addloop' (name, K tac);
fun ss delloop name = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
(congs, procs, mk_rews, termless, subgoal_tac,
(if AList.defined (op =) loop_tacs name
then ()
else warning ("No such looper in simpset: " ^ quote name);
AList.delete (op =) name loop_tacs), solvers));
fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, ([solver], solvers)));
fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
subgoal_tac, loop_tacs, (solvers, solvers)));
(* empty *)
fun init_ss mk_rews termless subgoal_tac solvers =
make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
init_ss mk_rews termless subgoal_tac solvers
|> inherit_context ss;
val basic_mk_rews: mk_rews =
{mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
mk_cong = I,
mk_sym = SOME o Drule.symmetric_fun,
mk_eq_True = K NONE,
reorient = default_reorient};
val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
(* merge *) (*NOTE: ignores some fields of 2nd simpset*)
fun merge_ss (ss1, ss2) =
if pointer_eq (ss1, ss2) then ss1
else
let
val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
{congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
{congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
val rules' = Net.merge eq_rrule (rules1, rules2);
val prems' = merge Thm.eq_thm_prop (prems1, prems2);
val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
val procs' = Net.merge eq_proc (procs1, procs2);
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
val solvers' = merge eq_solver (solvers1, solvers2);
in
make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
end;
(** rewriting **)
(*
Uses conversions, see:
L C Paulson, A higher-order implementation of rewriting,
Science of Computer Programming 3 (1983), pages 119-149.
*)
fun check_conv msg ss thm thm' =
let
val thm'' = transitive thm (transitive
(symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
handle THM _ =>
let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
trace_term false (fn () => "Should have proved:") ss thy prop0;
NONE
end;
(* mk_procrule *)
fun mk_procrule ss thm =
let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
if rewrite_rule_extra_vars prems lhs rhs
then (warn_thm "Extra vars on rhs:" ss thm; [])
else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
end;
(* rewritec: conversion to apply the meta simpset to a term *)
(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
normalized terms by carrying around the rhs of the rewrite rule just
applied. This is called the `skeleton'. It is decomposed in parallel
with the term. Once a Var is encountered, the corresponding term is
already in normal form.
skel0 is a dummy skeleton that is to enforce complete normalization.*)
val skel0 = Bound 0;
(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
The latter may happen iff there are weak congruence rules for constants
in the lhs.*)
fun uncond_skel ((_, weak), (lhs, rhs)) =
if null weak then rhs (*optimization*)
else if exists_Const (member (op =) weak o #1) lhs then skel0
else rhs;
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
Otherwise those vars may become instantiated with unnormalized terms
while the premises are solved.*)
fun cond_skel (args as (congs, (lhs, rhs))) =
if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
else skel0;
(*
Rewriting -- we try in order:
(1) beta reduction
(2) unconditional rewrite rules
(3) conditional rewrite rules
(4) simplification procedures
IMPORTANT: rewrite rules must not introduce new Vars or TVars!
*)
fun rewritec (prover, thyt, maxt) ss t =
let
val ctxt = the_context ss;
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
val eta_thm = Thm.eta_conversion t;
val eta_t' = Thm.rhs_of eta_thm;
val eta_t = term_of eta_t';
fun rew {thm, name, lhs, elhs, extra, fo, perm} =
let
val {thy, prop, maxidx, ...} = rep_thm thm;
val (rthm, elhs') =
if maxt = ~1 orelse not extra then (thm, elhs)
else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
val insts =
if fo then Thm.first_order_match (elhs', eta_t')
else Thm.match (elhs', eta_t');
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
val prop' = Thm.prop_of thm';
val unconditional = (Logic.count_prems prop' = 0);
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
in
if perm andalso not (termless (rhs', lhs'))
then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
if unconditional
then
(trace_thm (fn () => "Rewriting:") ss thm';
let val lr = Logic.dest_equals prop;
val SOME thm'' = check_conv false ss eta_thm thm'
in SOME (thm'', uncond_skel (congs, lr)) end)
else
(trace_thm (fn () => "Trying to rewrite:") ss thm';
if simp_depth ss > Config.get ctxt simp_depth_limit
then let val s = "simp_depth_limit exceeded - giving up"
in trace false (fn () => s) ss; warning s; NONE end
else
case prover ss thm' of
NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
| SOME thm2 =>
(case check_conv true ss eta_thm thm2 of
NONE => NONE |
SOME thm2' =>
let val concl = Logic.strip_imp_concl prop
val lr = Logic.dest_equals concl
in SOME (thm2', cond_skel (congs, lr)) end)))
end
fun rews [] = NONE
| rews (rrule :: rrules) =
let val opt = rew rrule handle Pattern.MATCH => NONE
in case opt of NONE => rews rrules | some => some end;
fun sort_rrules rrs = let
fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
Const("==",_) $ _ $ _ => true
| _ => false
fun sort [] (re1,re2) = re1 @ re2
| sort (rr::rrs) (re1,re2) = if is_simple rr
then sort rrs (rr::re1,re2)
else sort rrs (re1,rr::re2)
in sort rrs ([],[]) end
fun proc_rews [] = NONE
| proc_rews (Proc {name, proc, lhs, ...} :: ps) =
if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
(debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
case proc ss eta_t' of
NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
| SOME raw_thm =>
(trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
ss raw_thm;
(case rews (mk_procrule ss raw_thm) of
NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
" -- does not match") ss t; proc_rews ps)
| some => some)))
else proc_rews ps;
in case eta_t of
Abs _ $ _ => SOME (transitive eta_thm
(beta_conversion false eta_t'), skel0)
| _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
NONE => proc_rews (Net.match_term procs eta_t)
| some => some)
end;
(* conversion to apply a congruence rule to a term *)
fun congc prover ss maxt {thm=cong,lhs=lhs} t =
let val rthm = Thm.incr_indexes (maxt + 1) cong;
val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
val insts = Thm.match (rlhs, t)
(* Thm.match can raise Pattern.MATCH;
is handled when congc is called *)
val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
in case prover thm' of
NONE => err ("Congruence proof failed. Could not prove", thm')
| SOME thm2 => (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
NONE => err ("Congruence proof failed. Should not have proved", thm2)
| SOME thm2' =>
if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
then NONE else SOME thm2')
end;
val (cA, (cB, cC)) =
apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
fun transitive1 NONE NONE = NONE
| transitive1 (SOME thm1) NONE = SOME thm1
| transitive1 NONE (SOME thm2) = SOME thm2
| transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2)
fun transitive2 thm = transitive1 (SOME thm);
fun transitive3 thm = transitive1 thm o SOME;
fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
let
fun botc skel ss t =
if is_Var skel then NONE
else
(case subc skel ss t of
some as SOME thm1 =>
(case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
SOME (thm2, skel2) =>
transitive2 (transitive thm1 thm2)
(botc skel2 ss (Thm.rhs_of thm2))
| NONE => some)
| NONE =>
(case rewritec (prover, thy, maxidx) ss t of
SOME (thm2, skel2) => transitive2 thm2
(botc skel2 ss (Thm.rhs_of thm2))
| NONE => NONE))
and try_botc ss t =
(case botc skel0 ss t of
SOME trec1 => trec1 | NONE => (reflexive t))
and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
(case term_of t0 of
Abs (a, T, t) =>
let
val b = Name.bound (#1 bounds);
val (v, t') = Thm.dest_abs (SOME b) t0;
val b' = #1 (Term.dest_Free (Thm.term_of v));
val _ =
if b <> b' then
warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
else ();
val ss' = add_bound ((b', T), a) ss;
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
in case botc skel' ss' t' of
SOME thm => SOME (abstract_rule a v thm)
| NONE => NONE
end
| t $ _ => (case t of
Const ("==>", _) $ _ => impc t0 ss
| Abs _ =>
let val thm = beta_conversion false t0
in case subc skel0 ss (Thm.rhs_of thm) of
NONE => SOME thm
| SOME thm' => SOME (transitive thm thm')
end
| _ =>
let fun appc () =
let
val (tskel, uskel) = case skel of
tskel $ uskel => (tskel, uskel)
| _ => (skel0, skel0);
val (ct, cu) = Thm.dest_comb t0
in
(case botc tskel ss ct of
SOME thm1 =>
(case botc uskel ss cu of
SOME thm2 => SOME (combination thm1 thm2)
| NONE => SOME (combination thm1 (reflexive cu)))
| NONE =>
(case botc uskel ss cu of
SOME thm1 => SOME (combination (reflexive ct) thm1)
| NONE => NONE))
end
val (h, ts) = strip_comb t
in case cong_name h of
SOME a =>
(case AList.lookup (op =) (fst congs) a of
NONE => appc ()
| SOME cong =>
(*post processing: some partial applications h t1 ... tj, j <= length ts,
may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
(let
val thm = congc (prover ss) ss maxidx cong t0;
val t = the_default t0 (Option.map Thm.rhs_of thm);
val (cl, cr) = Thm.dest_comb t
val dVar = Var(("", 0), dummyT)
val skel =
list_comb (h, replicate (length ts) dVar)
in case botc skel ss cl of
NONE => thm
| SOME thm' => transitive3 thm
(combination thm' (reflexive cr))
end handle Pattern.MATCH => appc ()))
| _ => appc ()
end)
| _ => NONE)
and impc ct ss =
if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
and rules_of_prem ss prem =
if maxidx_of_term (term_of prem) <> ~1
then (trace_cterm true
(fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
ss prem; ([], NONE))
else
let val asm = assume prem
in (extract_safe_rrules (ss, asm), SOME asm) end
and add_rrules (rrss, asms) ss =
(fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
and disch r prem eq =
let
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' = implies_elim (Thm.instantiate
([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
(implies_intr prem eq)
in if not r then eq' else
let
val (prem', concl) = Thm.dest_implies lhs;
val (prem'', _) = Thm.dest_implies rhs
in transitive (transitive
(Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
Drule.swap_prems_eq) eq')
(Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
Drule.swap_prems_eq)
end
end
and rebuild [] _ _ _ _ eq = eq
| rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq =
let
val ss' = add_rrules (rev rrss, rev asms) ss;
val concl' =
Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
val dprem = Option.map (disch false prem)
in case rewritec (prover, thy, maxidx) ss' concl' of
NONE => rebuild prems concl' rrss asms ss (dprem eq)
| SOME (eq', _) => transitive2 (fold (disch false)
prems (the (transitive3 (dprem eq) eq')))
(mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)
end
and mut_impc0 prems concl rrss asms ss =
let
val prems' = strip_imp_prems concl;
val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
(asms @ asms') [] [] [] [] ss ~1 ~1
end
and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
(Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
(if changed > 0 then
mut_impc (rev prems') concl (rev rrss') (rev asms')
[] [] [] [] ss ~1 changed
else rebuild prems' concl rrss' asms' ss
(botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
| mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
prems' rrss' asms' eqns ss changed k =
case (if k = 0 then NONE else botc skel0 (add_rrules
(rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
NONE => mut_impc prems concl rrss asms (prem :: prems')
(rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
(if k = 0 then 0 else k - 1)
| SOME eqn =>
let
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
val i = 1 + Library.foldl Int.max (~1, map (fn p =>
find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
(Library.take (i, prems))
(Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
(Library.drop (i, prems), concl))))) :: eqns)
ss (length prems') ~1
end
(*legacy code - only for backwards compatibility*)
and nonmut_impc ct ss =
let val (prem, conc) = Thm.dest_implies ct;
val thm1 = if simprem then botc skel0 ss prem else NONE;
val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
val ss1 = if not useprem then ss else add_rrules
(apsnd single (apfst single (rules_of_prem ss prem1))) ss
in (case botc skel0 ss1 conc of
NONE => (case thm1 of
NONE => NONE
| SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
| SOME thm2 =>
let val thm2' = disch false prem1 thm2
in (case thm1 of
NONE => SOME thm2'
| SOME thm1' =>
SOME (transitive (Drule.imp_cong_rule thm1' (reflexive conc)) thm2'))
end)
end
in try_botc end;
(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
(*
Parameters:
mode = (simplify A,
use A in simplifying B,
use prems of B (if B is again a meta-impl.) to simplify A)
when simplifying A ==> B
prover: how to solve premises in conditional rewrites and congruences
*)
val debug_bounds = ref false;
fun check_bounds ss ct =
if ! debug_bounds then
let
val Simpset ({bounds = (_, bounds), ...}, _) = ss;
val bs = fold_aterms (fn Free (x, _) =>
if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
then insert (op =) x else I
| _ => I) (term_of ct) [];
in
if null bs then ()
else print_term ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
(Thm.theory_of_cterm ct) (Thm.term_of ct)
end
else ();
fun rewrite_cterm mode prover raw_ss raw_ct =
let
val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
val ss = inc_simp_depth (activate_context thy raw_ss);
val depth = simp_depth ss;
val _ =
if depth mod 20 = 0 then
warning ("Simplification depth " ^ string_of_int depth)
else ();
val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
val _ = check_bounds ss ct;
in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
val simple_prover =
SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
(*Rewrite a cterm*)
fun rewrite _ [] ct = Thm.reflexive ct
| rewrite full thms ct =
rewrite_cterm (full, false, false) simple_prover
(theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
(*Rewrite a theorem*)
fun simplify full thms = Conv.fconv_rule (rewrite full thms);
val rewrite_rule = simplify true;
(*simple term rewriting -- no proof*)
fun rewrite_term thy rules procs =
Pattern.rewrite_term thy (map decomp_simp' rules) procs;
fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
(*Rewrite the subgoals of a proof state (represented by a theorem)*)
fun rewrite_goals_rule thms th =
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
(theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
(*Rewrite the subgoal of a proof state (represented by a theorem)*)
fun rewrite_goal_rule mode prover ss i thm =
if 0 < i andalso i <= Thm.nprems_of thm
then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
else raise THM ("rewrite_goal_rule", i, [thm]);
(** meta-rewriting tactics **)
(*Rewrite throughout proof state. *)
fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs);
(*Rewrite subgoals only, not main goal. *)
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
fun rewtac def = rewrite_goals_tac [def];
(*Rewrite subgoal i only.*)
fun asm_rewrite_goal_tac mode prover_tac ss i =
PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss i);
fun rewrite_goal_tac rews =
let val ss = empty_ss addsimps rews in
fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
(theory_context (Thm.theory_of_thm st) ss) i st
end;
(*Prunes all redundant parameters from the proof state by rewriting.
DOES NOT rewrite main goal, where quantification over an unused bound
variable is sometimes done to avoid the need for cut_facts_tac.*)
val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
(* for folding definitions, handling critical pairs *)
(*The depth of nesting in a term*)
fun term_depth (Abs(a,T,t)) = 1 + term_depth t
| term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
| term_depth _ = 0;
val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
Returns longest lhs first to avoid folding its subexpressions.*)
fun sort_lhs_depths defs =
let val keylist = AList.make (term_depth o lhs_of_thm) defs
val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
in map (AList.find (op =) keylist) keys end;
val rev_defs = sort_lhs_depths o map symmetric;
fun fold_rule defs = fold rewrite_rule (rev_defs defs);
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
(* HHF normal form: !! before ==>, outermost !! generalized *)
local
fun gen_norm_hhf ss th =
(if Drule.is_norm_hhf (Thm.prop_of th) then th
else Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
|> Thm.adjust_maxidx_thm ~1
|> Drule.gen_all;
val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
in
val norm_hhf = gen_norm_hhf ss;
val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
end;
end;
structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
open BasicMetaSimplifier;