author | wenzelm |
Sun, 22 Jul 2012 12:26:41 +0200 | |
changeset 48423 | 0ccf143a2a69 |
parent 47468 | 402b753d8383 |
child 48776 | 37cd53e69840 |
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 |
|
41386 | 5 |
raw_simplifier.ML for the actual meta-level rewriting engine). |
16014 | 6 |
*) |
7 |
||
8 |
signature BASIC_SIMPLIFIER = |
|
9 |
sig |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
10 |
include BASIC_RAW_SIMPLIFIER |
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
11 |
val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
12 |
val simpset_of: Proof.context -> 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
|
13 |
val global_simpset_of: theory -> simpset |
16014 | 14 |
val Addsimprocs: simproc list -> unit |
15 |
val Delsimprocs: simproc list -> unit |
|
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 |
35613 | 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 |
|
16014 | 27 |
val asm_full_simplify: simpset -> thm -> thm |
28 |
end; |
|
29 |
||
30 |
signature SIMPLIFIER = |
|
31 |
sig |
|
32 |
include BASIC_SIMPLIFIER |
|
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
33 |
val map_simpset_global: (simpset -> simpset) -> theory -> theory |
30356 | 34 |
val pretty_ss: Proof.context -> simpset -> Pretty.T |
17004 | 35 |
val clear_ss: simpset -> simpset |
47239 | 36 |
val default_mk_sym: simpset -> thm -> thm option |
32738 | 37 |
val debug_bounds: bool Unsynchronized.ref |
43597 | 38 |
val prems_of: simpset -> thm list |
41226 | 39 |
val add_simp: thm -> simpset -> simpset |
40 |
val del_simp: thm -> simpset -> simpset |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
41 |
val add_eqcong: thm -> simpset -> simpset |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
42 |
val del_eqcong: thm -> simpset -> simpset |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
43 |
val add_cong: thm -> simpset -> simpset |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
44 |
val del_cong: thm -> simpset -> simpset |
41226 | 45 |
val add_prems: thm list -> simpset -> simpset |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
46 |
val mksimps: simpset -> thm -> thm list |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
47 |
val set_mksimps: (simpset -> thm -> thm list) -> simpset -> simpset |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
48 |
val set_mkcong: (simpset -> thm -> thm) -> simpset -> simpset |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
49 |
val set_mksym: (simpset -> thm -> thm option) -> simpset -> simpset |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
50 |
val set_mkeqTrue: (simpset -> thm -> thm option) -> simpset -> simpset |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
51 |
val set_termless: (term * term -> bool) -> simpset -> simpset |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
52 |
val set_subgoaler: (simpset -> int -> tactic) -> simpset -> simpset |
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset
|
53 |
val inherit_context: simpset -> simpset -> simpset |
17898 | 54 |
val the_context: simpset -> Proof.context |
55 |
val context: Proof.context -> simpset -> simpset |
|
37441 | 56 |
val global_context: theory -> simpset -> simpset |
36600 | 57 |
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset |
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
58 |
val simproc_global_i: theory -> string -> term list -> |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
59 |
(theory -> simpset -> term -> thm option) -> simproc |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
60 |
val simproc_global: theory -> string -> string list -> |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
61 |
(theory -> simpset -> term -> thm option) -> simproc |
35613 | 62 |
val rewrite: simpset -> conv |
63 |
val asm_rewrite: simpset -> conv |
|
64 |
val full_rewrite: simpset -> conv |
|
65 |
val asm_lr_rewrite: simpset -> conv |
|
23598 | 66 |
val asm_full_rewrite: simpset -> conv |
22379 | 67 |
val get_ss: Context.generic -> simpset |
68 |
val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
69 |
val attrib: (thm -> simpset -> simpset) -> attribute |
18728 | 70 |
val simp_add: attribute |
71 |
val simp_del: attribute |
|
72 |
val cong_add: attribute |
|
73 |
val cong_del: attribute |
|
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
74 |
val check_simproc: Proof.context -> xstring * Position.T -> string |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
75 |
val the_simproc: Proof.context -> string -> simproc |
42464 | 76 |
val def_simproc: {name: binding, lhss: term list, |
22236 | 77 |
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> |
22201 | 78 |
local_theory -> local_theory |
42464 | 79 |
val def_simproc_cmd: {name: binding, lhss: string list, |
22236 | 80 |
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> |
22201 | 81 |
local_theory -> local_theory |
30513 | 82 |
val cong_modifiers: Method.modifier parser list |
83 |
val simp_modifiers': Method.modifier parser list |
|
84 |
val simp_modifiers: Method.modifier parser list |
|
85 |
val method_setup: Method.modifier parser list -> theory -> theory |
|
18708 | 86 |
val easy_setup: thm -> thm list -> theory -> theory |
16014 | 87 |
end; |
88 |
||
89 |
structure Simplifier: SIMPLIFIER = |
|
90 |
struct |
|
91 |
||
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
92 |
open Raw_Simplifier; |
21708 | 93 |
|
94 |
||
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
95 |
(** data **) |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
96 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
97 |
structure Data = Generic_Data |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
98 |
( |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
99 |
type T = simpset * simproc Name_Space.table; |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
100 |
val empty : T = (empty_ss, Name_Space.empty_table "simproc"); |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
101 |
fun extend (ss, tab) = (Raw_Simplifier.inherit_context empty_ss ss, tab); |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
102 |
fun merge ((ss1, tab1), (ss2, tab2)) = |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
103 |
(merge_ss (ss1, ss2), Name_Space.merge_tables (tab1, tab2)); |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
104 |
); |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
105 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
106 |
val get_ss = fst o Data.get; |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
107 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
108 |
fun map_ss f context = |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
109 |
Data.map (apfst ((Raw_Simplifier.with_context (Context.proof_of context) f))) context; |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
110 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
111 |
val get_simprocs = snd o Data.get o Context.Proof; |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
112 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
113 |
|
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
114 |
|
30356 | 115 |
(** pretty printing **) |
116 |
||
117 |
fun pretty_ss ctxt ss = |
|
118 |
let |
|
119 |
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
|
120 |
val pretty_thm = Display.pretty_thm ctxt; |
30356 | 121 |
fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss); |
122 |
fun pretty_cong (name, thm) = |
|
123 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm]; |
|
124 |
||
125 |
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss; |
|
126 |
in |
|
127 |
[Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps), |
|
128 |
Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)), |
|
129 |
Pretty.big_list "congruences:" (map pretty_cong congs), |
|
130 |
Pretty.strs ("loopers:" :: map quote loopers), |
|
131 |
Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), |
|
132 |
Pretty.strs ("safe solvers:" :: map quote safe_solvers)] |
|
133 |
|> Pretty.chunks |
|
134 |
end; |
|
135 |
||
136 |
||
137 |
||
17883
efa1bc2bdcc6
removed obsolete/experimental context components (superceded by Simplifier.the_context);
wenzelm
parents:
17723
diff
changeset
|
138 |
(** simpset data **) |
16014 | 139 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
140 |
(* attributes *) |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
141 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
142 |
fun attrib f = Thm.declaration_attribute (map_ss o f); |
16014 | 143 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
144 |
val simp_add = attrib add_simp; |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
145 |
val simp_del = attrib del_simp; |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
146 |
val cong_add = attrib add_cong; |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
147 |
val cong_del = attrib del_cong; |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
148 |
|
16014 | 149 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
150 |
(* local simpset *) |
16014 | 151 |
|
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
152 |
fun map_simpset f = Context.proof_map (map_ss f); |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
153 |
fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt)); |
16014 | 154 |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
155 |
val _ = Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
156 |
(ML_Antiquote.value (Binding.name "simpset") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
157 |
(Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())"))); |
22132 | 158 |
|
16014 | 159 |
|
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
160 |
(* global simpset *) |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
161 |
|
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
162 |
fun map_simpset_global f = Context.theory_map (map_ss f); |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
163 |
fun global_simpset_of thy = |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
164 |
Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy)); |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
165 |
|
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
166 |
fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args)); |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
167 |
fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args)); |
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
168 |
|
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42793
diff
changeset
|
169 |
|
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
170 |
|
22201 | 171 |
(** named simprocs **) |
172 |
||
22204 | 173 |
(* get simprocs *) |
174 |
||
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
175 |
fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1; |
42466 | 176 |
val the_simproc = Name_Space.get o get_simprocs; |
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
177 |
|
42464 | 178 |
val _ = |
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
179 |
Context.>> (Context.map_theory |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
180 |
(ML_Antiquote.value (Binding.name "simproc") |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
181 |
(Args.context -- Scan.lift (Parse.position Args.name) |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
182 |
>> (fn (ctxt, name) => |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
183 |
"Simplifier.the_simproc (ML_Context.the_local_context ()) " ^ |
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42795
diff
changeset
|
184 |
ML_Syntax.print_string (check_simproc ctxt name))))); |
22204 | 185 |
|
186 |
||
187 |
(* define simprocs *) |
|
22201 | 188 |
|
189 |
local |
|
190 |
||
42464 | 191 |
fun gen_simproc prep {name = b, lhss, proc, identifier} lthy = |
22201 | 192 |
let |
22236 | 193 |
val simproc = make_simproc |
47001
a0e370d3d149
proper naming of simprocs according to actual target context;
wenzelm
parents:
46776
diff
changeset
|
194 |
{name = Local_Theory.full_name lthy b, |
22236 | 195 |
lhss = |
196 |
let |
|
197 |
val lhss' = prep lthy lhss; |
|
45326
8fa859aebc0d
tuned -- Variable.declare_term is already part of Variable.auto_fixes;
wenzelm
parents:
45291
diff
changeset
|
198 |
val ctxt' = fold Variable.auto_fixes lhss' lthy; |
22236 | 199 |
in Variable.export_terms ctxt' lthy lhss' end |
42360 | 200 |
|> map (Thm.cterm_of (Proof_Context.theory_of lthy)), |
22236 | 201 |
proc = proc, |
33551
c40ced05b10a
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
wenzelm
parents:
33519
diff
changeset
|
202 |
identifier = identifier}; |
22201 | 203 |
in |
47001
a0e370d3d149
proper naming of simprocs according to actual target context;
wenzelm
parents:
46776
diff
changeset
|
204 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => |
22201 | 205 |
let |
28991 | 206 |
val b' = Morphism.binding phi b; |
45290 | 207 |
val simproc' = transform_simproc phi simproc; |
22201 | 208 |
in |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42372
diff
changeset
|
209 |
context |
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
210 |
|> Data.map (fn (ss, tab) => |
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
47001
diff
changeset
|
211 |
(ss addsimprocs [simproc'], #2 (Name_Space.define context true (b', simproc') tab))) |
22201 | 212 |
end) |
213 |
end; |
|
214 |
||
215 |
in |
|
216 |
||
42464 | 217 |
val def_simproc = gen_simproc Syntax.check_terms; |
218 |
val def_simproc_cmd = gen_simproc Syntax.read_terms; |
|
22201 | 219 |
|
220 |
end; |
|
221 |
||
222 |
||
223 |
||
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
224 |
(** simplification tactics and rules **) |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
225 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
226 |
fun solve_all_tac solvers ss = |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
227 |
let |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
228 |
val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss ss; |
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
229 |
val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
230 |
in DEPTH_SOLVE (solve_tac 1) end; |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
231 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
232 |
(*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
|
233 |
fun generic_simp_tac safe mode ss = |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
234 |
let |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
235 |
val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = Raw_Simplifier.internal_ss ss; |
21286
b5e7b80caa6a
introduces canonical AList functions for loop_tacs
haftmann
parents:
20872
diff
changeset
|
236 |
val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
237 |
val solve_tac = FIRST' (map (Raw_Simplifier.solver ss) |
22717 | 238 |
(rev (if safe then solvers else unsafe_solvers))); |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
239 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
240 |
fun simp_loop_tac i = |
46465 | 241 |
Raw_Simplifier.generic_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
|
242 |
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
47468
402b753d8383
outermost SELECT_GOAL potentially improves performance;
wenzelm
parents:
47239
diff
changeset
|
243 |
in SELECT_GOAL (simp_loop_tac 1) end; |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
244 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
245 |
local |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
246 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
247 |
fun simp rew mode ss thm = |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
248 |
let |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
249 |
val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss ss; |
22717 | 250 |
val tacf = solve_all_tac (rev unsafe_solvers); |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
251 |
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
|
252 |
in rew mode prover ss thm end; |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
253 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
254 |
in |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
255 |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
256 |
val simp_thm = simp Raw_Simplifier.rewrite_thm; |
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
257 |
val simp_cterm = simp Raw_Simplifier.rewrite_cterm; |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
258 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
259 |
end; |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
260 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
261 |
|
16806 | 262 |
(* tactics *) |
263 |
||
16014 | 264 |
val simp_tac = generic_simp_tac false (false, false, false); |
265 |
val asm_simp_tac = generic_simp_tac false (false, true, false); |
|
266 |
val full_simp_tac = generic_simp_tac false (true, false, false); |
|
267 |
val asm_lr_simp_tac = generic_simp_tac false (true, true, false); |
|
268 |
val asm_full_simp_tac = generic_simp_tac false (true, true, true); |
|
269 |
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true); |
|
270 |
||
16806 | 271 |
|
272 |
(* conversions *) |
|
273 |
||
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
274 |
val simplify = simp_thm (false, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
275 |
val asm_simplify = simp_thm (false, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
276 |
val full_simplify = simp_thm (true, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
277 |
val asm_lr_simplify = simp_thm (true, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
278 |
val asm_full_simplify = simp_thm (true, true, true); |
16014 | 279 |
|
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
280 |
val rewrite = simp_cterm (false, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
281 |
val asm_rewrite = simp_cterm (false, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
282 |
val full_rewrite = simp_cterm (true, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
283 |
val asm_lr_rewrite = simp_cterm (true, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
284 |
val asm_full_rewrite = simp_cterm (true, true, true); |
16014 | 285 |
|
286 |
||
287 |
||
288 |
(** concrete syntax of attributes **) |
|
289 |
||
290 |
(* add / del *) |
|
291 |
||
292 |
val simpN = "simp"; |
|
293 |
val congN = "cong"; |
|
294 |
val onlyN = "only"; |
|
295 |
val no_asmN = "no_asm"; |
|
296 |
val no_asm_useN = "no_asm_use"; |
|
297 |
val no_asm_simpN = "no_asm_simp"; |
|
298 |
val asm_lrN = "asm_lr"; |
|
299 |
||
300 |
||
24024 | 301 |
(* simprocs *) |
302 |
||
303 |
local |
|
304 |
||
305 |
val add_del = |
|
306 |
(Args.del -- Args.colon >> K (op delsimprocs) || |
|
307 |
Scan.option (Args.add -- Args.colon) >> K (op addsimprocs)) |
|
308 |
>> (fn f => fn simproc => fn phi => Thm.declaration_attribute |
|
45290 | 309 |
(K (map_ss (fn ss => f (ss, [transform_simproc phi simproc]))))); |
24024 | 310 |
|
311 |
in |
|
312 |
||
30528 | 313 |
val simproc_att = |
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
314 |
(Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => |
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
315 |
Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt)))) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45326
diff
changeset
|
316 |
>> (fn atts => Thm.declaration_attribute (fn th => |
46776 | 317 |
fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)); |
24024 | 318 |
|
319 |
end; |
|
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset
|
320 |
|
24024 | 321 |
|
16014 | 322 |
(* conversions *) |
323 |
||
324 |
local |
|
325 |
||
326 |
fun conv_mode x = |
|
327 |
((Args.parens (Args.$$$ no_asmN) >> K simplify || |
|
328 |
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify || |
|
329 |
Args.parens (Args.$$$ no_asm_useN) >> K full_simplify || |
|
330 |
Scan.succeed asm_full_simplify) |> Scan.lift) x; |
|
331 |
||
332 |
in |
|
333 |
||
30528 | 334 |
val simplified = conv_mode -- Attrib.thms >> |
335 |
(fn (f, ths) => Thm.rule_attribute (fn context => |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
336 |
f ((if null ths then I else Raw_Simplifier.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
|
337 |
(simpset_of (Context.proof_of context)) addsimps ths))); |
16014 | 338 |
|
339 |
end; |
|
340 |
||
341 |
||
342 |
(* setup attributes *) |
|
343 |
||
26463 | 344 |
val _ = Context.>> (Context.map_theory |
30528 | 345 |
(Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del) |
346 |
"declaration of Simplifier rewrite rule" #> |
|
347 |
Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del) |
|
348 |
"declaration of Simplifier congruence rule" #> |
|
33671 | 349 |
Attrib.setup (Binding.name "simproc") simproc_att |
350 |
"declaration of simplification procedures" #> |
|
30528 | 351 |
Attrib.setup (Binding.name "simplified") simplified "simplified rule")); |
16014 | 352 |
|
353 |
||
354 |
||
31300 | 355 |
(** method syntax **) |
16014 | 356 |
|
357 |
val cong_modifiers = |
|
18728 | 358 |
[Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier), |
359 |
Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add), |
|
360 |
Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)]; |
|
16014 | 361 |
|
362 |
val simp_modifiers = |
|
18728 | 363 |
[Args.$$$ simpN -- Args.colon >> K (I, simp_add), |
364 |
Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add), |
|
365 |
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
|
366 |
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
367 |
>> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)] |
16014 | 368 |
@ cong_modifiers; |
369 |
||
370 |
val simp_modifiers' = |
|
18728 | 371 |
[Args.add -- Args.colon >> K (I, simp_add), |
372 |
Args.del -- Args.colon >> K (I, simp_del), |
|
18688 | 373 |
Args.$$$ onlyN -- Args.colon |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
374 |
>> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)] |
16014 | 375 |
@ cong_modifiers; |
376 |
||
31300 | 377 |
val simp_options = |
378 |
(Args.parens (Args.$$$ no_asmN) >> K simp_tac || |
|
379 |
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac || |
|
380 |
Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac || |
|
381 |
Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac || |
|
382 |
Scan.succeed asm_full_simp_tac); |
|
16014 | 383 |
|
31300 | 384 |
fun simp_method more_mods meth = |
35613 | 385 |
Scan.lift simp_options --| |
31300 | 386 |
Method.sections (more_mods @ simp_modifiers') >> |
35613 | 387 |
(fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts)); |
16014 | 388 |
|
389 |
||
390 |
||
18708 | 391 |
(** setup **) |
392 |
||
31300 | 393 |
fun method_setup more_mods = |
394 |
Method.setup (Binding.name simpN) |
|
395 |
(simp_method more_mods (fn ctxt => fn tac => fn facts => |
|
396 |
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
|
397 |
(CHANGED_PROP oo tac) (simpset_of ctxt)))) |
31300 | 398 |
"simplification" #> |
399 |
Method.setup (Binding.name "simp_all") |
|
400 |
(simp_method more_mods (fn ctxt => fn tac => fn facts => |
|
401 |
ALLGOALS (Method.insert_tac facts) THEN |
|
42372 | 402 |
(CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) (simpset_of ctxt))) |
31300 | 403 |
"simplification (all goals)"; |
16014 | 404 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
405 |
fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ => |
16014 | 406 |
let |
407 |
val trivialities = Drule.reflexive_thm :: trivs; |
|
408 |
||
43597 | 409 |
fun unsafe_solver_tac ss = |
410 |
FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac]; |
|
16014 | 411 |
val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; |
412 |
||
413 |
(*no premature instantiation of variables during simplification*) |
|
43597 | 414 |
fun safe_solver_tac ss = |
415 |
FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac]; |
|
16014 | 416 |
val safe_solver = mk_solver "easy safe" safe_solver_tac; |
417 |
||
418 |
fun mk_eq thm = |
|
20872 | 419 |
if can Logic.dest_equals (Thm.concl_of thm) then [thm] |
16014 | 420 |
else [thm RS reflect] handle THM _ => []; |
421 |
||
44058 | 422 |
fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm); |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
423 |
in |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
424 |
empty_ss |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
425 |
setSSolver safe_solver |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
426 |
setSolver unsafe_solver |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
427 |
|> set_subgoaler asm_simp_tac |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
428 |
|> set_mksimps (K mksimps) |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
429 |
end)); |
16014 | 430 |
|
431 |
end; |
|
432 |
||
32738 | 433 |
structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier; |
434 |
open Basic_Simplifier; |