1 (* Title: Pure/simplifier.ML
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
5 Generic simplifier, suitable for most logics (see also
6 meta_simplifier.ML for the actual meta-level rewriting engine).
9 signature BASIC_SIMPLIFIER =
11 include BASIC_META_SIMPLIFIER
12 val print_simpset: theory -> unit
13 val change_simpset_of: theory -> (simpset -> simpset) -> unit
14 val change_simpset: (simpset -> simpset) -> unit
15 val simpset_of: theory -> simpset
16 val simpset: unit -> simpset
17 val SIMPSET: (simpset -> tactic) -> tactic
18 val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
19 val Addsimps: thm list -> unit
20 val Delsimps: thm list -> unit
21 val Addsimprocs: simproc list -> unit
22 val Delsimprocs: simproc list -> unit
23 val Addcongs: thm list -> unit
24 val Delcongs: thm list -> unit
25 val local_simpset_of: Proof.context -> simpset
26 val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
27 val safe_asm_full_simp_tac: simpset -> int -> tactic
28 val simp_tac: simpset -> int -> tactic
29 val asm_simp_tac: simpset -> int -> tactic
30 val full_simp_tac: simpset -> int -> tactic
31 val asm_lr_simp_tac: simpset -> int -> tactic
32 val asm_full_simp_tac: simpset -> int -> tactic
33 val Simp_tac: int -> tactic
34 val Asm_simp_tac: int -> tactic
35 val Full_simp_tac: int -> tactic
36 val Asm_lr_simp_tac: int -> tactic
37 val Asm_full_simp_tac: int -> tactic
38 val simplify: simpset -> thm -> thm
39 val asm_simplify: simpset -> thm -> thm
40 val full_simplify: simpset -> thm -> thm
41 val asm_lr_simplify: simpset -> thm -> thm
42 val asm_full_simplify: simpset -> thm -> thm
45 signature SIMPLIFIER =
47 include BASIC_SIMPLIFIER
48 val clear_ss: simpset -> simpset
49 val debug_bounds: bool ref
50 val inherit_context: simpset -> simpset -> simpset
51 val the_context: simpset -> Proof.context
52 val context: Proof.context -> simpset -> simpset
53 val theory_context: theory -> simpset -> simpset
54 val simproc_i: theory -> string -> term list
55 -> (theory -> simpset -> term -> thm option) -> simproc
56 val simproc: theory -> string -> string list
57 -> (theory -> simpset -> term -> thm option) -> simproc
58 val rewrite: simpset -> cterm -> thm
59 val asm_rewrite: simpset -> cterm -> thm
60 val full_rewrite: simpset -> cterm -> thm
61 val asm_lr_rewrite: simpset -> cterm -> thm
62 val asm_full_rewrite: simpset -> cterm -> thm
63 val get_simpset: theory -> simpset
64 val print_local_simpset: Proof.context -> unit
65 val get_local_simpset: Proof.context -> simpset
66 val put_local_simpset: simpset -> Proof.context -> Proof.context
67 val get_ss: Context.generic -> simpset
68 val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
69 val attrib: (simpset * thm list -> simpset) -> attribute
70 val simp_add: attribute
71 val simp_del: attribute
72 val cong_add: attribute
73 val cong_del: attribute
74 val get_simproc: Proof.context -> xstring -> simproc
75 val def_simproc: {name: string, lhss: string list,
76 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
77 local_theory -> local_theory
78 val def_simproc_i: {name: string, lhss: term list,
79 proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
80 local_theory -> local_theory
81 val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
82 val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
83 val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
84 val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
86 val easy_setup: thm -> thm list -> theory -> theory
89 structure Simplifier: SIMPLIFIER =
99 structure GlobalSimpset = TheoryDataFun
101 val name = "Pure/simpset";
102 type T = simpset ref;
104 val empty = ref empty_ss;
105 fun copy (ref ss) = ref ss: T; (*create new reference!*)
106 fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss);
107 fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
108 fun print _ (ref ss) = print_ss ss;
111 val _ = Context.add_setup GlobalSimpset.init;
112 val print_simpset = GlobalSimpset.print;
113 val get_simpset = ! o GlobalSimpset.get;
115 val change_simpset_of = change o GlobalSimpset.get;
116 fun change_simpset f = change_simpset_of (ML_Context.the_context ()) f;
118 fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
119 val simpset = simpset_of o ML_Context.the_context;
122 fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;
123 fun SIMPSET' tacf i st = tacf (simpset_of (Thm.theory_of_thm st)) i st;
125 fun Addsimps args = change_simpset (fn ss => ss addsimps args);
126 fun Delsimps args = change_simpset (fn ss => ss delsimps args);
127 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
128 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
129 fun Addcongs args = change_simpset (fn ss => ss addcongs args);
130 fun Delcongs args = change_simpset (fn ss => ss delcongs args);
135 structure LocalSimpset = ProofDataFun
137 val name = "Pure/simpset";
139 val init = get_simpset;
140 fun print _ ss = print_ss ss;
143 val _ = Context.add_setup LocalSimpset.init;
144 val print_local_simpset = LocalSimpset.print;
145 val get_local_simpset = LocalSimpset.get;
146 val put_local_simpset = LocalSimpset.put;
148 fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_local_simpset ctxt);
150 val _ = ML_Context.value_antiq "simpset"
151 (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
154 (* generic simpsets *)
156 fun get_ss (Context.Theory thy) = simpset_of thy
157 | get_ss (Context.Proof ctxt) = local_simpset_of ctxt;
159 fun map_ss f (Context.Theory thy) = (change_simpset_of thy f; Context.Theory thy)
160 | map_ss f (Context.Proof ctxt) = Context.Proof (LocalSimpset.map f ctxt);
165 fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
167 val simp_add = attrib (op addsimps);
168 val simp_del = attrib (op delsimps);
169 val cong_add = attrib (op addcongs);
170 val cong_del = attrib (op delcongs);
174 (** named simprocs **)
176 fun err_dup_simprocs ds =
177 error ("Duplicate simproc(s): " ^ commas_quote ds);
182 structure Simprocs = GenericDataFun
184 val name = "Pure/simprocs";
185 type T = simproc NameSpace.table;
186 val empty = NameSpace.empty_table;
188 fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
189 handle Symtab.DUPS ds => err_dup_simprocs ds;
192 val _ = Context.add_setup Simprocs.init;
197 fun get_simproc ctxt xname =
199 val (space, tab) = Simprocs.get (Context.Proof ctxt);
200 val name = NameSpace.intern space xname;
202 (case Symtab.lookup tab name of
204 | NONE => error ("Undefined simplification procedure: " ^ quote name))
207 val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name =>
209 "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^ ML_Syntax.print_string name)));
212 (* define simprocs *)
217 fun read_terms ctxt ts =
218 #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) []
219 (map (rpair TypeInfer.logicT) ts));
222 fun cert_terms ctxt ts = map (ProofContext.cert_term ctxt) ts;
224 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
226 val naming = LocalTheory.full_naming lthy;
227 val simproc = make_simproc
228 {name = LocalTheory.full_name lthy name,
231 val lhss' = prep lthy lhss;
233 |> fold Variable.declare_term lhss'
234 |> fold Variable.auto_fixes lhss';
235 in Variable.export_terms ctxt' lthy lhss' end
236 |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
238 identifier = identifier}
239 |> morph_simproc (LocalTheory.target_morphism lthy);
241 lthy |> LocalTheory.declaration (fn phi => fn context =>
243 val name' = Morphism.name phi name;
244 val simproc' = morph_simproc phi simproc;
247 |> Simprocs.map (fn simprocs =>
248 NameSpace.extend_table naming (simprocs, [(name', simproc')])
249 handle Symtab.DUPS ds => err_dup_simprocs ds)
250 |> map_ss (fn ss => ss addsimprocs [simproc'])
256 val def_simproc = gen_simproc read_terms;
257 val def_simproc_i = gen_simproc cert_terms;
263 (** simplification tactics and rules **)
265 fun solve_all_tac solvers ss =
267 val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss;
268 val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
269 in DEPTH_SOLVE (solve_tac 1) end;
271 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
272 fun generic_simp_tac safe mode ss =
274 val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss;
275 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
276 val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
277 (if safe then solvers else unsafe_solvers));
279 fun simp_loop_tac i =
280 Goal.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
281 (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
282 in simp_loop_tac end;
286 fun simp rew mode ss thm =
288 val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss;
289 val tacf = solve_all_tac unsafe_solvers;
290 fun prover s th = Option.map #1 (Seq.pull (tacf s th));
291 in rew mode prover ss thm end;
295 val simp_thm = simp MetaSimplifier.rewrite_thm;
296 val simp_cterm = simp MetaSimplifier.rewrite_cterm;
303 val simp_tac = generic_simp_tac false (false, false, false);
304 val asm_simp_tac = generic_simp_tac false (false, true, false);
305 val full_simp_tac = generic_simp_tac false (true, false, false);
306 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
307 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
308 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
310 (*the abstraction over the proof state delays the dereferencing*)
311 fun Simp_tac i st = simp_tac (simpset ()) i st;
312 fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st;
313 fun Full_simp_tac i st = full_simp_tac (simpset ()) i st;
314 fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st;
315 fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
320 val simplify = simp_thm (false, false, false);
321 val asm_simplify = simp_thm (false, true, false);
322 val full_simplify = simp_thm (true, false, false);
323 val asm_lr_simplify = simp_thm (true, true, false);
324 val asm_full_simplify = simp_thm (true, true, true);
326 val rewrite = simp_cterm (false, false, false);
327 val asm_rewrite = simp_cterm (false, true, false);
328 val full_rewrite = simp_cterm (true, false, false);
329 val asm_lr_rewrite = simp_cterm (true, true, false);
330 val asm_full_rewrite = simp_cterm (true, true, true);
334 (** concrete syntax of attributes **)
343 val no_asmN = "no_asm";
344 val no_asm_useN = "no_asm_use";
345 val no_asm_simpN = "no_asm_simp";
346 val asm_lrN = "asm_lr";
354 ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
355 Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
356 Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
357 Scan.succeed asm_full_simplify) |> Scan.lift) x;
362 Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn x =>
363 f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
368 (* setup attributes *)
370 val _ = Context.add_setup
371 (Attrib.add_attributes
372 [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"),
373 (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
374 ("simplified", simplified, "simplified rule")]);
378 (** proof methods **)
383 (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
384 Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
385 Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
386 Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
387 Scan.succeed asm_full_simp_tac);
389 fun simp_flags x = (Scan.repeat
390 (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
391 >> setmp MetaSimplifier.simp_depth_limit)
392 >> (curry (Library.foldl op o) I o rev)) x;
395 [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
396 Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
397 Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
400 [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
401 Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
402 Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
403 Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
404 >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
407 val simp_modifiers' =
408 [Args.add -- Args.colon >> K (I, simp_add),
409 Args.del -- Args.colon >> K (I, simp_del),
410 Args.$$$ onlyN -- Args.colon
411 >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
414 fun simp_args more_mods =
415 Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options -- Scan.lift simp_flags)
416 (more_mods @ simp_modifiers');
418 fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
419 ALLGOALS (Method.insert_tac (prems @ facts)) THEN
420 (FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
422 fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
423 HEADGOAL (Method.insert_tac (prems @ facts) THEN'
424 ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
430 fun method_setup more_mods = Method.add_methods
431 [(simpN, simp_args more_mods simp_method', "simplification"),
432 ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
434 fun easy_setup reflect trivs = method_setup [] #> (fn thy =>
436 val trivialities = Drule.reflexive_thm :: trivs;
438 fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
439 val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
441 (*no premature instantiation of variables during simplification*)
442 fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
443 val safe_solver = mk_solver "easy safe" safe_solver_tac;
446 if can Logic.dest_equals (Thm.concl_of thm) then [thm]
447 else [thm RS reflect] handle THM _ => [];
449 fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
451 GlobalSimpset.get thy :=
452 empty_ss setsubgoaler asm_simp_tac
453 setSSolver safe_solver
454 setSolver unsafe_solver
461 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
462 open BasicSimplifier;