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