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