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