src/Pure/simplifier.ML
author haftmann
Fri Dec 05 08:04:53 2008 +0100 (2008-12-05)
changeset 28991 694227dd3e8c
parent 28965 1de908189869
child 29606 fedb8be05f24
permissions -rw-r--r--
dropped NameSpace.declare_base
     1 (*  Title:      Pure/simplifier.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Generic simplifier, suitable for most logics (see also
     6 meta_simplifier.ML for the actual meta-level rewriting engine).
     7 *)
     8 
     9 signature BASIC_SIMPLIFIER =
    10 sig
    11   include BASIC_META_SIMPLIFIER
    12   val change_simpset: (simpset -> simpset) -> unit
    13   val simpset_of: theory -> simpset
    14   val simpset: unit -> simpset
    15   val SIMPSET: (simpset -> tactic) -> tactic
    16   val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
    17   val Addsimps: thm list -> unit
    18   val Delsimps: thm list -> unit
    19   val Addsimprocs: simproc list -> unit
    20   val Delsimprocs: simproc list -> unit
    21   val Addcongs: thm list -> unit
    22   val Delcongs: thm list -> unit
    23   val local_simpset_of: Proof.context -> simpset
    24   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    25   val safe_asm_full_simp_tac: simpset -> int -> tactic
    26   val               simp_tac: simpset -> int -> tactic
    27   val           asm_simp_tac: simpset -> int -> tactic
    28   val          full_simp_tac: simpset -> int -> tactic
    29   val        asm_lr_simp_tac: simpset -> int -> tactic
    30   val      asm_full_simp_tac: simpset -> int -> tactic
    31   val               Simp_tac:            int -> tactic
    32   val           Asm_simp_tac:            int -> tactic
    33   val          Full_simp_tac:            int -> tactic
    34   val        Asm_lr_simp_tac:            int -> tactic
    35   val      Asm_full_simp_tac:            int -> tactic
    36   val          simplify: simpset -> thm -> thm
    37   val      asm_simplify: simpset -> thm -> thm
    38   val     full_simplify: simpset -> thm -> thm
    39   val   asm_lr_simplify: simpset -> thm -> thm
    40   val asm_full_simplify: simpset -> thm -> thm
    41 end;
    42 
    43 signature SIMPLIFIER =
    44 sig
    45   include BASIC_SIMPLIFIER
    46   val clear_ss: simpset -> simpset
    47   val debug_bounds: bool ref
    48   val inherit_context: simpset -> simpset -> simpset
    49   val the_context: simpset -> Proof.context
    50   val context: Proof.context -> simpset -> simpset
    51   val theory_context: theory  -> simpset -> simpset
    52   val simproc_i: theory -> string -> term list
    53     -> (theory -> simpset -> term -> thm option) -> simproc
    54   val simproc: theory -> string -> string list
    55     -> (theory -> simpset -> term -> thm option) -> simproc
    56   val          rewrite: simpset -> conv
    57   val      asm_rewrite: simpset -> conv
    58   val     full_rewrite: simpset -> conv
    59   val   asm_lr_rewrite: simpset -> conv
    60   val asm_full_rewrite: simpset -> conv
    61   val get_ss: Context.generic -> simpset
    62   val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
    63   val attrib: (simpset * thm list -> simpset) -> attribute
    64   val simp_add: attribute
    65   val simp_del: attribute
    66   val cong_add: attribute
    67   val cong_del: attribute
    68   val map_simpset: (simpset -> simpset) -> theory -> theory
    69   val get_simproc: Context.generic -> xstring -> simproc
    70   val def_simproc: {name: string, lhss: string list,
    71     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    72     local_theory -> local_theory
    73   val def_simproc_i: {name: string, lhss: term list,
    74     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    75     local_theory -> local_theory
    76   val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    77   val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    78   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    79   val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
    80     -> theory -> theory
    81   val easy_setup: thm -> thm list -> theory -> theory
    82 end;
    83 
    84 structure Simplifier: SIMPLIFIER =
    85 struct
    86 
    87 open MetaSimplifier;
    88 
    89 
    90 (** simpset data **)
    91 
    92 structure SimpsetData = GenericDataFun
    93 (
    94   type T = simpset;
    95   val empty = empty_ss;
    96   fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
    97   fun merge _ = merge_ss;
    98 );
    99 
   100 val get_ss = SimpsetData.get;
   101 val map_ss = SimpsetData.map;
   102 
   103 
   104 (* attributes *)
   105 
   106 fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
   107 
   108 val simp_add = attrib (op addsimps);
   109 val simp_del = attrib (op delsimps);
   110 val cong_add = attrib (op addcongs);
   111 val cong_del = attrib (op delcongs);
   112 
   113 
   114 (* global simpset *)
   115 
   116 fun map_simpset f = Context.theory_map (map_ss f);
   117 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   118 fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
   119 val simpset = simpset_of o ML_Context.the_global_context;
   120 
   121 fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
   122 fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
   123 
   124 fun Addsimps args = change_simpset (fn ss => ss addsimps args);
   125 fun Delsimps args = change_simpset (fn ss => ss delsimps args);
   126 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   127 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   128 fun Addcongs args = change_simpset (fn ss => ss addcongs args);
   129 fun Delcongs args = change_simpset (fn ss => ss delcongs args);
   130 
   131 
   132 (* local simpset *)
   133 
   134 fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
   135 
   136 val _ = ML_Antiquote.value "simpset"
   137   (Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())");
   138 
   139 
   140 
   141 (** named simprocs **)
   142 
   143 fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
   144 
   145 
   146 (* data *)
   147 
   148 structure Simprocs = GenericDataFun
   149 (
   150   type T = simproc NameSpace.table;
   151   val empty = NameSpace.empty_table;
   152   val extend = I;
   153   fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
   154     handle Symtab.DUP dup => err_dup_simproc dup;
   155 );
   156 
   157 
   158 (* get simprocs *)
   159 
   160 fun get_simproc context xname =
   161   let
   162     val (space, tab) = Simprocs.get context;
   163     val name = NameSpace.intern space xname;
   164   in
   165     (case Symtab.lookup tab name of
   166       SOME proc => proc
   167     | NONE => error ("Undefined simplification procedure: " ^ quote name))
   168   end;
   169 
   170 val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
   171   "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
   172 
   173 
   174 (* define simprocs *)
   175 
   176 local
   177 
   178 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   179   let
   180     val b = Binding.name name;
   181     val naming = LocalTheory.full_naming lthy;
   182     val simproc = make_simproc
   183       {name = LocalTheory.full_name lthy b,
   184        lhss =
   185         let
   186           val lhss' = prep lthy lhss;
   187           val ctxt' = lthy
   188             |> fold Variable.declare_term lhss'
   189             |> fold Variable.auto_fixes lhss';
   190         in Variable.export_terms ctxt' lthy lhss' end
   191         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
   192        proc = proc,
   193        identifier = identifier}
   194       |> morph_simproc (LocalTheory.target_morphism lthy);
   195   in
   196     lthy |> LocalTheory.declaration (fn phi =>
   197       let
   198         val b' = Morphism.binding phi b;
   199         val simproc' = morph_simproc phi simproc;
   200       in
   201         Simprocs.map (fn simprocs =>
   202           NameSpace.bind naming (b', simproc') simprocs |> snd
   203             handle Symtab.DUP dup => err_dup_simproc dup)
   204         #> map_ss (fn ss => ss addsimprocs [simproc'])
   205       end)
   206   end;
   207 
   208 in
   209 
   210 val def_simproc = gen_simproc Syntax.read_terms;
   211 val def_simproc_i = gen_simproc Syntax.check_terms;
   212 
   213 end;
   214 
   215 
   216 
   217 (** simplification tactics and rules **)
   218 
   219 fun solve_all_tac solvers ss =
   220   let
   221     val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
   222     val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   223   in DEPTH_SOLVE (solve_tac 1) end;
   224 
   225 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   226 fun generic_simp_tac safe mode ss =
   227   let
   228     val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
   229     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
   230     val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
   231       (rev (if safe then solvers else unsafe_solvers)));
   232 
   233     fun simp_loop_tac i =
   234       asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
   235       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   236   in simp_loop_tac end;
   237 
   238 local
   239 
   240 fun simp rew mode ss thm =
   241   let
   242     val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
   243     val tacf = solve_all_tac (rev unsafe_solvers);
   244     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   245   in rew mode prover ss thm end;
   246 
   247 in
   248 
   249 val simp_thm = simp MetaSimplifier.rewrite_thm;
   250 val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   251 
   252 end;
   253 
   254 
   255 (* tactics *)
   256 
   257 val simp_tac = generic_simp_tac false (false, false, false);
   258 val asm_simp_tac = generic_simp_tac false (false, true, false);
   259 val full_simp_tac = generic_simp_tac false (true, false, false);
   260 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   261 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   262 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   263 
   264 (*the abstraction over the proof state delays the dereferencing*)
   265 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   266 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   267 fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   268 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   269 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   270 
   271 
   272 (* conversions *)
   273 
   274 val          simplify = simp_thm (false, false, false);
   275 val      asm_simplify = simp_thm (false, true, false);
   276 val     full_simplify = simp_thm (true, false, false);
   277 val   asm_lr_simplify = simp_thm (true, true, false);
   278 val asm_full_simplify = simp_thm (true, true, true);
   279 
   280 val          rewrite = simp_cterm (false, false, false);
   281 val      asm_rewrite = simp_cterm (false, true, false);
   282 val     full_rewrite = simp_cterm (true, false, false);
   283 val   asm_lr_rewrite = simp_cterm (true, true, false);
   284 val asm_full_rewrite = simp_cterm (true, true, true);
   285 
   286 
   287 
   288 (** concrete syntax of attributes **)
   289 
   290 (* add / del *)
   291 
   292 val simpN = "simp";
   293 val congN = "cong";
   294 val addN = "add";
   295 val delN = "del";
   296 val onlyN = "only";
   297 val no_asmN = "no_asm";
   298 val no_asm_useN = "no_asm_use";
   299 val no_asm_simpN = "no_asm_simp";
   300 val asm_lrN = "asm_lr";
   301 
   302 
   303 (* simprocs *)
   304 
   305 local
   306 
   307 val add_del =
   308   (Args.del -- Args.colon >> K (op delsimprocs) ||
   309     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   310   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   311       (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
   312 
   313 in
   314 
   315 val simproc_att = Attrib.syntax
   316   (Scan.peek (fn context =>
   317     add_del :|-- (fn decl =>
   318       Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
   319       >> (Library.apply o map Morphism.form))));
   320 
   321 end;
   322 
   323 
   324 (* conversions *)
   325 
   326 local
   327 
   328 fun conv_mode x =
   329   ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   330     Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   331     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   332     Scan.succeed asm_full_simplify) |> Scan.lift) x;
   333 
   334 in
   335 
   336 val simplified =
   337   Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
   338     f ((if null ths then I else MetaSimplifier.clear_ss)
   339         (local_simpset_of (Context.proof_of context)) addsimps ths))));
   340 
   341 end;
   342 
   343 
   344 (* setup attributes *)
   345 
   346 val _ = Context.>> (Context.map_theory
   347  (Attrib.add_attributes
   348    [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
   349     (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
   350     ("simproc", simproc_att, "declaration of simplification procedures"),
   351     ("simplified", simplified, "simplified rule")]));
   352 
   353 
   354 
   355 (** proof methods **)
   356 
   357 (* simplification *)
   358 
   359 val simp_options =
   360  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   361   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   362   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   363   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   364   Scan.succeed asm_full_simp_tac);
   365 
   366 val cong_modifiers =
   367  [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
   368   Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
   369   Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
   370 
   371 val simp_modifiers =
   372  [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
   373   Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   374   Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
   375   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   376     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   377    @ cong_modifiers;
   378 
   379 val simp_modifiers' =
   380  [Args.add -- Args.colon >> K (I, simp_add),
   381   Args.del -- Args.colon >> K (I, simp_del),
   382   Args.$$$ onlyN -- Args.colon
   383     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   384    @ cong_modifiers;
   385 
   386 fun simp_args more_mods =
   387   Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
   388     (more_mods @ simp_modifiers');
   389 
   390 fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   391   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   392     (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
   393 
   394 fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   395   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   396       ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   397 
   398 
   399 
   400 (** setup **)
   401 
   402 fun method_setup more_mods = Method.add_methods
   403  [(simpN, simp_args more_mods simp_method', "simplification"),
   404   ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   405 
   406 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   407   let
   408     val trivialities = Drule.reflexive_thm :: trivs;
   409 
   410     fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
   411     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   412 
   413     (*no premature instantiation of variables during simplification*)
   414     fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   415     val safe_solver = mk_solver "easy safe" safe_solver_tac;
   416 
   417     fun mk_eq thm =
   418       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
   419       else [thm RS reflect] handle THM _ => [];
   420 
   421     fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   422   in
   423     empty_ss setsubgoaler asm_simp_tac
   424     setSSolver safe_solver
   425     setSolver unsafe_solver
   426     setmksimps mksimps
   427   end));
   428 
   429 end;
   430 
   431 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   432 open BasicSimplifier;