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