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