src/Pure/meta_simplifier.ML
author wenzelm
Mon Apr 07 21:29:46 2008 +0200 (2008-04-07)
changeset 26572 9178a7f4c4c8
parent 26424 a6cad32a27b0
child 26626 c6231d64d264
permissions -rw-r--r--
prefer plain ASCII 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   Sign.string_of_term 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      (warning "Simplifier: no proof context in simpset -- fallback to theory context!";
   385       theory_context thy ss);
   386 
   387 
   388 (* maintain simp rules *)
   389 
   390 (* FIXME: it seems that the conditions on extra variables are too liberal if
   391 prems are nonempty: does solving the prems really guarantee instantiation of
   392 all its Vars? Better: a dynamic check each time a rule is applied.
   393 *)
   394 fun rewrite_rule_extra_vars prems elhs erhs =
   395   let
   396     val elhss = elhs :: prems;
   397     val tvars = fold Term.add_tvars elhss [];
   398     val vars = fold Term.add_vars elhss [];
   399   in
   400     erhs |> Term.exists_type (Term.exists_subtype
   401       (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
   402     erhs |> Term.exists_subterm
   403       (fn Var v => not (member (op =) vars v) | _ => false)
   404   end;
   405 
   406 fun rrule_extra_vars elhs thm =
   407   rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
   408 
   409 fun mk_rrule2 {thm, name, lhs, elhs, perm} =
   410   let
   411     val t = term_of elhs;
   412     val fo = Pattern.first_order t orelse not (Pattern.pattern t);
   413     val extra = rrule_extra_vars elhs thm;
   414   in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
   415 
   416 fun del_rrule (rrule as {thm, elhs, ...}) ss =
   417   ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   418     (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
   419   handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
   420 
   421 fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
   422  (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
   423   ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
   424     let
   425       val rrule2 as {elhs, ...} = mk_rrule2 rrule;
   426       val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
   427     in (rules', prems, bounds, depth, context) end)
   428   handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
   429 
   430 fun vperm (Var _, Var _) = true
   431   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   432   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   433   | vperm (t, u) = (t = u);
   434 
   435 fun var_perm (t, u) =
   436   vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
   437 
   438 (*simple test for looping rewrite rules and stupid orientations*)
   439 fun default_reorient thy prems lhs rhs =
   440   rewrite_rule_extra_vars prems lhs rhs
   441     orelse
   442   is_Var (head_of lhs)
   443     orelse
   444 (* turns t = x around, which causes a headache if x is a local variable -
   445    usually it is very useful :-(
   446   is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
   447   andalso not(exists_subterm is_Var lhs)
   448     orelse
   449 *)
   450   exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
   451     orelse
   452   null prems andalso Pattern.matches thy (lhs, rhs)
   453     (*the condition "null prems" is necessary because conditional rewrites
   454       with extra variables in the conditions may terminate although
   455       the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
   456     orelse
   457   is_Const lhs andalso not (is_Const rhs);
   458 
   459 fun decomp_simp thm =
   460   let
   461     val {thy, prop, ...} = Thm.rep_thm thm;
   462     val prems = Logic.strip_imp_prems prop;
   463     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
   464     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
   465       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
   466     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
   467     val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
   468     val erhs = Envir.eta_contract (term_of rhs);
   469     val perm =
   470       var_perm (term_of elhs, erhs) andalso
   471       not (term_of elhs aconv erhs) andalso
   472       not (is_Var (term_of elhs));
   473   in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
   474 
   475 fun decomp_simp' thm =
   476   let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   477     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
   478     else (lhs, rhs)
   479   end;
   480 
   481 fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
   482   (case mk_eq_True thm of
   483     NONE => []
   484   | SOME eq_True =>
   485       let
   486         val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
   487         val extra = rrule_extra_vars elhs eq_True;
   488       in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
   489 
   490 (*create the rewrite rule and possibly also the eq_True variant,
   491   in case there are extra vars on the rhs*)
   492 fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
   493   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
   494     if rewrite_rule_extra_vars [] lhs rhs then
   495       mk_eq_True ss (thm2, name) @ [rrule]
   496     else [rrule]
   497   end;
   498 
   499 fun mk_rrule ss (thm, name) =
   500   let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   501     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   502     else
   503       (*weak test for loops*)
   504       if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
   505       then mk_eq_True ss (thm, name)
   506       else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   507   end;
   508 
   509 fun orient_rrule ss (thm, name) =
   510   let
   511     val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
   512     val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
   513   in
   514     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   515     else if reorient thy prems lhs rhs then
   516       if reorient thy prems rhs lhs
   517       then mk_eq_True ss (thm, name)
   518       else
   519         (case mk_sym thm of
   520           NONE => []
   521         | SOME thm' =>
   522             let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
   523             in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
   524     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   525   end;
   526 
   527 fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
   528   maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
   529 
   530 fun extract_safe_rrules (ss, thm) =
   531   maps (orient_rrule ss) (extract_rews (ss, [thm]));
   532 
   533 
   534 (* add/del rules explicitly *)
   535 
   536 fun comb_simps comb mk_rrule (ss, thms) =
   537   let
   538     val rews = extract_rews (ss, thms);
   539   in fold (fold comb o mk_rrule) rews ss end;
   540 
   541 fun ss addsimps thms =
   542   comb_simps insert_rrule (mk_rrule ss) (ss, thms);
   543 
   544 fun ss delsimps thms =
   545   comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
   546 
   547 
   548 (* congs *)
   549 
   550 fun cong_name (Const (a, _)) = SOME a
   551   | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
   552   | cong_name _ = NONE;
   553 
   554 local
   555 
   556 fun is_full_cong_prems [] [] = true
   557   | is_full_cong_prems [] _ = false
   558   | is_full_cong_prems (p :: prems) varpairs =
   559       (case Logic.strip_assums_concl p of
   560         Const ("==", _) $ lhs $ rhs =>
   561           let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
   562             is_Var x andalso forall is_Bound xs andalso
   563             not (has_duplicates (op =) xs) andalso xs = ys andalso
   564             member (op =) varpairs (x, y) andalso
   565             is_full_cong_prems prems (remove (op =) (x, y) varpairs)
   566           end
   567       | _ => false);
   568 
   569 fun is_full_cong thm =
   570   let
   571     val prems = prems_of thm and concl = concl_of thm;
   572     val (lhs, rhs) = Logic.dest_equals concl;
   573     val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   574   in
   575     f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
   576     is_full_cong_prems prems (xs ~~ ys)
   577   end;
   578 
   579 fun add_cong (ss, thm) = ss |>
   580   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   581     let
   582       val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
   583         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   584     (*val lhs = Envir.eta_contract lhs;*)
   585       val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
   586         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
   587       val (xs, weak) = congs;
   588       val _ =  if AList.defined (op =) xs a
   589         then warning ("Overwriting congruence rule for " ^ quote a)
   590         else ();
   591       val xs' = AList.update (op =) (a, {lhs = lhs, thm = thm}) xs;
   592       val weak' = if is_full_cong thm then weak else a :: weak;
   593     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   594 
   595 fun del_cong (ss, thm) = ss |>
   596   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   597     let
   598       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
   599         raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   600     (*val lhs = Envir.eta_contract lhs;*)
   601       val a = the (cong_name (head_of lhs)) handle Option.Option =>
   602         raise SIMPLIFIER ("Congruence must start with a constant", thm);
   603       val (xs, _) = congs;
   604       val xs' = filter_out (fn (x : string, _) => x = a) xs;
   605       val weak' = xs' |> map_filter (fn (a, {thm, ...}: cong) =>
   606         if is_full_cong thm then NONE else SOME a);
   607     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   608 
   609 fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
   610 
   611 in
   612 
   613 val (op addeqcongs) = Library.foldl add_cong;
   614 val (op deleqcongs) = Library.foldl del_cong;
   615 
   616 fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
   617 fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
   618 
   619 end;
   620 
   621 
   622 (* simprocs *)
   623 
   624 datatype simproc =
   625   Simproc of
   626     {name: string,
   627      lhss: cterm list,
   628      proc: morphism -> simpset -> cterm -> thm option,
   629      id: stamp * thm list};
   630 
   631 fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
   632 
   633 fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
   634   Simproc
   635    {name = name,
   636     lhss = map (Morphism.cterm phi) lhss,
   637     proc = Morphism.transform phi proc,
   638     id = (s, Morphism.fact phi ths)};
   639 
   640 fun make_simproc {name, lhss, proc, identifier} =
   641   Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
   642 
   643 fun mk_simproc name lhss proc =
   644   make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
   645     proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
   646 
   647 (* FIXME avoid global thy and Logic.varify *)
   648 fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
   649 fun simproc thy name = simproc_i thy name o map (Syntax.read_term_global thy);
   650 
   651 
   652 local
   653 
   654 fun add_proc (proc as Proc {name, lhs, ...}) ss =
   655  (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
   656   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   657     (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
   658       mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   659   handle Net.INSERT =>
   660     (warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
   661 
   662 fun del_proc (proc as Proc {name, lhs, ...}) ss =
   663   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   664     (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
   665       mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   666   handle Net.DELETE =>
   667     (warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
   668 
   669 fun prep_procs (Simproc {name, lhss, proc, id}) =
   670   lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
   671 
   672 in
   673 
   674 fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
   675 fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
   676 
   677 end;
   678 
   679 
   680 (* mk_rews *)
   681 
   682 local
   683 
   684 fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
   685       termless, subgoal_tac, loop_tacs, solvers) =>
   686   let
   687     val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
   688       f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
   689     val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
   690       reorient = reorient'};
   691   in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
   692 
   693 in
   694 
   695 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
   696   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   697 
   698 fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
   699   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   700 
   701 fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
   702   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   703 
   704 fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
   705   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   706 
   707 fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
   708   (mk, mk_cong, mk_sym, mk_eq_True, reorient));
   709 
   710 end;
   711 
   712 
   713 (* termless *)
   714 
   715 fun ss settermless termless = ss |>
   716   map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
   717    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   718 
   719 
   720 (* tactics *)
   721 
   722 fun ss setsubgoaler subgoal_tac = ss |>
   723   map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   724    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   725 
   726 fun ss setloop' tac = ss |>
   727   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
   728    (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
   729 
   730 fun ss setloop tac = ss setloop' (K tac);
   731 
   732 fun ss addloop' (name, tac) = 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
   736         then warning ("Overwriting looper " ^ quote name)
   737         else (); AList.update (op =) (name, tac) loop_tacs),
   738       solvers));
   739 
   740 fun ss addloop (name, tac) = ss addloop' (name, K tac);
   741 
   742 fun ss delloop name = ss |>
   743   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   744     (congs, procs, mk_rews, termless, subgoal_tac,
   745       (if AList.defined (op =) loop_tacs name
   746         then ()
   747         else warning ("No such looper in simpset: " ^ quote name);
   748        AList.delete (op =) name loop_tacs), solvers));
   749 
   750 fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   751   subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
   752     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
   753 
   754 fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   755   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   756     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
   757 
   758 fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   759   subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
   760     subgoal_tac, loop_tacs, ([solver], solvers)));
   761 
   762 fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
   763   subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
   764     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
   765 
   766 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
   767   subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
   768   subgoal_tac, loop_tacs, (solvers, solvers)));
   769 
   770 
   771 (* empty *)
   772 
   773 fun init_ss mk_rews termless subgoal_tac solvers =
   774   make_simpset ((Net.empty, [], (0, []), (0, ref false), NONE),
   775     (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
   776 
   777 fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
   778   init_ss mk_rews termless subgoal_tac solvers
   779   |> inherit_context ss;
   780 
   781 val basic_mk_rews: mk_rews =
   782  {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
   783   mk_cong = I,
   784   mk_sym = SOME o Drule.symmetric_fun,
   785   mk_eq_True = K NONE,
   786   reorient = default_reorient};
   787 
   788 val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
   789 
   790 
   791 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
   792 
   793 fun merge_ss (ss1, ss2) =
   794   if pointer_eq (ss1, ss2) then ss1
   795   else
   796     let
   797       val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
   798        {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
   799         loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
   800       val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
   801        {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
   802         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   803   
   804       val rules' = Net.merge eq_rrule (rules1, rules2);
   805       val prems' = merge Thm.eq_thm_prop (prems1, prems2);
   806       val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
   807       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
   808       val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
   809       val weak' = merge (op =) (weak1, weak2);
   810       val procs' = Net.merge eq_proc (procs1, procs2);
   811       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
   812       val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
   813       val solvers' = merge eq_solver (solvers1, solvers2);
   814     in
   815       make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
   816         mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   817     end;
   818 
   819 
   820 
   821 (** rewriting **)
   822 
   823 (*
   824   Uses conversions, see:
   825     L C Paulson, A higher-order implementation of rewriting,
   826     Science of Computer Programming 3 (1983), pages 119-149.
   827 *)
   828 
   829 fun check_conv msg ss thm thm' =
   830   let
   831     val thm'' = transitive thm thm' handle THM _ =>
   832      transitive thm (transitive
   833        (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
   834   in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
   835   handle THM _ =>
   836     let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
   837       trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
   838       trace_term false (fn () => "Should have proved:") ss thy prop0;
   839       NONE
   840     end;
   841 
   842 
   843 (* mk_procrule *)
   844 
   845 fun mk_procrule ss thm =
   846   let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
   847     if rewrite_rule_extra_vars prems lhs rhs
   848     then (warn_thm "Extra vars on rhs:" ss thm; [])
   849     else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
   850   end;
   851 
   852 
   853 (* rewritec: conversion to apply the meta simpset to a term *)
   854 
   855 (*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
   856   normalized terms by carrying around the rhs of the rewrite rule just
   857   applied. This is called the `skeleton'. It is decomposed in parallel
   858   with the term. Once a Var is encountered, the corresponding term is
   859   already in normal form.
   860   skel0 is a dummy skeleton that is to enforce complete normalization.*)
   861 
   862 val skel0 = Bound 0;
   863 
   864 (*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
   865   The latter may happen iff there are weak congruence rules for constants
   866   in the lhs.*)
   867 
   868 fun uncond_skel ((_, weak), (lhs, rhs)) =
   869   if null weak then rhs  (*optimization*)
   870   else if exists_Const (member (op =) weak o #1) lhs then skel0
   871   else rhs;
   872 
   873 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   874   Otherwise those vars may become instantiated with unnormalized terms
   875   while the premises are solved.*)
   876 
   877 fun cond_skel (args as (congs, (lhs, rhs))) =
   878   if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
   879   else skel0;
   880 
   881 (*
   882   Rewriting -- we try in order:
   883     (1) beta reduction
   884     (2) unconditional rewrite rules
   885     (3) conditional rewrite rules
   886     (4) simplification procedures
   887 
   888   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
   889 *)
   890 
   891 fun rewritec (prover, thyt, maxt) ss t =
   892   let
   893     val ctxt = the_context ss;
   894     val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
   895     val eta_thm = Thm.eta_conversion t;
   896     val eta_t' = Thm.rhs_of eta_thm;
   897     val eta_t = term_of eta_t';
   898     fun rew {thm, name, lhs, elhs, extra, fo, perm} =
   899       let
   900         val {thy, prop, maxidx, ...} = rep_thm thm;
   901         val (rthm, elhs') =
   902           if maxt = ~1 orelse not extra then (thm, elhs)
   903           else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
   904         val insts =
   905           if fo then Thm.first_order_match (elhs', eta_t')
   906           else Thm.match (elhs', eta_t');
   907         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
   908         val prop' = Thm.prop_of thm';
   909         val unconditional = (Logic.count_prems prop' = 0);
   910         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   911       in
   912         if perm andalso not (termless (rhs', lhs'))
   913         then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
   914               trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
   915         else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
   916            if unconditional
   917            then
   918              (trace_thm (fn () => "Rewriting:") ss thm';
   919               let val lr = Logic.dest_equals prop;
   920                   val SOME thm'' = check_conv false ss eta_thm thm'
   921               in SOME (thm'', uncond_skel (congs, lr)) end)
   922            else
   923              (trace_thm (fn () => "Trying to rewrite:") ss thm';
   924               if simp_depth ss > Config.get ctxt simp_depth_limit
   925               then let val s = "simp_depth_limit exceeded - giving up"
   926                    in trace false (fn () => s) ss; warning s; NONE end
   927               else
   928               case prover ss thm' of
   929                 NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
   930               | SOME thm2 =>
   931                   (case check_conv true ss eta_thm thm2 of
   932                      NONE => NONE |
   933                      SOME thm2' =>
   934                        let val concl = Logic.strip_imp_concl prop
   935                            val lr = Logic.dest_equals concl
   936                        in SOME (thm2', cond_skel (congs, lr)) end)))
   937       end
   938 
   939     fun rews [] = NONE
   940       | rews (rrule :: rrules) =
   941           let val opt = rew rrule handle Pattern.MATCH => NONE
   942           in case opt of NONE => rews rrules | some => some end;
   943 
   944     fun sort_rrules rrs = let
   945       fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
   946                                       Const("==",_) $ _ $ _ => true
   947                                       | _                   => false
   948       fun sort []        (re1,re2) = re1 @ re2
   949         | sort (rr::rrs) (re1,re2) = if is_simple rr
   950                                      then sort rrs (rr::re1,re2)
   951                                      else sort rrs (re1,rr::re2)
   952     in sort rrs ([],[]) end
   953 
   954     fun proc_rews [] = NONE
   955       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   956           if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
   957             (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss thyt eta_t;
   958              case proc ss eta_t' of
   959                NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
   960              | SOME raw_thm =>
   961                  (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
   962                    ss raw_thm;
   963                   (case rews (mk_procrule ss raw_thm) of
   964                     NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
   965                       " -- does not match") ss t; proc_rews ps)
   966                   | some => some)))
   967           else proc_rews ps;
   968   in case eta_t of
   969        Abs _ $ _ => SOME (transitive eta_thm
   970          (beta_conversion false eta_t'), skel0)
   971      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   972                NONE => proc_rews (Net.match_term procs eta_t)
   973              | some => some)
   974   end;
   975 
   976 
   977 (* conversion to apply a congruence rule to a term *)
   978 
   979 fun congc prover ss maxt {thm=cong,lhs=lhs} t =
   980   let val rthm = Thm.incr_indexes (maxt + 1) cong;
   981       val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   982       val insts = Thm.match (rlhs, t)
   983       (* Thm.match can raise Pattern.MATCH;
   984          is handled when congc is called *)
   985       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   986       val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
   987       fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
   988   in case prover thm' of
   989        NONE => err ("Congruence proof failed.  Could not prove", thm')
   990      | SOME thm2 => (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
   991           NONE => err ("Congruence proof failed.  Should not have proved", thm2)
   992         | SOME thm2' =>
   993             if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
   994             then NONE else SOME thm2')
   995   end;
   996 
   997 val (cA, (cB, cC)) =
   998   apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
   999 
  1000 fun transitive1 NONE NONE = NONE
  1001   | transitive1 (SOME thm1) NONE = SOME thm1
  1002   | transitive1 NONE (SOME thm2) = SOME thm2
  1003   | transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2)
  1004 
  1005 fun transitive2 thm = transitive1 (SOME thm);
  1006 fun transitive3 thm = transitive1 thm o SOME;
  1007 
  1008 fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
  1009   let
  1010     fun botc skel ss t =
  1011           if is_Var skel then NONE
  1012           else
  1013           (case subc skel ss t of
  1014              some as SOME thm1 =>
  1015                (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
  1016                   SOME (thm2, skel2) =>
  1017                     transitive2 (transitive thm1 thm2)
  1018                       (botc skel2 ss (Thm.rhs_of thm2))
  1019                 | NONE => some)
  1020            | NONE =>
  1021                (case rewritec (prover, thy, maxidx) ss t of
  1022                   SOME (thm2, skel2) => transitive2 thm2
  1023                     (botc skel2 ss (Thm.rhs_of thm2))
  1024                 | NONE => NONE))
  1025 
  1026     and try_botc ss t =
  1027           (case botc skel0 ss t of
  1028              SOME trec1 => trec1 | NONE => (reflexive t))
  1029 
  1030     and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
  1031        (case term_of t0 of
  1032            Abs (a, T, t) =>
  1033              let
  1034                  val b = Name.bound (#1 bounds);
  1035                  val (v, t') = Thm.dest_abs (SOME b) t0;
  1036                  val b' = #1 (Term.dest_Free (Thm.term_of v));
  1037                  val _ =
  1038                    if b <> b' then
  1039                      warning ("Simplifier: renamed bound variable " ^ quote b ^ " to " ^ quote b')
  1040                    else ();
  1041                  val ss' = add_bound ((b', T), a) ss;
  1042                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
  1043              in case botc skel' ss' t' of
  1044                   SOME thm => SOME (abstract_rule a v thm)
  1045                 | NONE => NONE
  1046              end
  1047          | t $ _ => (case t of
  1048              Const ("==>", _) $ _  => impc t0 ss
  1049            | Abs _ =>
  1050                let val thm = beta_conversion false t0
  1051                in case subc skel0 ss (Thm.rhs_of thm) of
  1052                     NONE => SOME thm
  1053                   | SOME thm' => SOME (transitive thm thm')
  1054                end
  1055            | _  =>
  1056                let fun appc () =
  1057                      let
  1058                        val (tskel, uskel) = case skel of
  1059                            tskel $ uskel => (tskel, uskel)
  1060                          | _ => (skel0, skel0);
  1061                        val (ct, cu) = Thm.dest_comb t0
  1062                      in
  1063                      (case botc tskel ss ct of
  1064                         SOME thm1 =>
  1065                           (case botc uskel ss cu of
  1066                              SOME thm2 => SOME (combination thm1 thm2)
  1067                            | NONE => SOME (combination thm1 (reflexive cu)))
  1068                       | NONE =>
  1069                           (case botc uskel ss cu of
  1070                              SOME thm1 => SOME (combination (reflexive ct) thm1)
  1071                            | NONE => NONE))
  1072                      end
  1073                    val (h, ts) = strip_comb t
  1074                in case cong_name h of
  1075                     SOME a =>
  1076                       (case AList.lookup (op =) (fst congs) a of
  1077                          NONE => appc ()
  1078                        | SOME cong =>
  1079   (*post processing: some partial applications h t1 ... tj, j <= length ts,
  1080     may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
  1081                           (let
  1082                              val thm = congc (prover ss) ss maxidx cong t0;
  1083                              val t = the_default t0 (Option.map Thm.rhs_of thm);
  1084                              val (cl, cr) = Thm.dest_comb t
  1085                              val dVar = Var(("", 0), dummyT)
  1086                              val skel =
  1087                                list_comb (h, replicate (length ts) dVar)
  1088                            in case botc skel ss cl of
  1089                                 NONE => thm
  1090                               | SOME thm' => transitive3 thm
  1091                                   (combination thm' (reflexive cr))
  1092                            end handle Pattern.MATCH => appc ()))
  1093                   | _ => appc ()
  1094                end)
  1095          | _ => NONE)
  1096 
  1097     and impc ct ss =
  1098       if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
  1099 
  1100     and rules_of_prem ss prem =
  1101       if maxidx_of_term (term_of prem) <> ~1
  1102       then (trace_cterm true
  1103         (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
  1104           ss prem; ([], NONE))
  1105       else
  1106         let val asm = assume prem
  1107         in (extract_safe_rrules (ss, asm), SOME asm) end
  1108 
  1109     and add_rrules (rrss, asms) ss =
  1110       (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
  1111 
  1112     and disch r prem eq =
  1113       let
  1114         val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
  1115         val eq' = implies_elim (Thm.instantiate
  1116           ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
  1117           (implies_intr prem eq)
  1118       in if not r then eq' else
  1119         let
  1120           val (prem', concl) = Thm.dest_implies lhs;
  1121           val (prem'', _) = Thm.dest_implies rhs
  1122         in transitive (transitive
  1123           (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
  1124              Drule.swap_prems_eq) eq')
  1125           (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
  1126              Drule.swap_prems_eq)
  1127         end
  1128       end
  1129 
  1130     and rebuild [] _ _ _ _ eq = eq
  1131       | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq =
  1132           let
  1133             val ss' = add_rrules (rev rrss, rev asms) ss;
  1134             val concl' =
  1135               Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
  1136             val dprem = Option.map (disch false prem)
  1137           in case rewritec (prover, thy, maxidx) ss' concl' of
  1138               NONE => rebuild prems concl' rrss asms ss (dprem eq)
  1139             | SOME (eq', _) => transitive2 (fold (disch false)
  1140                   prems (the (transitive3 (dprem eq) eq')))
  1141                 (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)
  1142           end
  1143 
  1144     and mut_impc0 prems concl rrss asms ss =
  1145       let
  1146         val prems' = strip_imp_prems concl;
  1147         val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
  1148       in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
  1149         (asms @ asms') [] [] [] [] ss ~1 ~1
  1150       end
  1151 
  1152     and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
  1153         transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
  1154             (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
  1155           (if changed > 0 then
  1156              mut_impc (rev prems') concl (rev rrss') (rev asms')
  1157                [] [] [] [] ss ~1 changed
  1158            else rebuild prems' concl rrss' asms' ss
  1159              (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
  1160 
  1161       | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
  1162           prems' rrss' asms' eqns ss changed k =
  1163         case (if k = 0 then NONE else botc skel0 (add_rrules
  1164           (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
  1165             NONE => mut_impc prems concl rrss asms (prem :: prems')
  1166               (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
  1167               (if k = 0 then 0 else k - 1)
  1168           | SOME eqn =>
  1169             let
  1170               val prem' = Thm.rhs_of eqn;
  1171               val tprems = map term_of prems;
  1172               val i = 1 + Library.foldl Int.max (~1, map (fn p =>
  1173                 find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
  1174               val (rrs', asm') = rules_of_prem ss prem'
  1175             in mut_impc prems concl rrss asms (prem' :: prems')
  1176               (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
  1177                 (Library.take (i, prems))
  1178                 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
  1179                   (Library.drop (i, prems), concl))))) :: eqns)
  1180                   ss (length prems') ~1
  1181             end
  1182 
  1183      (*legacy code - only for backwards compatibility*)
  1184      and nonmut_impc ct ss =
  1185        let val (prem, conc) = Thm.dest_implies ct;
  1186            val thm1 = if simprem then botc skel0 ss prem else NONE;
  1187            val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
  1188            val ss1 = if not useprem then ss else add_rrules
  1189              (apsnd single (apfst single (rules_of_prem ss prem1))) ss
  1190        in (case botc skel0 ss1 conc of
  1191            NONE => (case thm1 of
  1192                NONE => NONE
  1193              | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
  1194          | SOME thm2 =>
  1195            let val thm2' = disch false prem1 thm2
  1196            in (case thm1 of
  1197                NONE => SOME thm2'
  1198              | SOME thm1' =>
  1199                  SOME (transitive (Drule.imp_cong_rule thm1' (reflexive conc)) thm2'))
  1200            end)
  1201        end
  1202 
  1203  in try_botc end;
  1204 
  1205 
  1206 (* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
  1207 
  1208 (*
  1209   Parameters:
  1210     mode = (simplify A,
  1211             use A in simplifying B,
  1212             use prems of B (if B is again a meta-impl.) to simplify A)
  1213            when simplifying A ==> B
  1214     prover: how to solve premises in conditional rewrites and congruences
  1215 *)
  1216 
  1217 val debug_bounds = ref false;
  1218 
  1219 fun check_bounds ss ct =
  1220   if ! debug_bounds then
  1221     let
  1222       val Simpset ({bounds = (_, bounds), ...}, _) = ss;
  1223       val bs = fold_aterms (fn Free (x, _) =>
  1224           if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
  1225           then insert (op =) x else I
  1226         | _ => I) (term_of ct) [];
  1227     in
  1228       if null bs then ()
  1229       else print_term ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
  1230         (Thm.theory_of_cterm ct) (Thm.term_of ct)
  1231     end
  1232   else ();
  1233 
  1234 fun rewrite_cterm mode prover raw_ss raw_ct =
  1235   let
  1236     val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
  1237     val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
  1238     val ss = inc_simp_depth (activate_context thy raw_ss);
  1239     val depth = simp_depth ss;
  1240     val _ =
  1241       if depth mod 20 = 0 then
  1242         warning ("Simplification depth " ^ string_of_int depth)
  1243       else ();
  1244     val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
  1245     val _ = check_bounds ss ct;
  1246   in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
  1247 
  1248 val simple_prover =
  1249   SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
  1250 
  1251 (*Rewrite a cterm*)
  1252 fun rewrite _ [] ct = Thm.reflexive ct
  1253   | rewrite full thms ct =
  1254       rewrite_cterm (full, false, false) simple_prover
  1255         (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
  1256 
  1257 (*Rewrite a theorem*)
  1258 fun simplify full thms = Conv.fconv_rule (rewrite full thms);
  1259 val rewrite_rule = simplify true;
  1260 
  1261 (*simple term rewriting -- no proof*)
  1262 fun rewrite_term thy rules procs =
  1263   Pattern.rewrite_term thy (map decomp_simp' rules) procs;
  1264 
  1265 fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
  1266 
  1267 (*Rewrite the subgoals of a proof state (represented by a theorem)*)
  1268 fun rewrite_goals_rule thms th =
  1269   Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
  1270     (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
  1271 
  1272 (*Rewrite the subgoal of a proof state (represented by a theorem)*)
  1273 fun rewrite_goal_rule mode prover ss i thm =
  1274   if 0 < i andalso i <= Thm.nprems_of thm
  1275   then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
  1276   else raise THM ("rewrite_goal_rule", i, [thm]);
  1277 
  1278 
  1279 (** meta-rewriting tactics **)
  1280 
  1281 (*Rewrite throughout proof state. *)
  1282 fun rewrite_tac defs = PRIMITIVE (rewrite_rule defs);
  1283 
  1284 (*Rewrite subgoals only, not main goal. *)
  1285 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
  1286 fun rewtac def = rewrite_goals_tac [def];
  1287 
  1288 (*Rewrite subgoal i only.*)
  1289 fun asm_rewrite_goal_tac mode prover_tac ss i thm =
  1290   if 0 < i andalso i <= Thm.nprems_of thm then
  1291     Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
  1292   else Seq.empty;
  1293 
  1294 fun rewrite_goal_tac rews =
  1295   let val ss = empty_ss addsimps rews in
  1296     fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
  1297       (theory_context (Thm.theory_of_thm st) ss) i st
  1298   end;
  1299 
  1300 (*Prunes all redundant parameters from the proof state by rewriting.
  1301   DOES NOT rewrite main goal, where quantification over an unused bound
  1302     variable is sometimes done to avoid the need for cut_facts_tac.*)
  1303 val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
  1304 
  1305 
  1306 (* for folding definitions, handling critical pairs *)
  1307 
  1308 (*The depth of nesting in a term*)
  1309 fun term_depth (Abs(a,T,t)) = 1 + term_depth t
  1310   | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
  1311   | term_depth _ = 0;
  1312 
  1313 val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
  1314 
  1315 (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
  1316   Returns longest lhs first to avoid folding its subexpressions.*)
  1317 fun sort_lhs_depths defs =
  1318   let val keylist = AList.make (term_depth o lhs_of_thm) defs
  1319       val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
  1320   in map (AList.find (op =) keylist) keys end;
  1321 
  1322 val rev_defs = sort_lhs_depths o map symmetric;
  1323 
  1324 fun fold_rule defs = fold rewrite_rule (rev_defs defs);
  1325 fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
  1326 fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
  1327 
  1328 
  1329 (* HHF normal form: !! before ==>, outermost !! generalized *)
  1330 
  1331 local
  1332 
  1333 fun gen_norm_hhf ss th =
  1334   (if Drule.is_norm_hhf (Thm.prop_of th) then th
  1335    else Conv.fconv_rule
  1336     (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
  1337   |> Thm.adjust_maxidx_thm ~1
  1338   |> Drule.gen_all;
  1339 
  1340 val hhf_ss = empty_ss addsimps [Drule.norm_hhf_eq];
  1341 
  1342 in
  1343 
  1344 val norm_hhf = gen_norm_hhf hhf_ss;
  1345 val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
  1346 
  1347 end;
  1348 
  1349 end;
  1350 
  1351 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
  1352 open BasicMetaSimplifier;