# HG changeset patch # User lcp # Date 799508020 -7200 # Node ID f4335b56f7723ab32865ba7cf41fd7a8faebd570 # Parent 487089cb173edb8edd52d99c93349290474507eb Covers wrapper tacticals: setwrapper, ..., addss diff -r 487089cb173e -r f4335b56f772 doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Wed May 03 15:25:30 1995 +0200 +++ b/doc-src/Ref/classical.tex Wed May 03 15:33:40 1995 +0200 @@ -205,24 +205,27 @@ is unsafe if it instantiates unknowns shared with other subgoals --- thus \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. +\subsection{Adding rules to classical sets} Classical rule sets belong to the abstract type \mltydx{claset}, which supports the following operations (provided the classical reasoner is installed!): \begin{ttbox} -empty_cs : claset -addSIs : claset * thm list -> claset \hfill{\bf infix 4} -addSEs : claset * thm list -> claset \hfill{\bf infix 4} -addSDs : claset * thm list -> claset \hfill{\bf infix 4} -addIs : claset * thm list -> claset \hfill{\bf infix 4} -addEs : claset * thm list -> claset \hfill{\bf infix 4} -addDs : claset * thm list -> claset \hfill{\bf infix 4} -print_cs : claset -> unit +empty_cs : claset +print_cs : claset -> unit +addSIs : claset * thm list -> claset \hfill{\bf infix 4} +addSEs : claset * thm list -> claset \hfill{\bf infix 4} +addSDs : claset * thm list -> claset \hfill{\bf infix 4} +addIs : claset * thm list -> claset \hfill{\bf infix 4} +addEs : claset * thm list -> claset \hfill{\bf infix 4} +addDs : claset * thm list -> claset \hfill{\bf infix 4} \end{ttbox} There are no operations for deletion from a classical set. The add operations do not check for repetitions. \begin{ttdescription} \item[\ttindexbold{empty_cs}] is the empty classical set. +\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. + \item[$cs$ addSIs $rules$] \indexbold{*addSIs} adds safe introduction~$rules$ to~$cs$. @@ -240,8 +243,6 @@ \item[$cs$ addDs $rules$] \indexbold{*addDs} adds unsafe destruction~$rules$ to~$cs$. - -\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$. \end{ttdescription} Introduction rules are those that can be applied using ordinary resolution. @@ -251,6 +252,8 @@ subgoals they will yield; rules that generate the fewest subgoals will be tried first (see \S\ref{biresolve_tac}). + +\subsection{Modifying the search step} For a given classical set, the proof strategy is simple. Perform as many safe inferences as possible; or else, apply certain safe rules, allowing instantiation of unknowns; or else, apply an unsafe rule. The tactics may @@ -258,6 +261,47 @@ below). They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. +The classical reasoner allows you to modify this basic proof strategy by +applying an arbitrary {\bf wrapper tactical} to it. This affects each step of +the search. Usually it is the identity tactical, but it could apply another +tactic before or after the step tactic. It affects \ttindex{step_tac}, +\ttindex{slow_step_tac} and the tactics that call them. + +\begin{ttbox} +addss : claset * simpset -> claset \hfill{\bf infix 4} +addbefore : claset * tactic -> claset \hfill{\bf infix 4} +addafter : claset * tactic -> claset \hfill{\bf infix 4} +setwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} +compwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4} +\end{ttbox} +% +\index{simplification!from classical reasoner} +The wrapper tactical underlies the operator \ttindex{addss}, which precedes +each search step by simplification. Strictly speaking, {\tt addss} is not +part of the classical reasoner. It should be defined (using {\tt addbefore}) +when the simplifier is installed. + +\begin{ttdescription} +\item[$cs$ addss $ss$] \indexbold{*addss} +adds the simpset~$ss$ to the classical set. The assumptions and goal will be +simplified before each step of the search. + +\item[$cs$ addbefore $tac$] \indexbold{*addbefore} +changes the wrapper tactical to apply the given tactic {\em before} +each step of the search. + +\item[$cs$ addafter $tac$] \indexbold{*addafter} +changes the wrapper tactical to apply the given tactic {\em after} +each step of the search. + +\item[$cs$ setwrapper $tactical$] \indexbold{*setwrapper} +specifies a new wrapper tactical. + +\item[$cs$ compwrapper $tactical$] \indexbold{*compwrapper} +composes the $tactical$ with the existing wrapper tactical, to combine their +effects. +\end{ttdescription} + \section{The classical tactics} \index{classical reasoner!tactics} @@ -301,7 +345,7 @@ \end{ttbox} These work by exhaustive search up to a specified depth. Unsafe rules are modified to preserve the formula they act on, so that it be used repeatedly. -They can prove more goals than {\tt fast_tac}, etc., can. They are much +They can prove more goals than {\tt fast_tac} can but are much slower, for example if the assumptions have many universal quantifiers. The depth limits the number of unsafe steps. If you can estimate the minimum @@ -339,9 +383,9 @@ \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac}, but allows unknowns to be instantiated. -\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. If this -fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. -This is the basic step of the proof procedure. +\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof + procedure. The wrapper tactical is applied to a tactic that tries {\tt + safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$. \item[\ttindexbold{slow_step_tac}] resembles {\tt step_tac}, but allows backtracking between using safe