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