src/Pure/simplifier.ML
author haftmann
Thu Nov 20 19:06:02 2008 +0100 (2008-11-20)
changeset 28863 32e83a854e5e
parent 28792 1d80cee865de
child 28965 1de908189869
permissions -rw-r--r--
dropped legacy naming code
     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 naming = LocalTheory.full_naming lthy;
   181     val simproc = make_simproc
   182       {name = LocalTheory.full_name lthy name,
   183        lhss =
   184         let
   185           val lhss' = prep lthy lhss;
   186           val ctxt' = lthy
   187             |> fold Variable.declare_term lhss'
   188             |> fold Variable.auto_fixes lhss';
   189         in Variable.export_terms ctxt' lthy lhss' end
   190         |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
   191        proc = proc,
   192        identifier = identifier}
   193       |> morph_simproc (LocalTheory.target_morphism lthy);
   194   in
   195     lthy |> LocalTheory.declaration (fn phi =>
   196       let
   197         val b' = Morphism.name phi (Name.binding name);
   198         val simproc' = morph_simproc phi simproc;
   199       in
   200         Simprocs.map (fn simprocs =>
   201           NameSpace.table_declare naming (b', simproc') simprocs |> snd
   202             handle Symtab.DUP dup => err_dup_simproc dup)
   203         #> map_ss (fn ss => ss addsimprocs [simproc'])
   204       end)
   205   end;
   206 
   207 in
   208 
   209 val def_simproc = gen_simproc Syntax.read_terms;
   210 val def_simproc_i = gen_simproc Syntax.check_terms;
   211 
   212 end;
   213 
   214 
   215 
   216 (** simplification tactics and rules **)
   217 
   218 fun solve_all_tac solvers ss =
   219   let
   220     val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
   221     val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   222   in DEPTH_SOLVE (solve_tac 1) end;
   223 
   224 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   225 fun generic_simp_tac safe mode ss =
   226   let
   227     val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
   228     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
   229     val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
   230       (rev (if safe then solvers else unsafe_solvers)));
   231 
   232     fun simp_loop_tac i =
   233       asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
   234       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   235   in simp_loop_tac end;
   236 
   237 local
   238 
   239 fun simp rew mode ss thm =
   240   let
   241     val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
   242     val tacf = solve_all_tac (rev unsafe_solvers);
   243     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   244   in rew mode prover ss thm end;
   245 
   246 in
   247 
   248 val simp_thm = simp MetaSimplifier.rewrite_thm;
   249 val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   250 
   251 end;
   252 
   253 
   254 (* tactics *)
   255 
   256 val simp_tac = generic_simp_tac false (false, false, false);
   257 val asm_simp_tac = generic_simp_tac false (false, true, false);
   258 val full_simp_tac = generic_simp_tac false (true, false, false);
   259 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   260 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   261 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   262 
   263 (*the abstraction over the proof state delays the dereferencing*)
   264 fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   265 fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   266 fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   267 fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   268 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   269 
   270 
   271 (* conversions *)
   272 
   273 val          simplify = simp_thm (false, false, false);
   274 val      asm_simplify = simp_thm (false, true, false);
   275 val     full_simplify = simp_thm (true, false, false);
   276 val   asm_lr_simplify = simp_thm (true, true, false);
   277 val asm_full_simplify = simp_thm (true, true, true);
   278 
   279 val          rewrite = simp_cterm (false, false, false);
   280 val      asm_rewrite = simp_cterm (false, true, false);
   281 val     full_rewrite = simp_cterm (true, false, false);
   282 val   asm_lr_rewrite = simp_cterm (true, true, false);
   283 val asm_full_rewrite = simp_cterm (true, true, true);
   284 
   285 
   286 
   287 (** concrete syntax of attributes **)
   288 
   289 (* add / del *)
   290 
   291 val simpN = "simp";
   292 val congN = "cong";
   293 val addN = "add";
   294 val delN = "del";
   295 val onlyN = "only";
   296 val no_asmN = "no_asm";
   297 val no_asm_useN = "no_asm_use";
   298 val no_asm_simpN = "no_asm_simp";
   299 val asm_lrN = "asm_lr";
   300 
   301 
   302 (* simprocs *)
   303 
   304 local
   305 
   306 val add_del =
   307   (Args.del -- Args.colon >> K (op delsimprocs) ||
   308     Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   309   >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   310       (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
   311 
   312 in
   313 
   314 val simproc_att = Attrib.syntax
   315   (Scan.peek (fn context =>
   316     add_del :|-- (fn decl =>
   317       Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
   318       >> (Library.apply o map Morphism.form))));
   319 
   320 end;
   321 
   322 
   323 (* conversions *)
   324 
   325 local
   326 
   327 fun conv_mode x =
   328   ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   329     Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   330     Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   331     Scan.succeed asm_full_simplify) |> Scan.lift) x;
   332 
   333 in
   334 
   335 val simplified =
   336   Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
   337     f ((if null ths then I else MetaSimplifier.clear_ss)
   338         (local_simpset_of (Context.proof_of context)) addsimps ths))));
   339 
   340 end;
   341 
   342 
   343 (* setup attributes *)
   344 
   345 val _ = Context.>> (Context.map_theory
   346  (Attrib.add_attributes
   347    [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
   348     (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
   349     ("simproc", simproc_att, "declaration of simplification procedures"),
   350     ("simplified", simplified, "simplified rule")]));
   351 
   352 
   353 
   354 (** proof methods **)
   355 
   356 (* simplification *)
   357 
   358 val simp_options =
   359  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   360   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   361   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   362   Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   363   Scan.succeed asm_full_simp_tac);
   364 
   365 val cong_modifiers =
   366  [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
   367   Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
   368   Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
   369 
   370 val simp_modifiers =
   371  [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
   372   Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   373   Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
   374   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
   375     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   376    @ cong_modifiers;
   377 
   378 val simp_modifiers' =
   379  [Args.add -- Args.colon >> K (I, simp_add),
   380   Args.del -- Args.colon >> K (I, simp_del),
   381   Args.$$$ onlyN -- Args.colon
   382     >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
   383    @ cong_modifiers;
   384 
   385 fun simp_args more_mods =
   386   Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options)
   387     (more_mods @ simp_modifiers');
   388 
   389 fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   390   ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   391     (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
   392 
   393 fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   394   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   395       ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   396 
   397 
   398 
   399 (** setup **)
   400 
   401 fun method_setup more_mods = Method.add_methods
   402  [(simpN, simp_args more_mods simp_method', "simplification"),
   403   ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   404 
   405 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   406   let
   407     val trivialities = Drule.reflexive_thm :: trivs;
   408 
   409     fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
   410     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   411 
   412     (*no premature instantiation of variables during simplification*)
   413     fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   414     val safe_solver = mk_solver "easy safe" safe_solver_tac;
   415 
   416     fun mk_eq thm =
   417       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
   418       else [thm RS reflect] handle THM _ => [];
   419 
   420     fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   421   in
   422     empty_ss setsubgoaler asm_simp_tac
   423     setSSolver safe_solver
   424     setSolver unsafe_solver
   425     setmksimps mksimps
   426   end));
   427 
   428 end;
   429 
   430 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   431 open BasicSimplifier;