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