2 Author: David von Oheimb, TU Muenchen |
2 Author: David von Oheimb, TU Muenchen |
3 |
3 |
4 Combination of classical reasoner and simplifier (depends on |
4 Combination of classical reasoner and simplifier (depends on |
5 splitter.ML, classical.ML, blast.ML). |
5 splitter.ML, classical.ML, blast.ML). |
6 *) |
6 *) |
7 |
|
8 infix 4 addSss addss addss'; |
|
9 |
7 |
10 signature CLASIMP_DATA = |
8 signature CLASIMP_DATA = |
11 sig |
9 sig |
12 structure Splitter: SPLITTER |
10 structure Splitter: SPLITTER |
13 structure Classical: CLASSICAL |
11 structure Classical: CLASSICAL |
14 structure Blast: BLAST |
12 structure Blast: BLAST |
15 sharing type Classical.claset = Blast.claset |
|
16 val notE: thm |
13 val notE: thm |
17 val iffD1: thm |
14 val iffD1: thm |
18 val iffD2: thm |
15 val iffD2: thm |
19 end; |
16 end; |
20 |
17 |
21 signature CLASIMP = |
18 signature CLASIMP = |
22 sig |
19 sig |
23 type claset |
20 val addSss: Proof.context -> Proof.context |
24 type clasimpset |
21 val addss: Proof.context -> Proof.context |
25 val clasimpset_of: Proof.context -> clasimpset |
22 val addss': Proof.context -> Proof.context |
26 val addSss: claset * simpset -> claset |
23 val clarsimp_tac: Proof.context -> int -> tactic |
27 val addss: claset * simpset -> claset |
24 val mk_auto_tac: Proof.context -> int -> int -> tactic |
28 val addss': claset * simpset -> claset |
25 val auto_tac: Proof.context -> tactic |
29 val clarsimp_tac: clasimpset -> int -> tactic |
26 val force_tac: Proof.context -> int -> tactic |
30 val mk_auto_tac: clasimpset -> int -> int -> tactic |
27 val fast_simp_tac: Proof.context -> int -> tactic |
31 val auto_tac: clasimpset -> tactic |
28 val slow_simp_tac: Proof.context -> int -> tactic |
32 val force_tac: clasimpset -> int -> tactic |
29 val best_simp_tac: Proof.context -> int -> tactic |
33 val fast_simp_tac: clasimpset -> int -> tactic |
|
34 val slow_simp_tac: clasimpset -> int -> tactic |
|
35 val best_simp_tac: clasimpset -> int -> tactic |
|
36 val iff_add: attribute |
30 val iff_add: attribute |
37 val iff_add': attribute |
31 val iff_add': attribute |
38 val iff_del: attribute |
32 val iff_del: attribute |
39 val iff_modifiers: Method.modifier parser list |
33 val iff_modifiers: Method.modifier parser list |
40 val clasimp_modifiers: Method.modifier parser list |
34 val clasimp_modifiers: Method.modifier parser list |
47 structure Splitter = Data.Splitter; |
41 structure Splitter = Data.Splitter; |
48 structure Classical = Data.Classical; |
42 structure Classical = Data.Classical; |
49 structure Blast = Data.Blast; |
43 structure Blast = Data.Blast; |
50 |
44 |
51 |
45 |
52 (* type clasimpset *) |
|
53 |
|
54 type claset = Classical.claset; |
|
55 type clasimpset = claset * simpset; |
|
56 |
|
57 fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt); |
|
58 |
|
59 |
|
60 (* simp as classical wrapper *) |
46 (* simp as classical wrapper *) |
61 |
47 |
62 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
48 (*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
63 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true); |
49 val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true); |
64 |
50 |
65 (*Add a simpset to a classical set!*) |
51 fun clasimp f name tac ctxt = |
|
52 Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt; |
|
53 |
|
54 (*Add a simpset to the claset!*) |
66 (*Caution: only one simpset added can be added by each of addSss and addss*) |
55 (*Caution: only one simpset added can be added by each of addSss and addss*) |
67 fun cs addSss ss = |
56 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac; |
68 Classical.addSafter (cs, ("safe_asm_full_simp_tac", CHANGED o safe_asm_full_simp_tac ss)); |
57 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac; |
69 |
58 (* FIXME "asm_lr_simp_tac" !? *) |
70 fun cs addss ss = |
59 val addss' = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_lr_simp_tac; |
71 Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_full_simp_tac ss)); |
|
72 |
|
73 fun cs addss' ss = |
|
74 Classical.addbefore (cs, ("asm_full_simp_tac", CHANGED o Simplifier.asm_lr_simp_tac ss)); |
|
75 |
60 |
76 |
61 |
77 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
62 (* iffs: addition of rules to simpsets and clasets simultaneously *) |
78 |
63 |
79 local |
64 local |
126 end; |
111 end; |
127 |
112 |
128 |
113 |
129 (* tactics *) |
114 (* tactics *) |
130 |
115 |
131 fun clarsimp_tac (cs, ss) = |
116 fun clarsimp_tac ctxt = |
132 safe_asm_full_simp_tac ss THEN_ALL_NEW |
117 safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW |
133 Classical.clarify_tac (cs addSss ss); |
118 Classical.clarify_tac (addSss ctxt); |
134 |
119 |
135 |
120 |
136 (* auto_tac *) |
121 (* auto_tac *) |
137 |
122 |
138 fun blast_depth_tac cs m i thm = |
123 fun blast_depth_tac ctxt m i thm = |
139 Blast.depth_tac cs m i thm |
124 Blast.depth_tac ctxt m i thm |
140 handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); |
125 handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); |
141 |
126 |
142 (* a variant of depth_tac that avoids interference of the simplifier |
127 (* a variant of depth_tac that avoids interference of the simplifier |
143 with dup_step_tac when they are combined by auto_tac *) |
128 with dup_step_tac when they are combined by auto_tac *) |
144 local |
129 local |
145 |
130 |
146 fun slow_step_tac' cs = |
131 fun slow_step_tac' ctxt = |
147 Classical.appWrappers cs |
132 Classical.appWrappers ctxt |
148 (Classical.instp_step_tac cs APPEND' Classical.haz_step_tac cs); |
133 (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt); |
149 |
134 |
150 in |
135 in |
151 |
136 |
152 fun nodup_depth_tac cs m i st = |
137 fun nodup_depth_tac ctxt m i st = |
153 SELECT_GOAL |
138 SELECT_GOAL |
154 (Classical.safe_steps_tac cs 1 THEN_ELSE |
139 (Classical.safe_steps_tac ctxt 1 THEN_ELSE |
155 (DEPTH_SOLVE (nodup_depth_tac cs m 1), |
140 (DEPTH_SOLVE (nodup_depth_tac ctxt m 1), |
156 Classical.inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac |
141 Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac |
157 (slow_step_tac' cs 1 THEN DEPTH_SOLVE (nodup_depth_tac cs (m - 1) 1)))) i st; |
142 (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st; |
158 |
143 |
159 end; |
144 end; |
160 |
145 |
161 (*Designed to be idempotent, except if blast_depth_tac instantiates variables |
146 (*Designed to be idempotent, except if blast_depth_tac instantiates variables |
162 in some of the subgoals*) |
147 in some of the subgoals*) |
163 fun mk_auto_tac (cs, ss) m n = |
148 fun mk_auto_tac ctxt m n = |
164 let |
149 let |
165 val cs' = cs addss ss; |
|
166 val main_tac = |
150 val main_tac = |
167 blast_depth_tac cs m (* fast but can't use wrappers *) |
151 blast_depth_tac ctxt m (* fast but can't use wrappers *) |
168 ORELSE' |
152 ORELSE' |
169 (CHANGED o nodup_depth_tac cs' n); (* slower but more general *) |
153 (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) |
170 in |
154 in |
171 PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ss)) THEN |
155 PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN |
172 TRY (Classical.safe_tac cs) THEN |
156 TRY (Classical.safe_tac ctxt) THEN |
173 REPEAT_DETERM (FIRSTGOAL main_tac) THEN |
157 REPEAT_DETERM (FIRSTGOAL main_tac) THEN |
174 TRY (Classical.safe_tac (cs addSss ss)) THEN |
158 TRY (Classical.safe_tac (addSss ctxt)) THEN |
175 prune_params_tac |
159 prune_params_tac |
176 end; |
160 end; |
177 |
161 |
178 fun auto_tac css = mk_auto_tac css 4 2; |
162 fun auto_tac ctxt = mk_auto_tac ctxt 4 2; |
179 |
163 |
180 |
164 |
181 (* force_tac *) |
165 (* force_tac *) |
182 |
166 |
183 (* aimed to solve the given subgoal totally, using whatever tools possible *) |
167 (* aimed to solve the given subgoal totally, using whatever tools possible *) |
184 fun force_tac (cs, ss) = |
168 fun force_tac ctxt = |
185 let val cs' = cs addss ss in |
169 let val ctxt' = addss ctxt in |
186 SELECT_GOAL |
170 SELECT_GOAL |
187 (Classical.clarify_tac cs' 1 THEN |
171 (Classical.clarify_tac ctxt' 1 THEN |
188 IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1) THEN |
172 IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN |
189 ALLGOALS (Classical.first_best_tac cs')) |
173 ALLGOALS (Classical.first_best_tac ctxt')) |
190 end; |
174 end; |
191 |
175 |
192 |
176 |
193 (* basic combinations *) |
177 (* basic combinations *) |
194 |
178 |
195 fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end; |
179 val fast_simp_tac = Classical.fast_tac o addss; |
196 |
180 val slow_simp_tac = Classical.slow_tac o addss; |
197 val fast_simp_tac = ADDSS Classical.fast_tac; |
181 val best_simp_tac = Classical.best_tac o addss; |
198 val slow_simp_tac = ADDSS Classical.slow_tac; |
|
199 val best_simp_tac = ADDSS Classical.best_tac; |
|
200 |
182 |
201 |
183 |
202 |
184 |
203 (** concrete syntax **) |
185 (** concrete syntax **) |
204 |
186 |
224 Classical.cla_modifiers @ iff_modifiers; |
206 Classical.cla_modifiers @ iff_modifiers; |
225 |
207 |
226 |
208 |
227 (* methods *) |
209 (* methods *) |
228 |
210 |
229 fun clasimp_meth tac ctxt = METHOD (fn facts => |
|
230 ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt)); |
|
231 |
|
232 fun clasimp_meth' tac ctxt = METHOD (fn facts => |
|
233 HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt))); |
|
234 |
|
235 |
|
236 fun clasimp_method' tac = |
211 fun clasimp_method' tac = |
237 Method.sections clasimp_modifiers >> K (clasimp_meth' tac); |
212 Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac); |
238 |
213 |
239 val auto_method = |
214 val auto_method = |
240 Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --| |
215 Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --| |
241 Method.sections clasimp_modifiers >> |
216 Method.sections clasimp_modifiers >> |
242 (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac) |
217 (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac |
243 | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n))); |
218 | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n)))); |
244 |
219 |
245 |
220 |
246 (* theory setup *) |
221 (* theory setup *) |
247 |
222 |
248 val clasimp_setup = |
223 val clasimp_setup = |