src/Provers/simplifier.ML
author wenzelm
Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago)
changeset 9449 2f814053a6cc
parent 9446 7bc054e9fb1c
child 9513 8531c18d9181
permissions -rw-r--r--
intro_elim_tac: bimatch_from;
     1 (*  Title:      Provers/simplifier.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Generic simplifier, suitable for most logics.  See Pure/thm.ML for the
     6 actual meta-level rewriting engine.
     7 *)
     8 
     9 infix 4
    10   setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
    11   addSolver addsimps delsimps addeqcongs deleqcongs
    12   setmksimps setmkeqTrue setmksym settermless addsimprocs delsimprocs;
    13 
    14 signature BASIC_SIMPLIFIER =
    15 sig
    16   type simproc
    17   val mk_simproc: string -> cterm list
    18     -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    19   type solver
    20   val mk_solver: string -> (thm list -> int -> tactic) -> solver
    21   type simpset
    22   val empty_ss: simpset
    23   val rep_ss: simpset ->
    24    {mss: meta_simpset,
    25     subgoal_tac:        simpset -> int -> tactic,
    26     loop_tacs:          (string * (int -> tactic))list,
    27     unsafe_solvers: solver list,
    28            solvers: solver list};
    29   val print_ss: simpset -> unit
    30   val print_simpset: theory -> unit
    31   val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    32   val setloop:      simpset *             (int -> tactic) -> simpset
    33   val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    34   val delloop:      simpset *   string                    -> simpset
    35   val setSSolver:   simpset * solver -> simpset
    36   val addSSolver:   simpset * solver -> simpset
    37   val setSolver:    simpset * solver -> simpset
    38   val addSolver:    simpset * solver -> simpset
    39   val setmksimps:   simpset * (thm -> thm list) -> simpset
    40   val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    41   val setmksym:     simpset * (thm -> thm option) -> simpset
    42   val settermless:  simpset * (term * term -> bool) -> simpset
    43   val addsimps:     simpset * thm list -> simpset
    44   val delsimps:     simpset * thm list -> simpset
    45   val addeqcongs:   simpset * thm list -> simpset
    46   val deleqcongs:   simpset * thm list -> simpset
    47   val addsimprocs:  simpset * simproc list -> simpset
    48   val delsimprocs:  simpset * simproc list -> simpset
    49   val merge_ss:     simpset * simpset -> simpset
    50   val prems_of_ss:  simpset -> thm list
    51   val simpset_ref_of_sg: Sign.sg -> simpset ref
    52   val simpset_ref_of: theory -> simpset ref
    53   val simpset_of_sg: Sign.sg -> simpset
    54   val simpset_of: theory -> simpset
    55   val SIMPSET: (simpset -> tactic) -> tactic
    56   val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
    57   val simpset: unit -> simpset
    58   val simpset_ref: unit -> simpset ref
    59   val Addsimps: thm list -> unit
    60   val Delsimps: thm list -> unit
    61   val Addsimprocs: simproc list -> unit
    62   val Delsimprocs: simproc list -> unit
    63   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    64   val               simp_tac: simpset -> int -> tactic
    65   val           asm_simp_tac: simpset -> int -> tactic
    66   val          full_simp_tac: simpset -> int -> tactic
    67   val        asm_lr_simp_tac: simpset -> int -> tactic
    68   val      asm_full_simp_tac: simpset -> int -> tactic
    69   val               Simp_tac:            int -> tactic
    70   val           Asm_simp_tac:            int -> tactic
    71   val          Full_simp_tac:            int -> tactic
    72   val        Asm_lr_simp_tac:            int -> tactic
    73   val      Asm_full_simp_tac:            int -> tactic
    74   val          simplify: simpset -> thm -> thm
    75   val      asm_simplify: simpset -> thm -> thm
    76   val     full_simplify: simpset -> thm -> thm
    77   val asm_full_simplify: simpset -> thm -> thm
    78 end;
    79 
    80 signature SIMPLIFIER =
    81 sig
    82   include BASIC_SIMPLIFIER
    83   val          rewrite: simpset -> cterm -> thm
    84   val      asm_rewrite: simpset -> cterm -> thm
    85   val     full_rewrite: simpset -> cterm -> thm
    86   val asm_full_rewrite: simpset -> cterm -> thm
    87   val print_local_simpset: Proof.context -> unit
    88   val get_local_simpset: Proof.context -> simpset
    89   val put_local_simpset: simpset -> Proof.context -> Proof.context
    90   val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
    91   val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
    92   val simp_add_global: theory attribute
    93   val simp_del_global: theory attribute
    94   val simp_add_local: Proof.context attribute
    95   val simp_del_local: Proof.context attribute
    96   val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
    97   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    98   val setup: (theory -> theory) list
    99   val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
   100     -> (theory -> theory) list
   101   val easy_setup: thm -> thm list -> (theory -> theory) list
   102 end;
   103 
   104 structure Simplifier: SIMPLIFIER =
   105 struct
   106 
   107 
   108 (** simplification procedures **)
   109 
   110 (* datatype simproc *)
   111 
   112 datatype simproc =
   113   Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   114 
   115 fun mk_simproc name lhss proc =
   116   Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   117 
   118 fun rep_simproc (Simproc args) = args;
   119 
   120 
   121 
   122 (** solvers **)
   123 
   124 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   125 
   126 fun mk_solver name solver = Solver(name, solver, stamp());
   127 
   128 fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
   129 
   130 val merge_solvers = generic_merge eq_solver I I;
   131 
   132 fun app_sols [] _ _ = no_tac
   133   | app_sols (Solver(_,solver,_)::sols) thms i =
   134        solver thms i ORELSE app_sols sols thms i;
   135 
   136 
   137 
   138 (** simplification sets **)
   139 
   140 (* type simpset *)
   141 
   142 datatype simpset =
   143   Simpset of {
   144     mss: meta_simpset,
   145     subgoal_tac:        simpset -> int -> tactic,
   146     loop_tacs:          (string * (int -> tactic))list,
   147     unsafe_solvers: solver list,
   148            solvers: solver list};
   149 
   150 fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
   151   Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
   152     unsafe_solvers = unsafe_solvers, solvers = solvers};
   153 
   154 val empty_ss =
   155   let val mss = Thm.set_mk_sym (Thm.empty_mss, Some o symmetric_fun)
   156   in make_ss (mss, K (K no_tac), [], [], []) end;
   157 
   158 fun rep_ss (Simpset args) = args;
   159 fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
   160 
   161 
   162 (* print simpsets *)
   163 
   164 fun print_ss ss =
   165   let
   166     val Simpset {mss, ...} = ss;
   167     val {simps, procs, congs} = Thm.dest_mss mss;
   168 
   169     val pretty_thms = map Display.pretty_thm;
   170     fun pretty_proc (name, lhss) =
   171       Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   172   in
   173     [Pretty.big_list "simplification rules:" (pretty_thms simps),
   174       Pretty.big_list "simplification procedures:" (map pretty_proc procs),
   175       Pretty.big_list "congruences:" (pretty_thms congs)]
   176     |> Pretty.chunks |> Pretty.writeln
   177   end;
   178 
   179 
   180 (* extend simpsets *)
   181 
   182 fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
   183     setsubgoaler subgoal_tac =
   184   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   185 
   186 fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
   187     setloop tac =
   188   make_ss (mss, subgoal_tac, [("", tac)], unsafe_solvers, solvers);
   189 
   190 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   191     addloop tac = make_ss (mss, subgoal_tac, 
   192         (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x => 
   193          warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac)),
   194            unsafe_solvers, solvers);
   195 
   196 fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   197  delloop name =
   198   let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   199     if null del then (warning ("No such looper in simpset: " ^ name); ss)
   200     else make_ss (mss, subgoal_tac, rest, unsafe_solvers, solvers)
   201   end;
   202 
   203 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   204     setSSolver solver =
   205   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, [solver]);
   206 
   207 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   208     addSSolver sol =
   209   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers,
   210            merge_solvers solvers [sol]);
   211 
   212 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   213     setSolver unsafe_solver =
   214   make_ss (mss, subgoal_tac, loop_tacs, [unsafe_solver], solvers);
   215 
   216 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   217     addSolver sol =
   218   make_ss (mss, subgoal_tac, loop_tacs, 
   219     merge_solvers unsafe_solvers [sol], solvers);
   220 
   221 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   222     setmksimps mk_simps =
   223   make_ss (Thm.set_mk_rews (mss, mk_simps), subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   224 
   225 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   226     setmkeqTrue mk_eq_True =
   227   make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
   228     subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   229 
   230 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   231     setmksym mksym =
   232   make_ss (Thm.set_mk_sym (mss, mksym),
   233     subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   234 
   235 fun (Simpset {mss, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   236     settermless termless =
   237   make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
   238     unsafe_solvers, solvers);
   239 
   240 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   241     addsimps rews =
   242   make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs, 
   243 	   unsafe_solvers, solvers);
   244 
   245 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   246     delsimps rews =
   247   make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs, 
   248 	   unsafe_solvers, solvers);
   249 
   250 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   251     addeqcongs newcongs =
   252   make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs, 
   253 	   unsafe_solvers, solvers);
   254 
   255 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   256     deleqcongs oldcongs =
   257   make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs, 
   258 	   unsafe_solvers, solvers);
   259 
   260 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   261     addsimprocs simprocs =
   262   make_ss
   263     (Thm.add_simprocs (mss, map rep_simproc simprocs),
   264       subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   265 
   266 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   267     delsimprocs simprocs =
   268   make_ss
   269     (Thm.del_simprocs (mss, map rep_simproc simprocs),
   270       subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   271 
   272 fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
   273   make_ss (Thm.clear_mss mss, subgoal_tac, [], unsafe_solvers, solvers);
   274 
   275 
   276 (* merge simpsets *)
   277 
   278 (*ignores subgoal_tac of 2nd simpset!*)
   279 
   280 fun merge_ss
   281    (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac,
   282              unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   283     Simpset {mss = mss2, loop_tacs = loop_tacs2,
   284              unsafe_solvers = unsafe_solvers2, solvers = solvers2, ...}) =
   285   make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
   286     merge_alists loop_tacs1 loop_tacs2,
   287     merge_solvers unsafe_solvers1 unsafe_solvers2,
   288     merge_solvers solvers1 solvers2);
   289 
   290 
   291 
   292 (** global and local simpset data **)
   293 
   294 (* theory data kind 'Provers/simpset' *)
   295 
   296 structure GlobalSimpsetArgs =
   297 struct
   298   val name = "Provers/simpset";
   299   type T = simpset ref;
   300 
   301   val empty = ref empty_ss;
   302   fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
   303   val prep_ext = copy;
   304   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   305   fun print _ (ref ss) = print_ss ss;
   306 end;
   307 
   308 structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   309 val print_simpset = GlobalSimpset.print;
   310 val simpset_ref_of_sg = GlobalSimpset.get_sg;
   311 val simpset_ref_of = GlobalSimpset.get;
   312 
   313 
   314 (* access global simpset *)
   315 
   316 val simpset_of_sg = ! o simpset_ref_of_sg;
   317 val simpset_of = simpset_of_sg o Theory.sign_of;
   318 
   319 fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
   320 fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
   321 
   322 val simpset = simpset_of o Context.the_context;
   323 val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
   324 
   325 
   326 (* change global simpset *)
   327 
   328 fun change_simpset_of f x thy =
   329   let val r = simpset_ref_of thy
   330   in r := f (! r, x); thy end;
   331 
   332 fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());
   333 
   334 val Addsimps = change_simpset (op addsimps);
   335 val Delsimps = change_simpset (op delsimps);
   336 val Addsimprocs = change_simpset (op addsimprocs);
   337 val Delsimprocs = change_simpset (op delsimprocs);
   338 
   339 
   340 (* proof data kind 'Provers/simpset' *)
   341 
   342 structure LocalSimpsetArgs =
   343 struct
   344   val name = "Provers/simpset";
   345   type T = simpset;
   346   val init = simpset_of;
   347   fun print _ ss = print_ss ss;
   348 end;
   349 
   350 structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
   351 val print_local_simpset = LocalSimpset.print;
   352 val get_local_simpset = LocalSimpset.get;
   353 val put_local_simpset = LocalSimpset.put;
   354 fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;
   355 
   356 
   357 (* attributes *)
   358 
   359 fun change_global_ss f (thy, th) =
   360   let val r = simpset_ref_of thy
   361   in r := f (! r, [th]); (thy, th) end;
   362 
   363 fun change_local_ss f (ctxt, th) =
   364   let val ss = f (get_local_simpset ctxt, [th])
   365   in (put_local_simpset ss ctxt, th) end;
   366 
   367 val simp_add_global = change_global_ss (op addsimps);
   368 val simp_del_global = change_global_ss (op delsimps);
   369 val simp_add_local = change_local_ss (op addsimps);
   370 val simp_del_local = change_local_ss (op delsimps);
   371 
   372 
   373 
   374 (** simplification tactics **)
   375 
   376 fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers) mss =
   377   let
   378     val ss =
   379       make_ss (mss, subgoal_tac, loop_tacs,unsafe_solvers,unsafe_solvers);
   380     val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   381   in DEPTH_SOLVE solve1_tac end;
   382 
   383 fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   384 
   385 (*note: may instantiate unknowns that appear also in other subgoals*)
   386 fun generic_simp_tac safe mode =
   387   fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   388     let
   389       val solvs = app_sols (if safe then solvers else unsafe_solvers);
   390       fun simp_loop_tac i =
   391         asm_rewrite_goal_tac mode
   392           (solve_all_tac (subgoal_tac,loop_tacs,unsafe_solvers))
   393           mss i
   394         THEN (solvs (prems_of_mss mss) i ORELSE
   395               TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   396     in simp_loop_tac end;
   397 
   398 val          simp_tac = generic_simp_tac false (false, false, false);
   399 val      asm_simp_tac = generic_simp_tac false (false, true, false);
   400 val     full_simp_tac = generic_simp_tac false (true,  false, false);
   401 val   asm_lr_simp_tac = generic_simp_tac false (true,  true, false);
   402 val asm_full_simp_tac = generic_simp_tac false (true,  true, true);
   403 
   404 
   405 (*the abstraction over the proof state delays the dereferencing*)
   406 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   407 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   408 fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   409 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   410 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   411 
   412 
   413 
   414 (** simplification rules and conversions **)
   415 
   416 fun simp rew mode 
   417      (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   418   let
   419     val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers);
   420     fun prover m th = apsome fst (Seq.pull (tacf m th));
   421   in rew mode prover mss thm end;
   422 
   423 val simp_thm = simp Drule.rewrite_thm;
   424 val simp_cterm = simp Drule.rewrite_cterm;
   425 
   426 val          simplify = simp_thm (false, false, false);
   427 val      asm_simplify = simp_thm (false, true, false);
   428 val     full_simplify = simp_thm (true, false, false);
   429 val asm_full_simplify = simp_thm (true, true, false);
   430 
   431 val          rewrite = simp_cterm (false, false, false);
   432 val      asm_rewrite = simp_cterm (false, true, false);
   433 val     full_rewrite = simp_cterm (true, false, false);
   434 val asm_full_rewrite = simp_cterm (true, true, false);
   435 
   436 
   437 
   438 (** concrete syntax of attributes **)
   439 
   440 (* add / del *)
   441 
   442 val simpN = "simp";
   443 val addN = "add";
   444 val delN = "del";
   445 val onlyN = "only";
   446 val otherN = "other";
   447 
   448 val simp_attr =
   449  (Attrib.add_del_args simp_add_global simp_del_global,
   450   Attrib.add_del_args simp_add_local simp_del_local);
   451 
   452 
   453 (* conversions *)
   454 
   455 fun conv_attr f =
   456   (Attrib.no_args (Drule.rule_attribute (f o simpset_of)),
   457     Attrib.no_args (Drule.rule_attribute (f o get_local_simpset)));
   458 
   459 
   460 (* setup_attrs *)
   461 
   462 val setup_attrs = Attrib.add_attributes
   463  [(simpN,               simp_attr, "declare simplification rule"),
   464   ("simplify",          conv_attr simplify, "simplify rule"),
   465   ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
   466   ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
   467   ("asm_full_simplify", conv_attr asm_full_simplify, "fully simplify rule, using assumptions")];
   468 
   469 
   470 
   471 (** proof methods **)
   472 
   473 (* simplification *)
   474 
   475 val simp_options =
   476  (Args.parens (Args.$$$ "no_asm") >> K simp_tac ||
   477   Args.parens (Args.$$$ "no_asm_simp") >> K asm_simp_tac ||
   478   Args.parens (Args.$$$ "no_asm_use") >> K full_simp_tac ||
   479   Scan.succeed asm_full_simp_tac);
   480 
   481 val simp_modifiers =
   482  [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
   483   Args.$$$ simpN -- Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
   484   Args.$$$ simpN -- Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
   485   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
   486   Args.$$$ otherN -- Args.colon >> K (I, I)];
   487 
   488 val simp_modifiers' =
   489  [Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
   490   Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
   491   Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
   492   Args.$$$ otherN -- Args.colon >> K (I, I)];
   493 
   494 fun simp_args more_mods =
   495   Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
   496 
   497 
   498 fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   499   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   500     (CHANGED o ALLGOALS o tac) (get_local_simpset ctxt));
   501 
   502 fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   503   HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt)));
   504   
   505 
   506 (* setup_methods *)
   507 
   508 fun setup_methods more_mods = Method.add_methods
   509  [(simpN, simp_args more_mods simp_method', "simplification"),
   510   ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   511 
   512 
   513 
   514 (** theory setup **)
   515 
   516 val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs];
   517 fun method_setup mods = [setup_methods mods];
   518 
   519 fun easy_setup reflect trivs =
   520   let
   521     val trivialities = Drule.reflexive_thm :: trivs;
   522 
   523     fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
   524     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   525 
   526     (*no premature instantiation of variables during simplification*)
   527     fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   528     val safe_solver = mk_solver "easy safe" safe_solver_tac;
   529 
   530     fun mk_eq thm =
   531       if Logic.is_equals (Thm.concl_of thm) then [thm]
   532       else [thm RS reflect] handle THM _ => [];
   533 
   534     fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   535 
   536     fun init_ss thy =
   537       (simpset_ref_of thy :=
   538         empty_ss setsubgoaler asm_simp_tac
   539         setSSolver safe_solver
   540         setSolver unsafe_solver
   541         setmksimps mksimps; thy);
   542   in setup @ method_setup [] @ [init_ss] end;
   543 
   544 
   545 
   546 (** outer syntax **)
   547 
   548 val print_simpsetP =
   549   OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
   550     OuterSyntax.Keyword.diag
   551     (Scan.succeed (Toplevel.no_timing o (Toplevel.keep
   552       (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
   553 
   554 val _ = OuterSyntax.add_parsers [print_simpsetP];
   555 
   556 end;
   557 
   558 
   559 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   560 open BasicSimplifier;