src/Pure/meta_simplifier.ML
author wenzelm
Mon Sep 06 21:33:19 2010 +0200 (2010-09-06)
changeset 39163 4d701c0388c3
parent 39116 f14735a88886
child 40878 7695e4de4d86
permissions -rw-r--r--
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
     1 (*  Title:      Pure/meta_simplifier.ML
     2     Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
     3 
     4 Meta-level Simplification.
     5 *)
     6 
     7 infix 4
     8   addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
     9   setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
    10   setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
    11 
    12 signature BASIC_META_SIMPLIFIER =
    13 sig
    14   val debug_simp: bool Config.T
    15   val debug_simp_raw: Config.raw
    16   val trace_simp: bool Config.T
    17   val trace_simp_raw: Config.raw
    18   val trace_simp_default: bool Unsynchronized.ref
    19   val trace_simp_depth_limit: int Unsynchronized.ref
    20   type rrule
    21   val eq_rrule: rrule * rrule -> bool
    22   type simpset
    23   type proc
    24   type solver
    25   val mk_solver': string -> (simpset -> int -> tactic) -> solver
    26   val mk_solver: string -> (thm list -> int -> tactic) -> solver
    27   val empty_ss: simpset
    28   val merge_ss: simpset * simpset -> simpset
    29   val dest_ss: simpset ->
    30    {simps: (string * thm) list,
    31     procs: (string * cterm list) list,
    32     congs: (string * thm) list,
    33     weak_congs: string list,
    34     loopers: string list,
    35     unsafe_solvers: string list,
    36     safe_solvers: string list}
    37   type simproc
    38   val eq_simproc: simproc * simproc -> bool
    39   val morph_simproc: morphism -> simproc -> simproc
    40   val make_simproc: {name: string, lhss: cterm list,
    41     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
    42   val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
    43   val add_prems: thm list -> simpset -> simpset
    44   val prems_of_ss: simpset -> thm list
    45   val addsimps: simpset * thm list -> simpset
    46   val delsimps: simpset * thm list -> simpset
    47   val addeqcongs: simpset * thm list -> simpset
    48   val deleqcongs: simpset * thm list -> simpset
    49   val addcongs: simpset * thm list -> simpset
    50   val delcongs: simpset * thm list -> simpset
    51   val addsimprocs: simpset * simproc list -> simpset
    52   val delsimprocs: simpset * simproc list -> simpset
    53   val mksimps: simpset -> thm -> thm list
    54   val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
    55   val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
    56   val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
    57   val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
    58   val settermless: simpset * (term * term -> bool) -> simpset
    59   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
    60   val setloop': simpset * (simpset -> int -> tactic) -> simpset
    61   val setloop: simpset * (int -> tactic) -> simpset
    62   val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
    63   val addloop: simpset * (string * (int -> tactic)) -> simpset
    64   val delloop: simpset * string -> simpset
    65   val setSSolver: simpset * solver -> simpset
    66   val addSSolver: simpset * solver -> simpset
    67   val setSolver: simpset * solver -> simpset
    68   val addSolver: simpset * solver -> simpset
    69 
    70   val rewrite_rule: thm list -> thm -> thm
    71   val rewrite_goals_rule: thm list -> thm -> thm
    72   val rewrite_goals_tac: thm list -> tactic
    73   val rewrite_goal_tac: thm list -> int -> tactic
    74   val rewtac: thm -> tactic
    75   val prune_params_tac: tactic
    76   val fold_rule: thm list -> thm -> thm
    77   val fold_goals_tac: thm list -> tactic
    78   val norm_hhf: thm -> thm
    79   val norm_hhf_protect: thm -> thm
    80 end;
    81 
    82 signature META_SIMPLIFIER =
    83 sig
    84   include BASIC_META_SIMPLIFIER
    85   exception SIMPLIFIER of string * thm
    86   val internal_ss: simpset ->
    87    {rules: rrule Net.net,
    88     prems: thm list,
    89     bounds: int * ((string * typ) * string) list,
    90     depth: int * bool Unsynchronized.ref,
    91     context: Proof.context option} *
    92    {congs: (string * thm) list * string list,
    93     procs: proc Net.net,
    94     mk_rews:
    95      {mk: simpset -> thm -> thm list,
    96       mk_cong: simpset -> thm -> thm,
    97       mk_sym: simpset -> thm -> thm option,
    98       mk_eq_True: simpset -> thm -> thm option,
    99       reorient: theory -> term list -> term -> term -> bool},
   100     termless: term * term -> bool,
   101     subgoal_tac: simpset -> int -> tactic,
   102     loop_tacs: (string * (simpset -> int -> tactic)) list,
   103     solvers: solver list * solver list}
   104   val add_simp: thm -> simpset -> simpset
   105   val del_simp: thm -> simpset -> simpset
   106   val solver: simpset -> solver -> int -> tactic
   107   val simp_depth_limit_raw: Config.raw
   108   val simp_depth_limit: int Config.T
   109   val clear_ss: simpset -> simpset
   110   val simproc_global_i: theory -> string -> term list
   111     -> (theory -> simpset -> term -> thm option) -> simproc
   112   val simproc_global: theory -> string -> string list
   113     -> (theory -> simpset -> term -> thm option) -> simproc
   114   val inherit_context: simpset -> simpset -> simpset
   115   val the_context: simpset -> Proof.context
   116   val context: Proof.context -> simpset -> simpset
   117   val global_context: theory  -> simpset -> simpset
   118   val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
   119   val debug_bounds: bool Unsynchronized.ref
   120   val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   121   val set_solvers: solver list -> simpset -> simpset
   122   val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
   123   val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   124   val rewrite_thm: bool * bool * bool ->
   125     (simpset -> thm -> thm option) -> simpset -> thm -> thm
   126   val rewrite_goal_rule: bool * bool * bool ->
   127     (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
   128   val asm_rewrite_goal_tac: bool * bool * bool ->
   129     (simpset -> tactic) -> simpset -> int -> tactic
   130   val rewrite: bool -> thm list -> conv
   131   val simplify: bool -> thm list -> thm -> thm
   132 end;
   133 
   134 structure MetaSimplifier: META_SIMPLIFIER =
   135 struct
   136 
   137 (** datatype simpset **)
   138 
   139 (* rewrite rules *)
   140 
   141 type rrule =
   142  {thm: thm,         (*the rewrite rule*)
   143   name: string,     (*name of theorem from which rewrite rule was extracted*)
   144   lhs: term,        (*the left-hand side*)
   145   elhs: cterm,      (*the etac-contracted lhs*)
   146   extra: bool,      (*extra variables outside of elhs*)
   147   fo: bool,         (*use first-order matching*)
   148   perm: bool};      (*the rewrite rule is permutative*)
   149 
   150 (*
   151 Remarks:
   152   - elhs is used for matching,
   153     lhs only for preservation of bound variable names;
   154   - fo is set iff
   155     either elhs is first-order (no Var is applied),
   156       in which case fo-matching is complete,
   157     or elhs is not a pattern,
   158       in which case there is nothing better to do;
   159 *)
   160 
   161 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   162   Thm.eq_thm_prop (thm1, thm2);
   163 
   164 
   165 (* simplification sets, procedures, and solvers *)
   166 
   167 (*A simpset contains data required during conversion:
   168     rules: discrimination net of rewrite rules;
   169     prems: current premises;
   170     bounds: maximal index of bound variables already used
   171       (for generating new names when rewriting under lambda abstractions);
   172     depth: simp_depth and exceeded flag;
   173     congs: association list of congruence rules and
   174            a list of `weak' congruence constants.
   175            A congruence is `weak' if it avoids normalization of some argument.
   176     procs: discrimination net of simplification procedures
   177       (functions that prove rewrite rules on the fly);
   178     mk_rews:
   179       mk: turn simplification thms into rewrite rules;
   180       mk_cong: prepare congruence rules;
   181       mk_sym: turn == around;
   182       mk_eq_True: turn P into P == True;
   183     termless: relation for ordered rewriting;*)
   184 
   185 datatype simpset =
   186   Simpset of
   187    {rules: rrule Net.net,
   188     prems: thm list,
   189     bounds: int * ((string * typ) * string) list,
   190     depth: int * bool Unsynchronized.ref,
   191     context: Proof.context option} *
   192    {congs: (string * thm) list * string list,
   193     procs: proc Net.net,
   194     mk_rews:
   195      {mk: simpset -> thm -> thm list,
   196       mk_cong: simpset -> thm -> thm,
   197       mk_sym: simpset -> thm -> thm option,
   198       mk_eq_True: simpset -> thm -> thm option,
   199       reorient: theory -> term list -> term -> term -> bool},
   200     termless: term * term -> bool,
   201     subgoal_tac: simpset -> int -> tactic,
   202     loop_tacs: (string * (simpset -> int -> tactic)) list,
   203     solvers: solver list * solver list}
   204 and proc =
   205   Proc of
   206    {name: string,
   207     lhs: cterm,
   208     proc: simpset -> cterm -> thm option,
   209     id: stamp * thm list}
   210 and solver =
   211   Solver of
   212    {name: string,
   213     solver: simpset -> int -> tactic,
   214     id: stamp};
   215 
   216 
   217 fun internal_ss (Simpset args) = args;
   218 
   219 fun make_ss1 (rules, prems, bounds, depth, context) =
   220   {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
   221 
   222 fun map_ss1 f {rules, prems, bounds, depth, context} =
   223   make_ss1 (f (rules, prems, bounds, depth, context));
   224 
   225 fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
   226   {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
   227     subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
   228 
   229 fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
   230   make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   231 
   232 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
   233 
   234 fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
   235 fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
   236 
   237 fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   238 
   239 fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
   240   s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
   241 fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
   242 
   243 fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
   244 fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
   245 
   246 fun solver_name (Solver {name, ...}) = name;
   247 fun solver ss (Solver {solver = tac, ...}) = tac ss;
   248 fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
   249 
   250 
   251 (* simp depth *)
   252 
   253 val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
   254 val simp_depth_limit = Config.int simp_depth_limit_raw;
   255 
   256 val trace_simp_depth_limit = Unsynchronized.ref 1;
   257 
   258 fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
   259   if depth > ! trace_simp_depth_limit then
   260     if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
   261   else
   262     (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
   263 
   264 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   265   (rules, prems, bounds,
   266     (depth + 1,
   267       if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
   268 
   269 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
   270 
   271 
   272 (* diagnostics *)
   273 
   274 exception SIMPLIFIER of string * thm;
   275 
   276 val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
   277 val debug_simp = Config.bool debug_simp_raw;
   278 
   279 val trace_simp_default = Unsynchronized.ref false;
   280 val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
   281 val trace_simp = Config.bool trace_simp_raw;
   282 
   283 fun if_enabled (Simpset ({context, ...}, _)) flag f =
   284   (case context of
   285     SOME ctxt => if Config.get ctxt flag then f ctxt else ()
   286   | NONE => ())
   287 
   288 fun if_visible (Simpset ({context, ...}, _)) f x =
   289   (case context of
   290     SOME ctxt => if Context_Position.is_visible ctxt then f x else ()
   291   | NONE => ());
   292 
   293 local
   294 
   295 fun prnt ss warn a = if warn then warning a else trace_depth ss a;
   296 
   297 fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
   298   let
   299     val names = Term.declare_term_names t Name.context;
   300     val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
   301     fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
   302   in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
   303 
   304 fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
   305   Syntax.string_of_term ctxt
   306     (if Config.get ctxt debug_simp then t else show_bounds ss t));
   307 
   308 in
   309 
   310 fun print_term_global ss warn a thy t =
   311   print_term ss warn (K a) t (ProofContext.init_global thy);
   312 
   313 fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
   314 fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
   315 
   316 fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
   317 fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
   318 
   319 fun trace_cterm warn a ss ct =
   320   if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
   321 
   322 fun trace_thm a ss th =
   323   if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
   324 
   325 fun trace_named_thm a ss (th, name) =
   326   if_enabled ss trace_simp (print_term ss false
   327     (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
   328     (Thm.full_prop_of th));
   329 
   330 fun warn_thm a ss th =
   331   print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
   332 
   333 fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
   334 
   335 end;
   336 
   337 
   338 
   339 (** simpset operations **)
   340 
   341 (* context *)
   342 
   343 fun eq_bound (x: string, (y, _)) = x = y;
   344 
   345 fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
   346   (rules, prems, (count + 1, bound :: bounds), depth, context));
   347 
   348 fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   349   (rules, ths @ prems, bounds, depth, context));
   350 
   351 fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
   352   map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
   353 
   354 fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
   355   | the_context _ = raise Fail "Simplifier: no proof context in simpset";
   356 
   357 fun context ctxt =
   358   map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
   359 
   360 val global_context = context o ProofContext.init_global;
   361 
   362 fun activate_context thy ss =
   363   let
   364     val ctxt = the_context ss;
   365     val ctxt' = ctxt
   366       |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
   367       |> Context_Position.set_visible false;
   368   in context ctxt' ss end;
   369 
   370 fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
   371 
   372 
   373 (* maintain simp rules *)
   374 
   375 (* FIXME: it seems that the conditions on extra variables are too liberal if
   376 prems are nonempty: does solving the prems really guarantee instantiation of
   377 all its Vars? Better: a dynamic check each time a rule is applied.
   378 *)
   379 fun rewrite_rule_extra_vars prems elhs erhs =
   380   let
   381     val elhss = elhs :: prems;
   382     val tvars = fold Term.add_tvars elhss [];
   383     val vars = fold Term.add_vars elhss [];
   384   in
   385     erhs |> Term.exists_type (Term.exists_subtype
   386       (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
   387     erhs |> Term.exists_subterm
   388       (fn Var v => not (member (op =) vars v) | _ => false)
   389   end;
   390 
   391 fun rrule_extra_vars elhs thm =
   392   rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
   393 
   394 fun mk_rrule2 {thm, name, lhs, elhs, perm} =
   395   let
   396     val t = term_of elhs;
   397     val fo = Pattern.first_order t orelse not (Pattern.pattern t);
   398     val extra = rrule_extra_vars elhs thm;
   399   in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
   400 
   401 fun del_rrule (rrule as {thm, elhs, ...}) ss =
   402   ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   403     (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
   404   handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
   405 
   406 fun insert_rrule (rrule as {thm, name, ...}) ss =
   407  (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
   408   ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   409     let
   410       val rrule2 as {elhs, ...} = mk_rrule2 rrule;
   411       val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
   412     in (rules', prems, bounds, depth, context) end)
   413   handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
   414 
   415 fun vperm (Var _, Var _) = true
   416   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   417   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   418   | vperm (t, u) = (t = u);
   419 
   420 fun var_perm (t, u) =
   421   vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
   422 
   423 (*simple test for looping rewrite rules and stupid orientations*)
   424 fun default_reorient thy prems lhs rhs =
   425   rewrite_rule_extra_vars prems lhs rhs
   426     orelse
   427   is_Var (head_of lhs)
   428     orelse
   429 (* turns t = x around, which causes a headache if x is a local variable -
   430    usually it is very useful :-(
   431   is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
   432   andalso not(exists_subterm is_Var lhs)
   433     orelse
   434 *)
   435   exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
   436     orelse
   437   null prems andalso Pattern.matches thy (lhs, rhs)
   438     (*the condition "null prems" is necessary because conditional rewrites
   439       with extra variables in the conditions may terminate although
   440       the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
   441     orelse
   442   is_Const lhs andalso not (is_Const rhs);
   443 
   444 fun decomp_simp thm =
   445   let
   446     val thy = Thm.theory_of_thm thm;
   447     val prop = Thm.prop_of thm;
   448     val prems = Logic.strip_imp_prems prop;
   449     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
   450     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
   451       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
   452     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
   453     val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
   454     val erhs = Envir.eta_contract (term_of rhs);
   455     val perm =
   456       var_perm (term_of elhs, erhs) andalso
   457       not (term_of elhs aconv erhs) andalso
   458       not (is_Var (term_of elhs));
   459   in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
   460 
   461 fun decomp_simp' thm =
   462   let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   463     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
   464     else (lhs, rhs)
   465   end;
   466 
   467 fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
   468   (case mk_eq_True ss thm of
   469     NONE => []
   470   | SOME eq_True =>
   471       let
   472         val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
   473       in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
   474 
   475 (*create the rewrite rule and possibly also the eq_True variant,
   476   in case there are extra vars on the rhs*)
   477 fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
   478   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
   479     if rewrite_rule_extra_vars [] lhs rhs then
   480       mk_eq_True ss (thm2, name) @ [rrule]
   481     else [rrule]
   482   end;
   483 
   484 fun mk_rrule ss (thm, name) =
   485   let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   486     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   487     else
   488       (*weak test for loops*)
   489       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
   490       then mk_eq_True ss (thm, name)
   491       else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   492   end;
   493 
   494 fun orient_rrule ss (thm, name) =
   495   let
   496     val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
   497     val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
   498   in
   499     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   500     else if reorient thy prems lhs rhs then
   501       if reorient thy prems rhs lhs
   502       then mk_eq_True ss (thm, name)
   503       else
   504         (case mk_sym ss thm of
   505           NONE => []
   506         | SOME thm' =>
   507             let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
   508             in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
   509     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   510   end;
   511 
   512 fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
   513   maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
   514 
   515 fun extract_safe_rrules (ss, thm) =
   516   maps (orient_rrule ss) (extract_rews (ss, [thm]));
   517 
   518 
   519 (* add/del rules explicitly *)
   520 
   521 fun comb_simps comb mk_rrule (ss, thms) =
   522   let
   523     val rews = extract_rews (ss, thms);
   524   in fold (fold comb o mk_rrule) rews ss end;
   525 
   526 fun ss addsimps thms =
   527   comb_simps insert_rrule (mk_rrule ss) (ss, thms);
   528 
   529 fun ss delsimps thms =
   530   comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
   531 
   532 fun add_simp thm ss = ss addsimps [thm];
   533 fun del_simp thm ss = ss delsimps [thm];
   534 
   535 
   536 (* congs *)
   537 
   538 fun cong_name (Const (a, _)) = SOME a
   539   | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
   540   | cong_name _ = NONE;
   541 
   542 local
   543 
   544 fun is_full_cong_prems [] [] = true
   545   | is_full_cong_prems [] _ = false
   546   | is_full_cong_prems (p :: prems) varpairs =
   547       (case Logic.strip_assums_concl p of
   548         Const ("==", _) $ lhs $ rhs =>
   549           let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
   550             is_Var x andalso forall is_Bound xs andalso
   551             not (has_duplicates (op =) xs) andalso xs = ys andalso
   552             member (op =) varpairs (x, y) andalso
   553             is_full_cong_prems prems (remove (op =) (x, y) varpairs)
   554           end
   555       | _ => false);
   556 
   557 fun is_full_cong thm =
   558   let
   559     val prems = prems_of thm and concl = concl_of thm;
   560     val (lhs, rhs) = Logic.dest_equals concl;
   561     val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   562   in
   563     f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
   564     is_full_cong_prems prems (xs ~~ ys)
   565   end;
   566 
   567 fun add_cong (ss, thm) = ss |>
   568   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   569     let
   570       val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
   571         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   572     (*val lhs = Envir.eta_contract lhs;*)
   573       val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
   574         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
   575       val (xs, weak) = congs;
   576       val _ =
   577         if AList.defined (op =) xs a
   578         then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
   579         else ();
   580       val xs' = AList.update (op =) (a, thm) xs;
   581       val weak' = if is_full_cong thm then weak else a :: weak;
   582     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   583 
   584 fun del_cong (ss, thm) = ss |>
   585   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   586     let
   587       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
   588         raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   589     (*val lhs = Envir.eta_contract lhs;*)
   590       val a = the (cong_name (head_of lhs)) handle Option.Option =>
   591         raise SIMPLIFIER ("Congruence must start with a constant", thm);
   592       val (xs, _) = congs;
   593       val xs' = filter_out (fn (x : string, _) => x = a) xs;
   594       val weak' = xs' |> map_filter (fn (a, thm) =>
   595         if is_full_cong thm then NONE else SOME a);
   596     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   597 
   598 fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
   599 
   600 in
   601 
   602 val (op addeqcongs) = Library.foldl add_cong;
   603 val (op deleqcongs) = Library.foldl del_cong;
   604 
   605 fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
   606 fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
   607 
   608 end;
   609 
   610 
   611 (* simprocs *)
   612 
   613 datatype simproc =
   614   Simproc of
   615     {name: string,
   616      lhss: cterm list,
   617      proc: morphism -> simpset -> cterm -> thm option,
   618      id: stamp * thm list};
   619 
   620 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
   621 
   622 fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
   623   Simproc
   624    {name = name,
   625     lhss = map (Morphism.cterm phi) lhss,
   626     proc = Morphism.transform phi proc,
   627     id = (s, Morphism.fact phi ths)};
   628 
   629 fun make_simproc {name, lhss, proc, identifier} =
   630   Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
   631 
   632 fun mk_simproc name lhss proc =
   633   make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
   634     proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
   635 
   636 (* FIXME avoid global thy and Logic.varify_global *)
   637 fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
   638 fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
   639 
   640 
   641 local
   642 
   643 fun add_proc (proc as Proc {name, lhs, ...}) ss =
   644  (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
   645   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   646     (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   647       mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   648   handle Net.INSERT =>
   649     (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
   650 
   651 fun del_proc (proc as Proc {name, lhs, ...}) ss =
   652   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   653     (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   654       mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   655   handle Net.DELETE =>
   656     (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
   657 
   658 fun prep_procs (Simproc {name, lhss, proc, id}) =
   659   lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
   660 
   661 in
   662 
   663 fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
   664 fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
   665 
   666 end;
   667 
   668 
   669 (* mk_rews *)
   670 
   671 local
   672 
   673 fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
   674       termless, subgoal_tac, loop_tacs, solvers) =>
   675   let
   676     val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
   677       f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
   678     val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
   679       reorient = reorient'};
   680   in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
   681 
   682 in
   683 
   684 fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
   685 
   686 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   687   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   688 
   689 fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   690   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   691 
   692 fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   693   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   694 
   695 fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   696   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   697 
   698 fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
   699   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   700 
   701 end;
   702 
   703 
   704 (* termless *)
   705 
   706 fun ss settermless termless = ss |>
   707   map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
   708    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   709 
   710 
   711 (* tactics *)
   712 
   713 fun ss setsubgoaler subgoal_tac = ss |>
   714   map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   715    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   716 
   717 fun ss setloop' tac = ss |>
   718   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
   719    (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
   720 
   721 fun ss setloop tac = ss setloop' (K tac);
   722 
   723 fun ss addloop' (name, tac) = ss |>
   724   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   725     (congs, procs, mk_rews, termless, subgoal_tac,
   726      (if AList.defined (op =) loop_tacs name
   727       then if_visible ss warning ("Overwriting looper " ^ quote name)
   728       else (); AList.update (op =) (name, tac) loop_tacs), solvers));
   729 
   730 fun ss addloop (name, tac) = ss addloop' (name, K tac);
   731 
   732 fun ss delloop name = ss |>
   733   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   734     (congs, procs, mk_rews, termless, subgoal_tac,
   735      (if AList.defined (op =) loop_tacs name then ()
   736       else if_visible ss warning ("No such looper in simpset: " ^ quote name);
   737       AList.delete (op =) name loop_tacs), solvers));
   738 
   739 fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   740   subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
   741     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
   742 
   743 fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   744   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   745     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
   746 
   747 fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   748   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
   749     subgoal_tac, loop_tacs, ([solver], solvers)));
   750 
   751 fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   752   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   753     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
   754 
   755 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
   756   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
   757   subgoal_tac, loop_tacs, (solvers, solvers)));
   758 
   759 
   760 (* empty *)
   761 
   762 fun init_ss mk_rews termless subgoal_tac solvers =
   763   make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
   764     (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
   765 
   766 fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
   767   init_ss mk_rews termless subgoal_tac solvers
   768   |> inherit_context ss;
   769 
   770 val empty_ss =
   771   init_ss
   772     {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
   773       mk_cong = K I,
   774       mk_sym = K (SOME o Drule.symmetric_fun),
   775       mk_eq_True = K (K NONE),
   776       reorient = default_reorient}
   777     Term_Ord.termless (K (K no_tac)) ([], []);
   778 
   779 
   780 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
   781 
   782 fun merge_ss (ss1, ss2) =
   783   if pointer_eq (ss1, ss2) then ss1
   784   else
   785     let
   786       val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
   787        {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
   788         loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
   789       val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
   790        {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
   791         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   792 
   793       val rules' = Net.merge eq_rrule (rules1, rules2);
   794       val prems' = Thm.merge_thms (prems1, prems2);
   795       val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
   796       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
   797       val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
   798       val weak' = merge (op =) (weak1, weak2);
   799       val procs' = Net.merge eq_proc (procs1, procs2);
   800       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
   801       val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
   802       val solvers' = merge eq_solver (solvers1, solvers2);
   803     in
   804       make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
   805         mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   806     end;
   807 
   808 
   809 (* dest_ss *)
   810 
   811 fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
   812  {simps = Net.entries rules
   813     |> map (fn {name, thm, ...} => (name, thm)),
   814   procs = Net.entries procs
   815     |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
   816     |> partition_eq (eq_snd eq_procid)
   817     |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
   818   congs = #1 congs,
   819   weak_congs = #2 congs,
   820   loopers = map fst loop_tacs,
   821   unsafe_solvers = map solver_name (#1 solvers),
   822   safe_solvers = map solver_name (#2 solvers)};
   823 
   824 
   825 
   826 (** rewriting **)
   827 
   828 (*
   829   Uses conversions, see:
   830     L C Paulson, A higher-order implementation of rewriting,
   831     Science of Computer Programming 3 (1983), pages 119-149.
   832 *)
   833 
   834 fun check_conv msg ss thm thm' =
   835   let
   836     val thm'' = Thm.transitive thm thm' handle THM _ =>
   837      Thm.transitive thm (Thm.transitive
   838        (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
   839   in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   840   handle THM _ =>
   841     let
   842       val _ $ _ $ prop0 = Thm.prop_of thm;
   843     in
   844       trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
   845       trace_term false (fn () => "Should have proved:") ss prop0;
   846       NONE
   847     end;
   848 
   849 
   850 (* mk_procrule *)
   851 
   852 fun mk_procrule ss thm =
   853   let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
   854     if rewrite_rule_extra_vars prems lhs rhs
   855     then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
   856     else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
   857   end;
   858 
   859 
   860 (* rewritec: conversion to apply the meta simpset to a term *)
   861 
   862 (*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
   863   normalized terms by carrying around the rhs of the rewrite rule just
   864   applied. This is called the `skeleton'. It is decomposed in parallel
   865   with the term. Once a Var is encountered, the corresponding term is
   866   already in normal form.
   867   skel0 is a dummy skeleton that is to enforce complete normalization.*)
   868 
   869 val skel0 = Bound 0;
   870 
   871 (*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
   872   The latter may happen iff there are weak congruence rules for constants
   873   in the lhs.*)
   874 
   875 fun uncond_skel ((_, weak), (lhs, rhs)) =
   876   if null weak then rhs  (*optimization*)
   877   else if exists_Const (member (op =) weak o #1) lhs then skel0
   878   else rhs;
   879 
   880 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   881   Otherwise those vars may become instantiated with unnormalized terms
   882   while the premises are solved.*)
   883 
   884 fun cond_skel (args as (_, (lhs, rhs))) =
   885   if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   886   else skel0;
   887 
   888 (*
   889   Rewriting -- we try in order:
   890     (1) beta reduction
   891     (2) unconditional rewrite rules
   892     (3) conditional rewrite rules
   893     (4) simplification procedures
   894 
   895   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
   896 *)
   897 
   898 fun rewritec (prover, thyt, maxt) ss t =
   899   let
   900     val ctxt = the_context ss;
   901     val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
   902     val eta_thm = Thm.eta_conversion t;
   903     val eta_t' = Thm.rhs_of eta_thm;
   904     val eta_t = term_of eta_t';
   905     fun rew {thm, name, lhs, elhs, extra, fo, perm} =
   906       let
   907         val prop = Thm.prop_of thm;
   908         val (rthm, elhs') =
   909           if maxt = ~1 orelse not extra then (thm, elhs)
   910           else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
   911         val insts =
   912           if fo then Thm.first_order_match (elhs', eta_t')
   913           else Thm.match (elhs', eta_t');
   914         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
   915         val prop' = Thm.prop_of thm';
   916         val unconditional = (Logic.count_prems prop' = 0);
   917         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   918       in
   919         if perm andalso not (termless (rhs', lhs'))
   920         then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
   921               trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
   922         else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
   923            if unconditional
   924            then
   925              (trace_thm (fn () => "Rewriting:") ss thm';
   926               let
   927                 val lr = Logic.dest_equals prop;
   928                 val SOME thm'' = check_conv false ss eta_thm thm';
   929               in SOME (thm'', uncond_skel (congs, lr)) end)
   930            else
   931              (trace_thm (fn () => "Trying to rewrite:") ss thm';
   932               if simp_depth ss > Config.get ctxt simp_depth_limit
   933               then
   934                 let
   935                   val s = "simp_depth_limit exceeded - giving up";
   936                   val _ = trace false (fn () => s) ss;
   937                   val _ = if_visible ss warning s;
   938                 in NONE end
   939               else
   940               case prover ss thm' of
   941                 NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
   942               | SOME thm2 =>
   943                   (case check_conv true ss eta_thm thm2 of
   944                      NONE => NONE |
   945                      SOME thm2' =>
   946                        let val concl = Logic.strip_imp_concl prop
   947                            val lr = Logic.dest_equals concl
   948                        in SOME (thm2', cond_skel (congs, lr)) end)))
   949       end
   950 
   951     fun rews [] = NONE
   952       | rews (rrule :: rrules) =
   953           let val opt = rew rrule handle Pattern.MATCH => NONE
   954           in case opt of NONE => rews rrules | some => some end;
   955 
   956     fun sort_rrules rrs =
   957       let
   958         fun is_simple ({thm, ...}: rrule) =
   959           (case Thm.prop_of thm of
   960             Const ("==", _) $ _ $ _ => true
   961           | _ => false);
   962         fun sort [] (re1, re2) = re1 @ re2
   963           | sort (rr :: rrs) (re1, re2) =
   964               if is_simple rr
   965               then sort rrs (rr :: re1, re2)
   966               else sort rrs (re1, rr :: re2);
   967       in sort rrs ([], []) end;
   968 
   969     fun proc_rews [] = NONE
   970       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   971           if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
   972             (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
   973              case proc ss eta_t' of
   974                NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
   975              | SOME raw_thm =>
   976                  (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
   977                    ss raw_thm;
   978                   (case rews (mk_procrule ss raw_thm) of
   979                     NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
   980                       " -- does not match") ss t; proc_rews ps)
   981                   | some => some)))
   982           else proc_rews ps;
   983   in
   984     (case eta_t of
   985       Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
   986     | _ =>
   987       (case rews (sort_rrules (Net.match_term rules eta_t)) of
   988         NONE => proc_rews (Net.match_term procs eta_t)
   989       | some => some))
   990   end;
   991 
   992 
   993 (* conversion to apply a congruence rule to a term *)
   994 
   995 fun congc prover ss maxt cong t =
   996   let val rthm = Thm.incr_indexes (maxt + 1) cong;
   997       val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   998       val insts = Thm.match (rlhs, t)
   999       (* Thm.match can raise Pattern.MATCH;
  1000          is handled when congc is called *)
  1001       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
  1002       val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
  1003       fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
  1004   in
  1005     (case prover thm' of
  1006       NONE => err ("Congruence proof failed.  Could not prove", thm')
  1007     | SOME thm2 =>
  1008         (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
  1009           NONE => err ("Congruence proof failed.  Should not have proved", thm2)
  1010         | SOME thm2' =>
  1011             if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
  1012             then NONE else SOME thm2'))
  1013   end;
  1014 
  1015 val (cA, (cB, cC)) =
  1016   apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
  1017 
  1018 fun transitive1 NONE NONE = NONE
  1019   | transitive1 (SOME thm1) NONE = SOME thm1
  1020   | transitive1 NONE (SOME thm2) = SOME thm2
  1021   | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
  1022 
  1023 fun transitive2 thm = transitive1 (SOME thm);
  1024 fun transitive3 thm = transitive1 thm o SOME;
  1025 
  1026 fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
  1027   let
  1028     fun botc skel ss t =
  1029           if is_Var skel then NONE
  1030           else
  1031           (case subc skel ss t of
  1032              some as SOME thm1 =>
  1033                (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
  1034                   SOME (thm2, skel2) =>
  1035                     transitive2 (Thm.transitive thm1 thm2)
  1036                       (botc skel2 ss (Thm.rhs_of thm2))
  1037                 | NONE => some)
  1038            | NONE =>
  1039                (case rewritec (prover, thy, maxidx) ss t of
  1040                   SOME (thm2, skel2) => transitive2 thm2
  1041                     (botc skel2 ss (Thm.rhs_of thm2))
  1042                 | NONE => NONE))
  1043 
  1044     and try_botc ss t =
  1045           (case botc skel0 ss t of
  1046              SOME trec1 => trec1 | NONE => (Thm.reflexive t))
  1047 
  1048     and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
  1049        (case term_of t0 of
  1050            Abs (a, T, _) =>
  1051              let
  1052                  val b = Name.bound (#1 bounds);
  1053                  val (v, t') = Thm.dest_abs (SOME b) t0;
  1054                  val b' = #1 (Term.dest_Free (Thm.term_of v));
  1055                  val _ =
  1056                    if b <> b' then
  1057                      warning ("Simplifier: renamed bound variable " ^
  1058                        quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
  1059                    else ();
  1060                  val ss' = add_bound ((b', T), a) ss;
  1061                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
  1062              in case botc skel' ss' t' of
  1063                   SOME thm => SOME (Thm.abstract_rule a v thm)
  1064                 | NONE => NONE
  1065              end
  1066          | t $ _ => (case t of
  1067              Const ("==>", _) $ _  => impc t0 ss
  1068            | Abs _ =>
  1069                let val thm = Thm.beta_conversion false t0
  1070                in case subc skel0 ss (Thm.rhs_of thm) of
  1071                     NONE => SOME thm
  1072                   | SOME thm' => SOME (Thm.transitive thm thm')
  1073                end
  1074            | _  =>
  1075                let fun appc () =
  1076                      let
  1077                        val (tskel, uskel) = case skel of
  1078                            tskel $ uskel => (tskel, uskel)
  1079                          | _ => (skel0, skel0);
  1080                        val (ct, cu) = Thm.dest_comb t0
  1081                      in
  1082                      (case botc tskel ss ct of
  1083                         SOME thm1 =>
  1084                           (case botc uskel ss cu of
  1085                              SOME thm2 => SOME (Thm.combination thm1 thm2)
  1086                            | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
  1087                       | NONE =>
  1088                           (case botc uskel ss cu of
  1089                              SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
  1090                            | NONE => NONE))
  1091                      end
  1092                    val (h, ts) = strip_comb t
  1093                in case cong_name h of
  1094                     SOME a =>
  1095                       (case AList.lookup (op =) (fst congs) a of
  1096                          NONE => appc ()
  1097                        | SOME cong =>
  1098   (*post processing: some partial applications h t1 ... tj, j <= length ts,
  1099     may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
  1100                           (let
  1101                              val thm = congc (prover ss) ss maxidx cong t0;
  1102                              val t = the_default t0 (Option.map Thm.rhs_of thm);
  1103                              val (cl, cr) = Thm.dest_comb t
  1104                              val dVar = Var(("", 0), dummyT)
  1105                              val skel =
  1106                                list_comb (h, replicate (length ts) dVar)
  1107                            in case botc skel ss cl of
  1108                                 NONE => thm
  1109                               | SOME thm' => transitive3 thm
  1110                                   (Thm.combination thm' (Thm.reflexive cr))
  1111                            end handle Pattern.MATCH => appc ()))
  1112                   | _ => appc ()
  1113                end)
  1114          | _ => NONE)
  1115 
  1116     and impc ct ss =
  1117       if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
  1118 
  1119     and rules_of_prem ss prem =
  1120       if maxidx_of_term (term_of prem) <> ~1
  1121       then (trace_cterm true
  1122         (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
  1123           ss prem; ([], NONE))
  1124       else
  1125         let val asm = Thm.assume prem
  1126         in (extract_safe_rrules (ss, asm), SOME asm) end
  1127 
  1128     and add_rrules (rrss, asms) ss =
  1129       (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
  1130 
  1131     and disch r prem eq =
  1132       let
  1133         val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
  1134         val eq' = Thm.implies_elim (Thm.instantiate
  1135           ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
  1136           (Thm.implies_intr prem eq)
  1137       in if not r then eq' else
  1138         let
  1139           val (prem', concl) = Thm.dest_implies lhs;
  1140           val (prem'', _) = Thm.dest_implies rhs
  1141         in Thm.transitive (Thm.transitive
  1142           (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
  1143              Drule.swap_prems_eq) eq')
  1144           (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
  1145              Drule.swap_prems_eq)
  1146         end
  1147       end
  1148 
  1149     and rebuild [] _ _ _ _ eq = eq
  1150       | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
  1151           let
  1152             val ss' = add_rrules (rev rrss, rev asms) ss;
  1153             val concl' =
  1154               Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
  1155             val dprem = Option.map (disch false prem)
  1156           in
  1157             (case rewritec (prover, thy, maxidx) ss' concl' of
  1158               NONE => rebuild prems concl' rrss asms ss (dprem eq)
  1159             | SOME (eq', _) => transitive2 (fold (disch false)
  1160                   prems (the (transitive3 (dprem eq) eq')))
  1161                 (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
  1162           end
  1163 
  1164     and mut_impc0 prems concl rrss asms ss =
  1165       let
  1166         val prems' = strip_imp_prems concl;
  1167         val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
  1168       in
  1169         mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
  1170           (asms @ asms') [] [] [] [] ss ~1 ~1
  1171       end
  1172 
  1173     and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
  1174         transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
  1175             (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
  1176           (if changed > 0 then
  1177              mut_impc (rev prems') concl (rev rrss') (rev asms')
  1178                [] [] [] [] ss ~1 changed
  1179            else rebuild prems' concl rrss' asms' ss
  1180              (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
  1181 
  1182       | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
  1183           prems' rrss' asms' eqns ss changed k =
  1184         case (if k = 0 then NONE else botc skel0 (add_rrules
  1185           (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
  1186             NONE => mut_impc prems concl rrss asms (prem :: prems')
  1187               (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
  1188               (if k = 0 then 0 else k - 1)
  1189           | SOME eqn =>
  1190             let
  1191               val prem' = Thm.rhs_of eqn;
  1192               val tprems = map term_of prems;
  1193               val i = 1 + fold Integer.max (map (fn p =>
  1194                 find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
  1195               val (rrs', asm') = rules_of_prem ss prem'
  1196             in mut_impc prems concl rrss asms (prem' :: prems')
  1197               (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
  1198                 (take i prems)
  1199                 (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
  1200                   (drop i prems, concl))))) :: eqns)
  1201                   ss (length prems') ~1
  1202             end
  1203 
  1204      (*legacy code - only for backwards compatibility*)
  1205     and nonmut_impc ct ss =
  1206       let
  1207         val (prem, conc) = Thm.dest_implies ct;
  1208         val thm1 = if simprem then botc skel0 ss prem else NONE;
  1209         val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
  1210         val ss1 =
  1211           if not useprem then ss
  1212           else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
  1213       in
  1214         (case botc skel0 ss1 conc of
  1215           NONE =>
  1216             (case thm1 of
  1217               NONE => NONE
  1218             | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
  1219         | SOME thm2 =>
  1220             let val thm2' = disch false prem1 thm2 in
  1221               (case thm1 of
  1222                 NONE => SOME thm2'
  1223               | SOME thm1' =>
  1224                  SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
  1225             end)
  1226       end
  1227 
  1228  in try_botc end;
  1229 
  1230 
  1231 (* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
  1232 
  1233 (*
  1234   Parameters:
  1235     mode = (simplify A,
  1236             use A in simplifying B,
  1237             use prems of B (if B is again a meta-impl.) to simplify A)
  1238            when simplifying A ==> B
  1239     prover: how to solve premises in conditional rewrites and congruences
  1240 *)
  1241 
  1242 val debug_bounds = Unsynchronized.ref false;
  1243 
  1244 fun check_bounds ss ct =
  1245   if ! debug_bounds then
  1246     let
  1247       val Simpset ({bounds = (_, bounds), ...}, _) = ss;
  1248       val bs = fold_aterms (fn Free (x, _) =>
  1249           if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
  1250           then insert (op =) x else I
  1251         | _ => I) (term_of ct) [];
  1252     in
  1253       if null bs then ()
  1254       else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
  1255         (Thm.theory_of_cterm ct) (Thm.term_of ct)
  1256     end
  1257   else ();
  1258 
  1259 fun rewrite_cterm mode prover raw_ss raw_ct =
  1260   let
  1261     val thy = Thm.theory_of_cterm raw_ct;
  1262     val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
  1263     val {maxidx, ...} = Thm.rep_cterm ct;
  1264     val ss = inc_simp_depth (activate_context thy raw_ss);
  1265     val depth = simp_depth ss;
  1266     val _ =
  1267       if depth mod 20 = 0 then
  1268         if_visible ss warning ("Simplification depth " ^ string_of_int depth)
  1269       else ();
  1270     val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
  1271     val _ = check_bounds ss ct;
  1272   in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
  1273 
  1274 val simple_prover =
  1275   SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
  1276 
  1277 fun rewrite _ [] ct = Thm.reflexive ct
  1278   | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
  1279       (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
  1280 
  1281 fun simplify full thms = Conv.fconv_rule (rewrite full thms);
  1282 val rewrite_rule = simplify true;
  1283 
  1284 (*simple term rewriting -- no proof*)
  1285 fun rewrite_term thy rules procs =
  1286   Pattern.rewrite_term thy (map decomp_simp' rules) procs;
  1287 
  1288 fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
  1289 
  1290 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
  1291 fun rewrite_goals_rule thms th =
  1292   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
  1293     (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
  1294 
  1295 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
  1296 fun rewrite_goal_rule mode prover ss i thm =
  1297   if 0 < i andalso i <= Thm.nprems_of thm
  1298   then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
  1299   else raise THM ("rewrite_goal_rule", i, [thm]);
  1300 
  1301 
  1302 (** meta-rewriting tactics **)
  1303 
  1304 (*Rewrite all subgoals*)
  1305 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
  1306 fun rewtac def = rewrite_goals_tac [def];
  1307 
  1308 (*Rewrite one subgoal*)
  1309 fun asm_rewrite_goal_tac mode prover_tac ss i thm =
  1310   if 0 < i andalso i <= Thm.nprems_of thm then
  1311     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
  1312   else Seq.empty;
  1313 
  1314 fun rewrite_goal_tac rews =
  1315   let val ss = empty_ss addsimps rews in
  1316     fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
  1317       (global_context (Thm.theory_of_thm st) ss) i st
  1318   end;
  1319 
  1320 (*Prunes all redundant parameters from the proof state by rewriting.
  1321   DOES NOT rewrite main goal, where quantification over an unused bound
  1322     variable is sometimes done to avoid the need for cut_facts_tac.*)
  1323 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
  1324 
  1325 
  1326 (* for folding definitions, handling critical pairs *)
  1327 
  1328 (*The depth of nesting in a term*)
  1329 fun term_depth (Abs (_, _, t)) = 1 + term_depth t
  1330   | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
  1331   | term_depth _ = 0;
  1332 
  1333 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
  1334 
  1335 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
  1336   Returns longest lhs first to avoid folding its subexpressions.*)
  1337 fun sort_lhs_depths defs =
  1338   let val keylist = AList.make (term_depth o lhs_of_thm) defs
  1339       val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
  1340   in map (AList.find (op =) keylist) keys end;
  1341 
  1342 val rev_defs = sort_lhs_depths o map Thm.symmetric;
  1343 
  1344 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
  1345 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
  1346 
  1347 
  1348 (* HHF normal form: !! before ==>, outermost !! generalized *)
  1349 
  1350 local
  1351 
  1352 fun gen_norm_hhf ss th =
  1353   (if Drule.is_norm_hhf (Thm.prop_of th) then th
  1354    else Conv.fconv_rule
  1355     (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
  1356   |> Thm.adjust_maxidx_thm ~1
  1357   |> Drule.gen_all;
  1358 
  1359 val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
  1360 
  1361 in
  1362 
  1363 val norm_hhf = gen_norm_hhf hhf_ss;
  1364 val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
  1365 
  1366 end;
  1367 
  1368 end;
  1369 
  1370 structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
  1371 open Basic_Meta_Simplifier;