diff -r 994dbab40849 -r f4cecad9b6a0 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Mon Apr 04 17:09:45 1994 +0200
+++ b/doc-src/Ref/classical.tex	Mon Apr 04 17:20:15 1994 +0200
@@ -1,12 +1,13 @@
 %% $Id$
 \chapter{The Classical Reasoner}
 \index{classical reasoner|(}
-\newcommand\ainfer[2]{\begin{array}{r@{}l}#2\\ \hline#1\end{array}}
+\newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}}
+
 Although Isabelle is generic, many users will be working in some extension
-of classical first-order logic (FOL).  Isabelle's set theory is built upon
-FOL, while higher-order logic contains FOL as a fragment.  Theorem-proving
-in FOL is of course undecidable, but many researchers have developed
-strategies to assist in this task.
+of classical first-order logic.  Isabelle's set theory~{\tt ZF} is built
+upon theory~{\tt FOL}, while higher-order logic contains first-order logic
+as a fragment.  Theorem-proving in predicate logic is undecidable, but many
+researchers have developed strategies to assist in this task.
 
 Isabelle's classical reasoner is an \ML{} functor that accepts certain
 information about a logic and delivers a suite of automatic tactics.  Each
@@ -20,15 +21,16 @@
 \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x))
    \imp \neg (\exists z. \forall x. F(x,z))  
 \]
-The tactics are generic.  They are not restricted to~FOL, and have been
-heavily used in the development of Isabelle's set theory.  Few interactive
-proof assistants provide this much automation.  Isabelle does not record
-proofs, but the tactics can be traced, and their components can be called
-directly.  In this manner, any proof can be viewed interactively.
+%
+The tactics are generic.  They are not restricted to first-order logic, and
+have been heavily used in the development of Isabelle's set theory.  Few
+interactive proof assistants provide this much automation.  The tactics can
+be traced, and their components can be called directly; in this manner,
+any proof can be viewed interactively.
 
-The logics FOL, HOL and ZF have the classical reasoner already installed.  We
-shall first consider how to use it, then see how to instantiate it for new
-logics. 
+The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner
+already installed.  We shall first consider how to use it, then see how to
+instantiate it for new logics.
 
 
 \section{The sequent calculus}
@@ -40,8 +42,9 @@
 generalization of natural deduction, is easier to automate.
 
 A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$
-and~$\Delta$ are sets of formulae.\footnote{For FOL, sequents can
-equivalently be made from lists or multisets of formulae.}  The sequent
+and~$\Delta$ are sets of formulae.%
+\footnote{For first-order logic, sequents can equivalently be made from
+  lists or multisets of formulae.} The sequent
 \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \]
 is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj
 Q@n$.  Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true,
@@ -52,8 +55,12 @@
 Sequent rules are classified as {\bf right} or {\bf left}, indicating which
 side of the $\turn$~symbol they operate on.  Rules that operate on the
 right side are analogous to natural deduction's introduction rules, and
-left rules are analogous to elimination rules.  The sequent calculus
-analogue of~$({\imp}I)$ is the rule
+left rules are analogous to elimination rules.  
+Recall the natural deduction rules for
+  first-order logic, 
+\iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}%
+                          {Fig.\ts\ref{fol-fig}}.
+The sequent calculus analogue of~$({\imp}I)$ is the rule
 $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q}
    \eqno({\imp}R) $$
 This breaks down some implication on the right side of a sequent; $\Gamma$
@@ -82,7 +89,7 @@
 
 
 \section{Simulating sequents by natural deduction}
-Isabelle can represent sequents directly, as in the object-logic~{\sc lk}.
+Isabelle can represent sequents directly, as in the object-logic~{\tt LK}\@.
 But natural deduction is easier to work with, and most object-logics employ
 it.  Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn
 Q@1,\ldots,Q@n$ by the Isabelle formula
@@ -91,16 +98,17 @@
 Elim-resolution plays a key role in simulating sequent proofs.
 
 We can easily handle reasoning on the left.
-As discussed in the {\em Introduction to Isabelle},
+As discussed in
+\iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, 
 elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$
 achieves a similar effect as the corresponding sequent rules.  For the
 other connectives, we use sequent-style elimination rules instead of
-destruction rules.  But note that the rule $(\neg L)$ has no effect
-under our representation of sequents!
+destruction rules such as $({\conj}E1,2)$ and $(\forall E)$.  But note that
+the rule $(\neg L)$ has no effect under our representation of sequents!
 $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}
    \eqno({\neg}L) $$
 What about reasoning on the right?  Introduction rules can only affect the
-formula in the conclusion, namely~$Q@1$.  The other right-side formula are
+formula in the conclusion, namely~$Q@1$.  The other right-side formulae are
 represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$.  In
 order to operate on one of these, it must first be exchanged with~$Q@1$.
 Elim-resolution with the {\bf swap} rule has this effect:
@@ -129,8 +137,8 @@
 The destruction rule $({\imp}E)$ is replaced by
 \[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \]
 Quantifier replication also requires special rules.  In classical logic,
-$\exists x{.}P$ is equivalent to $\forall x{.}P$, and the rules $(\exists R)$
-and $(\forall L)$ are dual:
+$\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
+$(\exists R)$ and $(\forall L)$ are dual:
 \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P}
           {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R)
    \qquad
@@ -139,9 +147,9 @@
 \]
 Thus both kinds of quantifier may be replicated.  Theorems requiring
 multiple uses of a universal formula are easy to invent; consider 
-$(\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(x))$, for any~$n>1$.
-Natural examples of the multiple use of an existential formula are rare; a
-standard one is $\exists x.\forall y. P(x)\imp P(y)$.
+\[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \]
+for any~$n>1$.  Natural examples of the multiple use of an existential
+formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$.
 
 Forgoing quantifier replication loses completeness, but gains decidability,
 since the search space becomes finite.  Many useful theorems can be proved
@@ -169,22 +177,21 @@
 
 \section{Classical rule sets}
 \index{classical sets|bold}
-Each automatic tactic takes a {\bf classical rule set} -- a collection of
+Each automatic tactic takes a {\bf classical rule set} --- a collection of
 rules, classified as introduction or elimination and as {\bf safe} or {\bf
 unsafe}.  In general, safe rules can be attempted blindly, while unsafe
 rules must be used with care.  A safe rule must never reduce a provable
-goal to an unprovable set of subgoals.  The rule~$({\disj}I1)$ is obviously
-unsafe, since it reduces $P\disj Q$ to~$P$; fortunately, we do not require
-this rule.
+goal to an unprovable set of subgoals.  
 
-In general, any rule is unsafe whose premises contain new unknowns.  The
-elimination rule~$(\forall E@2)$ is unsafe, since it is applied via
-elim-resolution, which discards the assumption $\forall x{.}P(x)$ and
-replaces it by the weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$
-is unsafe for similar reasons.  The rule~$(\forall E@3)$ is unsafe in a
-different sense: since it keeps the assumption $\forall x{.}P(x)$, it is
-prone to looping.  In classical first-order logic, all rules are safe
-except those mentioned above.
+The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$.  Any
+rule is unsafe whose premises contain new unknowns.  The elimination
+rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution,
+which discards the assumption $\forall x{.}P(x)$ and replaces it by the
+weaker assumption~$P(\Var{t})$.  The rule $({\exists}I)$ is unsafe for
+similar reasons.  The rule~$(\forall E@3)$ is unsafe in a different sense:
+since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping.
+In classical first-order logic, all rules are safe except those mentioned
+above.
 
 The safe/unsafe distinction is vague, and may be regarded merely as a way
 of giving some rules priority over others.  One could argue that
@@ -211,29 +218,30 @@
 \end{ttbox}
 There are no operations for deletion from a classical set.  The add
 operations do not check for repetitions.
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{empty_cs}] is the empty classical set.
 
-\item[\tt $cs$ addSIs $rules$] \indexbold{*addSIs}
-adds some safe introduction~$rules$ to the classical set~$cs$.
+\item[$cs$ addSIs $rules$] \indexbold{*addSIs}
+adds safe introduction~$rules$ to~$cs$.
 
-\item[\tt $cs$ addSEs $rules$] \indexbold{*addSEs}
-adds some safe elimination~$rules$ to the classical set~$cs$.
+\item[$cs$ addSEs $rules$] \indexbold{*addSEs}
+adds safe elimination~$rules$ to~$cs$.
 
-\item[\tt $cs$ addSDs $rules$] \indexbold{*addSDs}
-adds some safe destruction~$rules$ to the classical set~$cs$.
+\item[$cs$ addSDs $rules$] \indexbold{*addSDs}
+adds safe destruction~$rules$ to~$cs$.
 
-\item[\tt $cs$ addIs $rules$] \indexbold{*addIs}
-adds some unsafe introduction~$rules$ to the classical set~$cs$.
+\item[$cs$ addIs $rules$] \indexbold{*addIs}
+adds unsafe introduction~$rules$ to~$cs$.
 
-\item[\tt $cs$ addEs $rules$] \indexbold{*addEs}
-adds some unsafe elimination~$rules$ to the classical set~$cs$.
+\item[$cs$ addEs $rules$] \indexbold{*addEs}
+adds unsafe elimination~$rules$ to~$cs$.
 
-\item[\tt $cs$ addDs $rules$] \indexbold{*addDs}
-adds some unsafe destruction~$rules$ to the classical set~$cs$.
+\item[$cs$ addDs $rules$] \indexbold{*addDs}
+adds unsafe destruction~$rules$ to~$cs$.
 
-\item[\ttindexbold{print_cs} $cs$] prints the rules of the classical set~$cs$.
-\end{description}
+\item[\ttindexbold{print_cs} $cs$] prints the rules of~$cs$.
+\end{ttdescription}
+
 Introduction rules are those that can be applied using ordinary resolution.
 The classical set automatically generates their swapped forms, which will
 be applied using elim-resolution.  Elimination rules are applied using
@@ -265,7 +273,7 @@
 \end{ttbox}
 The automatic proof procedures call these tactics.  By calling them
 yourself, you can execute these procedures one step at a time.
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
 subgoal~$i$.  This may include proof by assumption or Modus Ponens, taking
 care not to instantiate unknowns, or \ttindex{hyp_subst_tac}.
@@ -288,7 +296,7 @@
   The resulting search space is too large for use in the standard proof
   procedures, but {\tt slow_step_tac} is worth considering in special
   situations.
-\end{description}
+\end{ttdescription}
 
 
 \subsection{The automatic tactics}
@@ -299,7 +307,7 @@
 Both of these tactics work by applying {\tt step_tac} repeatedly.  Their
 effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
 solve this subgoal or fail.
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
 depth-first search, to solve subgoal~$i$.
 
@@ -307,7 +315,7 @@
 best-first search, to solve subgoal~$i$.  A heuristic function ---
 typically, the total size of the proof state --- guides the search.  This
 function is supplied when the classical reasoner is set up.
-\end{description}
+\end{ttdescription}
 
 
 \subsection{Other useful tactics}
@@ -320,7 +328,7 @@
 swap_res_tac : thm list -> int -> tactic
 \end{ttbox}
 These can be used in the body of a specialized search.
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{contr_tac} {\it i}] solves subgoal~$i$ by detecting a
 contradiction among two assumptions of the form $P$ and~$\neg P$, or fail.
 It may instantiate unknowns.  The tactic can produce multiple outcomes,
@@ -341,23 +349,23 @@
 rules.  First, it attempts to solve the goal using \ttindex{assume_tac} or
 {\tt contr_tac}.  It then attempts to apply each rule in turn, attempting
 resolution and also elim-resolution with the swapped form.
-\end{description}
+\end{ttdescription}
 
 \subsection{Creating swapped rules}
 \begin{ttbox} 
 swapify   : thm list -> thm list
 joinrules : thm list * thm list -> (bool * thm) list
 \end{ttbox}
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the
 swapped versions of~{\it thms}, regarded as introduction rules.
 
-\item[\ttindexbold{joinrules} \tt({\it intrs}, {\it elims})]
+\item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})]
 joins introduction rules, their swapped versions, and elimination rules for
 use with \ttindex{biresolve_tac}.  Each rule is paired with~{\tt false}
 (indicating ordinary resolution) or~{\tt true} (indicating
 elim-resolution).
-\end{description}
+\end{ttdescription}
 
 
 \section{Setting up the classical reasoner}
@@ -378,7 +386,7 @@
   end;
 \end{ttbox}
 Thus, the functor requires the following items:
-\begin{description}
+\begin{ttdescription}
 \item[\ttindexbold{mp}] should be the Modus Ponens rule
 $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
 
@@ -399,7 +407,7 @@
 the hypotheses, typically created by \ttindex{HypsubstFun} (see
 Chapter~\ref{substitution}).  This list can, of course, be empty.  The
 tactics are assumed to be safe!
-\end{description}
+\end{ttdescription}
 The functor is not at all sensitive to the formalization of the
 object-logic.  It does not even examine the rules, but merely applies them
 according to its fixed strategy.  The functor resides in {\tt