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