1.1 --- a/doc-src/Ref/classical.tex Wed May 03 15:25:30 1995 +0200
1.2 +++ b/doc-src/Ref/classical.tex Wed May 03 15:33:40 1995 +0200
1.3 @@ -205,24 +205,27 @@
1.4 is unsafe if it instantiates unknowns shared with other subgoals --- thus
1.5 \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}.
1.6
1.7 +\subsection{Adding rules to classical sets}
1.8 Classical rule sets belong to the abstract type \mltydx{claset}, which
1.9 supports the following operations (provided the classical reasoner is
1.10 installed!):
1.11 \begin{ttbox}
1.12 -empty_cs : claset
1.13 -addSIs : claset * thm list -> claset \hfill{\bf infix 4}
1.14 -addSEs : claset * thm list -> claset \hfill{\bf infix 4}
1.15 -addSDs : claset * thm list -> claset \hfill{\bf infix 4}
1.16 -addIs : claset * thm list -> claset \hfill{\bf infix 4}
1.17 -addEs : claset * thm list -> claset \hfill{\bf infix 4}
1.18 -addDs : claset * thm list -> claset \hfill{\bf infix 4}
1.19 -print_cs : claset -> unit
1.20 +empty_cs : claset
1.21 +print_cs : claset -> unit
1.22 +addSIs : claset * thm list -> claset \hfill{\bf infix 4}
1.23 +addSEs : claset * thm list -> claset \hfill{\bf infix 4}
1.24 +addSDs : claset * thm list -> claset \hfill{\bf infix 4}
1.25 +addIs : claset * thm list -> claset \hfill{\bf infix 4}
1.26 +addEs : claset * thm list -> claset \hfill{\bf infix 4}
1.27 +addDs : claset * thm list -> claset \hfill{\bf infix 4}
1.28 \end{ttbox}
1.29 There are no operations for deletion from a classical set. The add
1.30 operations do not check for repetitions.
1.31 \begin{ttdescription}
1.32 \item[\ttindexbold{empty_cs}] is the empty classical set.
1.33
1.34 +\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
1.35 +
1.36 \item[$cs$ addSIs $rules$] \indexbold{*addSIs}
1.37 adds safe introduction~$rules$ to~$cs$.
1.38
1.39 @@ -240,8 +243,6 @@
1.40
1.41 \item[$cs$ addDs $rules$] \indexbold{*addDs}
1.42 adds unsafe destruction~$rules$ to~$cs$.
1.43 -
1.44 -\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
1.45 \end{ttdescription}
1.46
1.47 Introduction rules are those that can be applied using ordinary resolution.
1.48 @@ -251,6 +252,8 @@
1.49 subgoals they will yield; rules that generate the fewest subgoals will be
1.50 tried first (see \S\ref{biresolve_tac}).
1.51
1.52 +
1.53 +\subsection{Modifying the search step}
1.54 For a given classical set, the proof strategy is simple. Perform as many
1.55 safe inferences as possible; or else, apply certain safe rules, allowing
1.56 instantiation of unknowns; or else, apply an unsafe rule. The tactics may
1.57 @@ -258,6 +261,47 @@
1.58 below). They may perform a form of Modus Ponens: if there are assumptions
1.59 $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$.
1.60
1.61 +The classical reasoner allows you to modify this basic proof strategy by
1.62 +applying an arbitrary {\bf wrapper tactical} to it. This affects each step of
1.63 +the search. Usually it is the identity tactical, but it could apply another
1.64 +tactic before or after the step tactic. It affects \ttindex{step_tac},
1.65 +\ttindex{slow_step_tac} and the tactics that call them.
1.66 +
1.67 +\begin{ttbox}
1.68 +addss : claset * simpset -> claset \hfill{\bf infix 4}
1.69 +addbefore : claset * tactic -> claset \hfill{\bf infix 4}
1.70 +addafter : claset * tactic -> claset \hfill{\bf infix 4}
1.71 +setwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4}
1.72 +compwrapper : claset * (tactic->tactic) -> claset \hfill{\bf infix 4}
1.73 +\end{ttbox}
1.74 +%
1.75 +\index{simplification!from classical reasoner}
1.76 +The wrapper tactical underlies the operator \ttindex{addss}, which precedes
1.77 +each search step by simplification. Strictly speaking, {\tt addss} is not
1.78 +part of the classical reasoner. It should be defined (using {\tt addbefore})
1.79 +when the simplifier is installed.
1.80 +
1.81 +\begin{ttdescription}
1.82 +\item[$cs$ addss $ss$] \indexbold{*addss}
1.83 +adds the simpset~$ss$ to the classical set. The assumptions and goal will be
1.84 +simplified before each step of the search.
1.85 +
1.86 +\item[$cs$ addbefore $tac$] \indexbold{*addbefore}
1.87 +changes the wrapper tactical to apply the given tactic {\em before}
1.88 +each step of the search.
1.89 +
1.90 +\item[$cs$ addafter $tac$] \indexbold{*addafter}
1.91 +changes the wrapper tactical to apply the given tactic {\em after}
1.92 +each step of the search.
1.93 +
1.94 +\item[$cs$ setwrapper $tactical$] \indexbold{*setwrapper}
1.95 +specifies a new wrapper tactical.
1.96 +
1.97 +\item[$cs$ compwrapper $tactical$] \indexbold{*compwrapper}
1.98 +composes the $tactical$ with the existing wrapper tactical, to combine their
1.99 +effects.
1.100 +\end{ttdescription}
1.101 +
1.102
1.103 \section{The classical tactics}
1.104 \index{classical reasoner!tactics}
1.105 @@ -301,7 +345,7 @@
1.106 \end{ttbox}
1.107 These work by exhaustive search up to a specified depth. Unsafe rules are
1.108 modified to preserve the formula they act on, so that it be used repeatedly.
1.109 -They can prove more goals than {\tt fast_tac}, etc., can. They are much
1.110 +They can prove more goals than {\tt fast_tac} can but are much
1.111 slower, for example if the assumptions have many universal quantifiers.
1.112
1.113 The depth limits the number of unsafe steps. If you can estimate the minimum
1.114 @@ -339,9 +383,9 @@
1.115 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
1.116 but allows unknowns to be instantiated.
1.117
1.118 -\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}. If this
1.119 -fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
1.120 -This is the basic step of the proof procedure.
1.121 +\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
1.122 + procedure. The wrapper tactical is applied to a tactic that tries {\tt
1.123 + safe_tac}, {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
1.124
1.125 \item[\ttindexbold{slow_step_tac}]
1.126 resembles {\tt step_tac}, but allows backtracking between using safe