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