src/Provers/simplifier.ML
author wenzelm
Tue Sep 21 23:06:50 1999 +0200 (1999-09-21 ago)
changeset 7571 44e9db3150f6
parent 7568 436c87ac2fac
child 7646 1ad3866b86cc
permissions -rw-r--r--
merged in lost update;
     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               simp_tac: simpset -> int -> tactic
    64   val           asm_simp_tac: simpset -> int -> tactic
    65   val          full_simp_tac: simpset -> int -> tactic
    66   val        asm_lr_simp_tac: simpset -> int -> tactic
    67   val      asm_full_simp_tac: simpset -> int -> tactic
    68   val safe_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 simp_add_global: theory attribute
    91   val simp_del_global: theory attribute
    92   val simp_add_local: Proof.context attribute
    93   val simp_del_local: Proof.context attribute
    94   val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
    95   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    96   val setup: (theory -> theory) list
    97 end;
    98 
    99 structure Simplifier: SIMPLIFIER =
   100 struct
   101 
   102 
   103 (** simplification procedures **)
   104 
   105 (* datatype simproc *)
   106 
   107 datatype simproc =
   108   Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   109 
   110 fun mk_simproc name lhss proc =
   111   Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   112 
   113 fun rep_simproc (Simproc args) = args;
   114 
   115 (** solvers **)
   116 
   117 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   118 
   119 fun mk_solver name solver = Solver(name, solver, stamp());
   120 
   121 fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
   122 
   123 val merge_solvers = generic_merge eq_solver I I;
   124 
   125 fun app_sols [] _ _ = no_tac
   126   | app_sols (Solver(_,solver,_)::sols) thms i =
   127        solver thms i ORELSE app_sols sols thms i;
   128 
   129 (** simplification sets **)
   130 
   131 (* type simpset *)
   132 
   133 datatype simpset =
   134   Simpset of {
   135     mss: meta_simpset,
   136     subgoal_tac:        simpset -> int -> tactic,
   137     loop_tacs:          (string * (int -> tactic))list,
   138     unsafe_solvers: solver list,
   139            solvers: solver list};
   140 
   141 fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
   142   Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
   143     unsafe_solvers = unsafe_solvers, solvers = solvers};
   144 
   145 val empty_ss =
   146   let val mss = Thm.set_mk_sym (Thm.empty_mss, Some o symmetric_fun)
   147   in make_ss (mss, K (K no_tac), [], [], []) end;
   148 
   149 fun rep_ss (Simpset args) = args;
   150 fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
   151 
   152 
   153 (* print simpsets *)
   154 
   155 fun print_ss ss =
   156   let
   157     val Simpset {mss, ...} = ss;
   158     val {simps, procs, congs} = Thm.dest_mss mss;
   159 
   160     val pretty_thms = map Display.pretty_thm;
   161     fun pretty_proc (name, lhss) =
   162       Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   163   in
   164     Pretty.writeln (Pretty.big_list "simplification rules:" (pretty_thms simps));
   165     Pretty.writeln (Pretty.big_list "simplification procedures:" (map pretty_proc procs));
   166     Pretty.writeln (Pretty.big_list "congruences:" (pretty_thms congs))
   167   end;
   168 
   169 
   170 (* extend simpsets *)
   171 
   172 fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
   173     setsubgoaler subgoal_tac =
   174   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   175 
   176 fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
   177     setloop tac =
   178   make_ss (mss, subgoal_tac, [("",tac)], unsafe_solvers, solvers);
   179 
   180 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   181     addloop tac = make_ss (mss, subgoal_tac, 
   182         (case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
   183          warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
   184            unsafe_solvers, solvers);
   185 
   186 fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   187  delloop name =
   188   let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   189     if null del then (warning ("No such looper in simpset: " ^ name); ss)
   190     else make_ss (mss, subgoal_tac, rest, unsafe_solvers, solvers)
   191   end;
   192 
   193 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   194     setSSolver solver =
   195   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, [solver]);
   196 
   197 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   198     addSSolver sol =
   199   make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers,
   200            merge_solvers solvers [sol]);
   201 
   202 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   203     setSolver unsafe_solver =
   204   make_ss (mss, subgoal_tac, loop_tacs, [unsafe_solver], solvers);
   205 
   206 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   207     addSolver sol =
   208   make_ss (mss, subgoal_tac, loop_tacs, 
   209     merge_solvers unsafe_solvers [sol], solvers);
   210 
   211 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   212     setmksimps mk_simps =
   213   make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
   214     subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   215 
   216 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   217     setmkeqTrue mk_eq_True =
   218   make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
   219     subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   220 
   221 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   222     setmksym mksym =
   223   make_ss (Thm.set_mk_sym (mss, mksym),
   224     subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   225 
   226 fun (Simpset {mss, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   227     settermless termless =
   228   make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
   229     unsafe_solvers, solvers);
   230 
   231 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   232     addsimps rews =
   233   make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs, 
   234 	   unsafe_solvers, solvers);
   235 
   236 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   237     delsimps rews =
   238   make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs, 
   239 	   unsafe_solvers, solvers);
   240 
   241 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   242     addeqcongs newcongs =
   243   make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs, 
   244 	   unsafe_solvers, solvers);
   245 
   246 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   247     deleqcongs oldcongs =
   248   make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs, 
   249 	   unsafe_solvers, solvers);
   250 
   251 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   252     addsimprocs simprocs =
   253   make_ss
   254     (Thm.add_simprocs (mss, map rep_simproc simprocs),
   255       subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   256 
   257 fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   258     delsimprocs simprocs =
   259   make_ss
   260     (Thm.del_simprocs (mss, map rep_simproc simprocs),
   261       subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   262 
   263 fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers}) =
   264   make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   265 
   266 
   267 (* merge simpsets *)
   268 (*NOTE: ignores subgoal_tac of 2nd simpset *)
   269 
   270 fun merge_ss
   271    (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac,
   272              unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   273     Simpset {mss = mss2, loop_tacs = loop_tacs2,
   274              unsafe_solvers = unsafe_solvers2, solvers = solvers2, ...}) =
   275   make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
   276     merge_alists loop_tacs1 loop_tacs2,
   277     merge_solvers unsafe_solvers1 unsafe_solvers2,
   278     merge_solvers solvers1 solvers2);
   279 
   280 
   281 (** global and local simpset data **)
   282 
   283 (* theory data kind 'Provers/simpset' *)
   284 
   285 structure GlobalSimpsetArgs =
   286 struct
   287   val name = "Provers/simpset";
   288   type T = simpset ref;
   289 
   290   val empty = ref empty_ss;
   291   fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
   292   val prep_ext = copy;
   293   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   294   fun print _ (ref ss) = print_ss ss;
   295 end;
   296 
   297 structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   298 val print_simpset = GlobalSimpset.print;
   299 val simpset_ref_of_sg = GlobalSimpset.get_sg;
   300 val simpset_ref_of = GlobalSimpset.get;
   301 
   302 
   303 (* access global simpset *)
   304 
   305 val simpset_of_sg = ! o simpset_ref_of_sg;
   306 val simpset_of = simpset_of_sg o Theory.sign_of;
   307 
   308 fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
   309 fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
   310 
   311 val simpset = simpset_of o Context.the_context;
   312 val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
   313 
   314 
   315 (* change global simpset *)
   316 
   317 fun change_simpset_of f x thy =
   318   let val r = simpset_ref_of thy
   319   in r := f (! r, x); thy end;
   320 
   321 fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());
   322 
   323 val Addsimps = change_simpset (op addsimps);
   324 val Delsimps = change_simpset (op delsimps);
   325 val Addsimprocs = change_simpset (op addsimprocs);
   326 val Delsimprocs = change_simpset (op delsimprocs);
   327 
   328 
   329 (* proof data kind 'Provers/simpset' *)
   330 
   331 structure LocalSimpsetArgs =
   332 struct
   333   val name = "Provers/simpset";
   334   type T = simpset;
   335   val init = simpset_of;
   336   fun print _ ss = print_ss ss;
   337 end;
   338 
   339 structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
   340 val print_local_simpset = LocalSimpset.print;
   341 val get_local_simpset = LocalSimpset.get;
   342 val put_local_simpset = LocalSimpset.put;
   343 fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;
   344 
   345 
   346 (* attributes *)
   347 
   348 fun change_global_ss f (thy, th) =
   349   let val r = simpset_ref_of thy
   350   in r := f (! r, [th]); (thy, th) end;
   351 
   352 fun change_local_ss f (ctxt, th) =
   353   let val ss = f (get_local_simpset ctxt, [th])
   354   in (put_local_simpset ss ctxt, th) end;
   355 
   356 val simp_add_global = change_global_ss (op addsimps);
   357 val simp_del_global = change_global_ss (op delsimps);
   358 val simp_add_local = change_local_ss (op addsimps);
   359 val simp_del_local = change_local_ss (op delsimps);
   360 
   361 
   362 
   363 (** simplification tactics **)
   364 
   365 fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers) mss =
   366   let
   367     val ss =
   368       make_ss (mss, subgoal_tac, loop_tacs,unsafe_solvers,unsafe_solvers);
   369     val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   370   in DEPTH_SOLVE solve1_tac end;
   371 
   372 fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   373 
   374 (*unsafe: may instantiate unknowns that appear also in other subgoals*)
   375 fun basic_gen_simp_tac mode solvers =
   376   fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =>
   377     let
   378       fun simp_loop_tac i =
   379         asm_rewrite_goal_tac mode
   380           (solve_all_tac (subgoal_tac,loop_tacs,unsafe_solvers))
   381           mss i
   382         THEN (solvers (prems_of_mss mss) i ORELSE
   383               TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   384     in simp_loop_tac end;
   385 
   386 fun gen_simp_tac mode 
   387       (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =
   388   basic_gen_simp_tac mode (app_sols unsafe_solvers) ss;
   389 
   390 val          simp_tac = gen_simp_tac (false, false, false);
   391 val      asm_simp_tac = gen_simp_tac (false, true, false);
   392 val     full_simp_tac = gen_simp_tac (true,  false, false);
   393 val   asm_lr_simp_tac = gen_simp_tac (true,  true, false);
   394 val asm_full_simp_tac = gen_simp_tac (true,  true, true);
   395 
   396 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   397 fun safe_asm_full_simp_tac (ss as Simpset {mss, subgoal_tac, loop_tacs, 
   398 	unsafe_solvers, solvers}) = 
   399   basic_gen_simp_tac (true, true, true) (app_sols solvers) ss;
   400 
   401 (*the abstraction over the proof state delays the dereferencing*)
   402 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   403 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   404 fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   405 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   406 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   407 
   408 
   409 
   410 (** simplification rules and conversions **)
   411 
   412 fun simp rew mode 
   413      (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   414   let
   415     val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers);
   416     fun prover m th = apsome fst (Seq.pull (tacf m th));
   417   in rew mode prover mss thm end;
   418 
   419 val simp_thm = simp Drule.rewrite_thm;
   420 val simp_cterm = simp Drule.rewrite_cterm;
   421 
   422 val          simplify = simp_thm (false, false, false);
   423 val      asm_simplify = simp_thm (false, true, false);
   424 val     full_simplify = simp_thm (true, false, false);
   425 val asm_full_simplify = simp_thm (true, true, false);
   426 
   427 val          rewrite = simp_cterm (false, false, false);
   428 val      asm_rewrite = simp_cterm (false, true, false);
   429 val     full_rewrite = simp_cterm (true, false, false);
   430 val asm_full_rewrite = simp_cterm (true, true, false);
   431 
   432 
   433 
   434 (** concrete syntax of attributes **)
   435 
   436 (* add / del *)
   437 
   438 val simpN = "simp";
   439 val addN = "add";
   440 val delN = "del";
   441 val onlyN = "only";
   442 val otherN = "other";
   443 
   444 fun simp_att change =
   445   (Args.$$$ addN >> K (op addsimps) ||
   446     Args.$$$ delN >> K (op delsimps) ||
   447     Scan.succeed (op addsimps))
   448   >> change
   449   |> Scan.lift
   450   |> Attrib.syntax;
   451 
   452 val simp_attr = (simp_att change_global_ss, simp_att change_local_ss);
   453 
   454 
   455 (* conversions *)
   456 
   457 fun conv_attr f =
   458   (Attrib.no_args (Drule.rule_attribute (f o simpset_of)),
   459     Attrib.no_args (Drule.rule_attribute (f o get_local_simpset)));
   460 
   461 
   462 (* setup_attrs *)
   463 
   464 val setup_attrs = Attrib.add_attributes
   465  [(simpN,               simp_attr, "simplification rule"),
   466   ("simplify",          conv_attr simplify, "simplify rule"),
   467   ("asm_simplify",      conv_attr asm_simplify, "simplify rule, using assumptions"),
   468   ("full_simplify",     conv_attr full_simplify, "fully simplify rule"),
   469   ("asm_full_simplify", conv_attr asm_full_simplify, "fully simplify rule, using assumptions")];
   470 
   471 
   472 
   473 (** proof methods **)
   474 
   475 (* simplification *)
   476 
   477 val simp_modifiers =
   478  [Args.$$$ simpN -- Args.$$$ addN >> K (I, simp_add_local),
   479   Args.$$$ simpN -- Args.$$$ delN >> K (I, simp_del_local),
   480   Args.$$$ simpN -- Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
   481   Args.$$$ otherN >> K (I, I)];
   482 
   483 val simp_modifiers' =
   484  [Args.$$$ addN >> K (I, simp_add_local),
   485   Args.$$$ delN >> K (I, simp_del_local),
   486   Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
   487   Args.$$$ otherN >> K (I, I)];
   488 
   489 fun simp_method tac =
   490   (fn prems => fn ctxt => Method.METHOD (fn facts =>
   491     FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   492   |> Method.bang_sectioned_args simp_modifiers';
   493   
   494 
   495 (* setup_methods *)
   496 
   497 val setup_methods = Method.add_methods
   498  [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
   499   ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
   500   ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
   501   ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
   502   ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
   503   ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
   504 
   505 
   506 
   507 (** theory setup **)
   508 
   509 val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs, setup_methods];
   510 
   511 
   512 end;
   513 
   514 
   515 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   516 open BasicSimplifier;