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