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