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