1(*  Title:      Pure/simplifier.ML
2    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
3
4Generic simplifier, suitable for most logics (see also
5raw_simplifier.ML for the actual meta-level rewriting engine).
6*)
7
8signature BASIC_SIMPLIFIER =
9sig
10  include BASIC_RAW_SIMPLIFIER
11  val simp_tac: Proof.context -> int -> tactic
12  val asm_simp_tac: Proof.context -> int -> tactic
13  val full_simp_tac: Proof.context -> int -> tactic
14  val asm_lr_simp_tac: Proof.context -> int -> tactic
15  val asm_full_simp_tac: Proof.context -> int -> tactic
16  val safe_simp_tac: Proof.context -> int -> tactic
17  val safe_asm_simp_tac: Proof.context -> int -> tactic
18  val safe_full_simp_tac: Proof.context -> int -> tactic
19  val safe_asm_lr_simp_tac: Proof.context -> int -> tactic
20  val safe_asm_full_simp_tac: Proof.context -> int -> tactic
21  val simplify: Proof.context -> thm -> thm
22  val asm_simplify: Proof.context -> thm -> thm
23  val full_simplify: Proof.context -> thm -> thm
24  val asm_lr_simplify: Proof.context -> thm -> thm
25  val asm_full_simplify: Proof.context -> thm -> thm
26end;
27
28signature SIMPLIFIER =
29sig
30  include BASIC_SIMPLIFIER
31  val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
32  val attrib: (thm -> Proof.context -> Proof.context) -> attribute
33  val simp_add: attribute
34  val simp_del: attribute
35  val simp_flip: attribute
36  val cong_add: attribute
37  val cong_del: attribute
38  val check_simproc: Proof.context -> xstring * Position.T -> string
39  val the_simproc: Proof.context -> string -> simproc
40  type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
41  val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
42  val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
43  val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
44  val pretty_simpset: bool -> Proof.context -> Pretty.T
45  val default_mk_sym: Proof.context -> thm -> thm option
46  val prems_of: Proof.context -> thm list
47  val add_simp: thm -> Proof.context -> Proof.context
48  val del_simp: thm -> Proof.context -> Proof.context
49  val init_simpset: thm list -> Proof.context -> Proof.context
50  val add_eqcong: thm -> Proof.context -> Proof.context
51  val del_eqcong: thm -> Proof.context -> Proof.context
52  val add_cong: thm -> Proof.context -> Proof.context
53  val del_cong: thm -> Proof.context -> Proof.context
54  val add_prems: thm list -> Proof.context -> Proof.context
55  val mksimps: Proof.context -> thm -> thm list
56  val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
57  val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
58  val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
59  val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
60  val set_term_ord: term ord -> Proof.context -> Proof.context
61  val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
62  type trace_ops
63  val set_trace_ops: trace_ops -> theory -> theory
64  val rewrite: Proof.context -> conv
65  val asm_rewrite: Proof.context -> conv
66  val full_rewrite: Proof.context -> conv
67  val asm_lr_rewrite: Proof.context -> conv
68  val asm_full_rewrite: Proof.context -> conv
69  val cong_modifiers: Method.modifier parser list
70  val simp_modifiers': Method.modifier parser list
71  val simp_modifiers: Method.modifier parser list
72  val method_setup: Method.modifier parser list -> theory -> theory
73  val unsafe_solver_tac: Proof.context -> int -> tactic
74  val unsafe_solver: solver
75  val safe_solver_tac: Proof.context -> int -> tactic
76  val safe_solver: solver
77end;
78
79structure Simplifier: SIMPLIFIER =
80struct
81
82open Raw_Simplifier;
83
84
85(** declarations **)
86
87(* attributes *)
88
89fun attrib f = Thm.declaration_attribute (map_ss o f);
90
91val simp_add = attrib add_simp;
92val simp_del = attrib del_simp;
93val simp_flip = attrib flip_simp;
94val cong_add = attrib add_cong;
95val cong_del = attrib del_cong;
96
97
98(** named simprocs **)
99
100structure Simprocs = Generic_Data
101(
102  type T = simproc Name_Space.table;
103  val empty : T = Name_Space.empty_table "simproc";
104  val extend = I;
105  fun merge data : T = Name_Space.merge_tables data;
106);
107
108
109(* get simprocs *)
110
111val get_simprocs = Simprocs.get o Context.Proof;
112
113fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
114val the_simproc = Name_Space.get o get_simprocs;
115
116val _ = Theory.setup
117  (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
118    (Args.context -- Scan.lift Args.embedded_position
119      >> (fn (ctxt, name) =>
120        "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
121
122
123(* define simprocs *)
124
125type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
126
127fun make_simproc ctxt name {lhss, proc} =
128  let
129    val ctxt' = fold Proof_Context.augment lhss ctxt;
130    val lhss' = Variable.export_terms ctxt' ctxt lhss;
131  in
132    cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
133  end;
134
135local
136
137fun def_simproc prep b {lhss, proc} lthy =
138  let
139    val simproc =
140      make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
141  in
142    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
143      let
144        val b' = Morphism.binding phi b;
145        val simproc' = transform_simproc phi simproc;
146      in
147        context
148        |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
149        |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
150      end)
151  end;
152
153in
154
155val define_simproc = def_simproc Syntax.check_terms;
156val define_simproc_cmd = def_simproc Syntax.read_terms;
157
158end;
159
160
161
162(** pretty_simpset **)
163
164fun pretty_simpset verbose ctxt =
165  let
166    val pretty_term = Syntax.pretty_term ctxt;
167    val pretty_thm = Thm.pretty_thm ctxt;
168    val pretty_thm_item = Thm.pretty_thm_item ctxt;
169
170    fun pretty_simproc (name, lhss) =
171      Pretty.block
172        (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
173          Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss));
174
175    fun pretty_cong_name (const, name) =
176      pretty_term ((if const then Const else Free) (name, dummyT));
177    fun pretty_cong (name, thm) =
178      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
179
180    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
181      dest_ss (simpset_of ctxt);
182    val simprocs =
183      Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
184  in
185    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
186      Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
187      Pretty.big_list "congruences:" (map pretty_cong congs),
188      Pretty.strs ("loopers:" :: map quote loopers),
189      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
190      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
191    |> Pretty.chunks
192  end;
193
194
195
196(** simplification tactics and rules **)
197
198fun solve_all_tac solvers ctxt =
199  let
200    val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt);
201    val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac);
202  in DEPTH_SOLVE (solve_tac 1) end;
203
204(*NOTE: may instantiate unknowns that appear also in other subgoals*)
205fun generic_simp_tac safe mode ctxt =
206  let
207    val loop_tac = Raw_Simplifier.loop_tac ctxt;
208    val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt;
209    val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
210      (rev (if safe then solvers else unsafe_solvers)));
211
212    fun simp_loop_tac i =
213      Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
214      (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
215  in PREFER_GOAL (simp_loop_tac 1) end;
216
217local
218
219fun simp rew mode ctxt thm =
220  let
221    val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt;
222    val tacf = solve_all_tac (rev unsafe_solvers);
223    fun prover s th = Option.map #1 (Seq.pull (tacf s th));
224  in rew mode prover ctxt thm end;
225
226in
227
228val simp_thm = simp Raw_Simplifier.rewrite_thm;
229val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
230
231end;
232
233
234(* tactics *)
235
236val simp_tac = generic_simp_tac false (false, false, false);
237val asm_simp_tac = generic_simp_tac false (false, true, false);
238val full_simp_tac = generic_simp_tac false (true, false, false);
239val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
240val asm_full_simp_tac = generic_simp_tac false (true, true, true);
241
242(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
243val safe_simp_tac = generic_simp_tac true (false, false, false);
244val safe_asm_simp_tac = generic_simp_tac true (false, true, false);
245val safe_full_simp_tac = generic_simp_tac true (true, false, false);
246val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false);
247val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
248
249
250(* conversions *)
251
252val          simplify = simp_thm (false, false, false);
253val      asm_simplify = simp_thm (false, true, false);
254val     full_simplify = simp_thm (true, false, false);
255val   asm_lr_simplify = simp_thm (true, true, false);
256val asm_full_simplify = simp_thm (true, true, true);
257
258val          rewrite = simp_cterm (false, false, false);
259val      asm_rewrite = simp_cterm (false, true, false);
260val     full_rewrite = simp_cterm (true, false, false);
261val   asm_lr_rewrite = simp_cterm (true, true, false);
262val asm_full_rewrite = simp_cterm (true, true, true);
263
264
265
266(** concrete syntax of attributes **)
267
268(* add / del *)
269
270val simpN = "simp";
271val flipN = "flip"
272val congN = "cong";
273val onlyN = "only";
274val no_asmN = "no_asm";
275val no_asm_useN = "no_asm_use";
276val no_asm_simpN = "no_asm_simp";
277val asm_lrN = "asm_lr";
278
279
280(* simprocs *)
281
282local
283
284val add_del =
285  (Args.del -- Args.colon >> K (op delsimprocs) ||
286    Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
287  >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
288      (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))));
289
290in
291
292val simproc_att =
293  (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
294    Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
295  >> (fn atts => Thm.declaration_attribute (fn th =>
296        fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));
297
298end;
299
300
301(* conversions *)
302
303local
304
305fun conv_mode x =
306  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
307    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
308    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
309    Scan.succeed asm_full_simplify) |> Scan.lift) x;
310
311in
312
313val simplified = conv_mode -- Attrib.thms >>
314  (fn (f, ths) => Thm.rule_attribute ths (fn context =>
315    f ((if null ths then I else Raw_Simplifier.clear_simpset)
316        (Context.proof_of context) addsimps ths)));
317
318end;
319
320
321(* setup attributes *)
322
323val _ = Theory.setup
324 (Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
325    "declaration of Simplifier rewrite rule" #>
326  Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del)
327    "declaration of Simplifier congruence rule" #>
328  Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
329    "declaration of simplification procedures" #>
330  Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
331
332
333
334(** method syntax **)
335
336val cong_modifiers =
337 [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add \<^here>),
338  Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>),
339  Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>)];
340
341val simp_modifiers =
342 [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
343  Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
344  Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
345  Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
346  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
347    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
348   @ cong_modifiers;
349
350val simp_modifiers' =
351 [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
352  Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
353  Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
354  Args.$$$ onlyN -- Args.colon >>
355    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
356   @ cong_modifiers;
357
358val 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
365fun simp_method more_mods meth =
366  Scan.lift simp_options --|
367    Method.sections (more_mods @ simp_modifiers') >>
368    (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));
369
370
371
372(** setup **)
373
374fun method_setup more_mods =
375  Method.setup \<^binding>\<open>simp\<close>
376    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
377      HEADGOAL (Method.insert_tac ctxt facts THEN'
378        (CHANGED_PROP oo tac) ctxt)))
379    "simplification" #>
380  Method.setup \<^binding>\<open>simp_all\<close>
381    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
382      ALLGOALS (Method.insert_tac ctxt facts) THEN
383        (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
384    "simplification (all goals)";
385
386fun unsafe_solver_tac ctxt =
387  FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
388val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
389
390(*no premature instantiation of variables during simplification*)
391fun safe_solver_tac ctxt =
392  FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
393val safe_solver = mk_solver "Pure safe" safe_solver_tac;
394
395val _ =
396  Theory.setup
397    (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
398      empty_simpset ctxt
399      setSSolver safe_solver
400      setSolver unsafe_solver
401      |> set_subgoaler asm_simp_tac)));
402
403end;
404
405structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
406open Basic_Simplifier;
407