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