203 instantiates an unknown in the proof state --- thus \ttindex{match_tac} |
203 instantiates an unknown in the proof state --- thus \ttindex{match_tac} |
204 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption |
204 must be used, rather than \ttindex{resolve_tac}. Even proof by assumption |
205 is unsafe if it instantiates unknowns shared with other subgoals --- thus |
205 is unsafe if it instantiates unknowns shared with other subgoals --- thus |
206 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. |
206 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. |
207 |
207 |
|
208 \subsection{Adding rules to classical sets} |
208 Classical rule sets belong to the abstract type \mltydx{claset}, which |
209 Classical rule sets belong to the abstract type \mltydx{claset}, which |
209 supports the following operations (provided the classical reasoner is |
210 supports the following operations (provided the classical reasoner is |
210 installed!): |
211 installed!): |
211 \begin{ttbox} |
212 \begin{ttbox} |
212 empty_cs : claset |
213 empty_cs : claset |
213 addSIs : claset * thm list -> claset \hfill{\bf infix 4} |
214 print_cs : claset -> unit |
214 addSEs : claset * thm list -> claset \hfill{\bf infix 4} |
215 addSIs : claset * thm list -> claset \hfill{\bf infix 4} |
215 addSDs : claset * thm list -> claset \hfill{\bf infix 4} |
216 addSEs : claset * thm list -> claset \hfill{\bf infix 4} |
216 addIs : claset * thm list -> claset \hfill{\bf infix 4} |
217 addSDs : claset * thm list -> claset \hfill{\bf infix 4} |
217 addEs : claset * thm list -> claset \hfill{\bf infix 4} |
218 addIs : claset * thm list -> claset \hfill{\bf infix 4} |
218 addDs : claset * thm list -> claset \hfill{\bf infix 4} |
219 addEs : claset * thm list -> claset \hfill{\bf infix 4} |
219 print_cs : claset -> unit |
220 addDs : claset * thm list -> claset \hfill{\bf infix 4} |
220 \end{ttbox} |
221 \end{ttbox} |
221 There are no operations for deletion from a classical set. The add |
222 There are no operations for deletion from a classical set. The add |
222 operations do not check for repetitions. |
223 operations do not check for repetitions. |
223 \begin{ttdescription} |
224 \begin{ttdescription} |
224 \item[\ttindexbold{empty_cs}] is the empty classical set. |
225 \item[\ttindexbold{empty_cs}] is the empty classical set. |
225 |
226 |
|
227 \item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. |
|
228 |
226 \item[$cs$ addSIs $rules$] \indexbold{*addSIs} |
229 \item[$cs$ addSIs $rules$] \indexbold{*addSIs} |
227 adds safe introduction~$rules$ to~$cs$. |
230 adds safe introduction~$rules$ to~$cs$. |
228 |
231 |
229 \item[$cs$ addSEs $rules$] \indexbold{*addSEs} |
232 \item[$cs$ addSEs $rules$] \indexbold{*addSEs} |
230 adds safe elimination~$rules$ to~$cs$. |
233 adds safe elimination~$rules$ to~$cs$. |
238 \item[$cs$ addEs $rules$] \indexbold{*addEs} |
241 \item[$cs$ addEs $rules$] \indexbold{*addEs} |
239 adds unsafe elimination~$rules$ to~$cs$. |
242 adds unsafe elimination~$rules$ to~$cs$. |
240 |
243 |
241 \item[$cs$ addDs $rules$] \indexbold{*addDs} |
244 \item[$cs$ addDs $rules$] \indexbold{*addDs} |
242 adds unsafe destruction~$rules$ to~$cs$. |
245 adds unsafe destruction~$rules$ to~$cs$. |
243 |
|
244 \item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. |
|
245 \end{ttdescription} |
246 \end{ttdescription} |
246 |
247 |
247 Introduction rules are those that can be applied using ordinary resolution. |
248 Introduction rules are those that can be applied using ordinary resolution. |
248 The classical set automatically generates their swapped forms, which will |
249 The classical set automatically generates their swapped forms, which will |
249 be applied using elim-resolution. Elimination rules are applied using |
250 be applied using elim-resolution. Elimination rules are applied using |
250 elim-resolution. In a classical set, rules are sorted by the number of new |
251 elim-resolution. In a classical set, rules are sorted by the number of new |
251 subgoals they will yield; rules that generate the fewest subgoals will be |
252 subgoals they will yield; rules that generate the fewest subgoals will be |
252 tried first (see \S\ref{biresolve_tac}). |
253 tried first (see \S\ref{biresolve_tac}). |
253 |
254 |
|
255 |
|
256 \subsection{Modifying the search step} |
254 For a given classical set, the proof strategy is simple. Perform as many |
257 For a given classical set, the proof strategy is simple. Perform as many |
255 safe inferences as possible; or else, apply certain safe rules, allowing |
258 safe inferences as possible; or else, apply certain safe rules, allowing |
256 instantiation of unknowns; or else, apply an unsafe rule. The tactics may |
259 instantiation of unknowns; or else, apply an unsafe rule. The tactics may |
257 also apply {\tt hyp_subst_tac}, if they have been set up to do so (see |
260 also apply {\tt hyp_subst_tac}, if they have been set up to do so (see |
258 below). They may perform a form of Modus Ponens: if there are assumptions |
261 below). They may perform a form of Modus Ponens: if there are assumptions |
259 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. |
262 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. |
260 |
263 |
|
264 The classical reasoner allows you to modify this basic proof strategy by |
|
265 applying an arbitrary {\bf wrapper tactical} to it. This affects each step of |
|
266 the search. Usually it is the identity tactical, but it could apply another |
|
267 tactic before or after the step tactic. It affects \ttindex{step_tac}, |
|
268 \ttindex{slow_step_tac} and the tactics that call them. |
|
269 |
|
270 \begin{ttbox} |
|
271 addss : claset * simpset -> claset \hfill{\bf infix 4} |
|
272 addbefore : claset * tactic -> claset \hfill{\bf infix 4} |
|
273 addafter : claset * tactic -> claset \hfill{\bf infix 4} |
|
274 setwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} |
|
275 compwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} |
|
276 \end{ttbox} |
|
277 % |
|
278 \index{simplification!from classical reasoner} |
|
279 The wrapper tactical underlies the operator \ttindex{addss}, which precedes |
|
280 each search step by simplification. Strictly speaking, {\tt addss} is not |
|
281 part of the classical reasoner. It should be defined (using {\tt addbefore}) |
|
282 when the simplifier is installed. |
|
283 |
|
284 \begin{ttdescription} |
|
285 \item[$cs$ addss $ss$] \indexbold{*addss} |
|
286 adds the simpset~$ss$ to the classical set. The assumptions and goal will be |
|
287 simplified before each step of the search. |
|
288 |
|
289 \item[$cs$ addbefore $tac$] \indexbold{*addbefore} |
|
290 changes the wrapper tactical to apply the given tactic {\em before} |
|
291 each step of the search. |
|
292 |
|
293 \item[$cs$ addafter $tac$] \indexbold{*addafter} |
|
294 changes the wrapper tactical to apply the given tactic {\em after} |
|
295 each step of the search. |
|
296 |
|
297 \item[$cs$ setwrapper $tactical$] \indexbold{*setwrapper} |
|
298 specifies a new wrapper tactical. |
|
299 |
|
300 \item[$cs$ compwrapper $tactical$] \indexbold{*compwrapper} |
|
301 composes the $tactical$ with the existing wrapper tactical, to combine their |
|
302 effects. |
|
303 \end{ttdescription} |
|
304 |
261 |
305 |
262 \section{The classical tactics} |
306 \section{The classical tactics} |
263 \index{classical reasoner!tactics} |
307 \index{classical reasoner!tactics} |
264 If installed, the classical module provides several tactics (and other |
308 If installed, the classical module provides several tactics (and other |
265 operations) for simulating the classical sequent calculus. |
309 operations) for simulating the classical sequent calculus. |
299 depth_tac : claset -> int -> int -> tactic |
343 depth_tac : claset -> int -> int -> tactic |
300 deepen_tac : claset -> int -> int -> tactic |
344 deepen_tac : claset -> int -> int -> tactic |
301 \end{ttbox} |
345 \end{ttbox} |
302 These work by exhaustive search up to a specified depth. Unsafe rules are |
346 These work by exhaustive search up to a specified depth. Unsafe rules are |
303 modified to preserve the formula they act on, so that it be used repeatedly. |
347 modified to preserve the formula they act on, so that it be used repeatedly. |
304 They can prove more goals than {\tt fast_tac}, etc., can. They are much |
348 They can prove more goals than {\tt fast_tac} can but are much |
305 slower, for example if the assumptions have many universal quantifiers. |
349 slower, for example if the assumptions have many universal quantifiers. |
306 |
350 |
307 The depth limits the number of unsafe steps. If you can estimate the minimum |
351 The depth limits the number of unsafe steps. If you can estimate the minimum |
308 number of unsafe steps needed, supply this value as~$m$ to save time. |
352 number of unsafe steps needed, supply this value as~$m$ to save time. |
309 \begin{ttdescription} |
353 \begin{ttdescription} |
337 can replicate certain quantifiers explicitly by applying appropriate rules. |
381 can replicate certain quantifiers explicitly by applying appropriate rules. |
338 |
382 |
339 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac}, |
383 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac}, |
340 but allows unknowns to be instantiated. |
384 but allows unknowns to be instantiated. |
341 |
385 |
342 \item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. If this |
386 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof |
343 fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. |
387 procedure. The wrapper tactical is applied to a tactic that tries {\tt |
344 This is the basic step of the proof procedure. |
388 safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. |
345 |
389 |
346 \item[\ttindexbold{slow_step_tac}] |
390 \item[\ttindexbold{slow_step_tac}] |
347 resembles {\tt step_tac}, but allows backtracking between using safe |
391 resembles {\tt step_tac}, but allows backtracking between using safe |
348 rules with instantiation ({\tt inst_step_tac}) and using unsafe rules. |
392 rules with instantiation ({\tt inst_step_tac}) and using unsafe rules. |
349 The resulting search space is larger. |
393 The resulting search space is larger. |