author lcp Fri, 22 Apr 1994 18:08:57 +0200 changeset 331 13660d5f6a77 parent 330 2fda15dd1e0f child 332 01b87a921967
final Springer copy
 doc-src/Intro/advanced.tex file | annotate | diff | comparison | revisions doc-src/Intro/foundations.tex file | annotate | diff | comparison | revisions doc-src/Intro/getting.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Intro/advanced.tex	Fri Apr 22 12:43:53 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Fri Apr 22 18:08:57 1994 +0200
@@ -9,9 +9,8 @@
the literature.  Set theory~({\tt ZF}) and Constructive Type Theory~({\tt
CTT}) form a richer world for mathematical reasoning and, again, many
examples are in the literature.  Higher-order logic~({\tt HOL}) is
-Isabelle's most sophisticated logic, because its types and functions are
-identified with those of the meta-logic; this may cause difficulties for
-beginners.
+Isabelle's most sophisticated logic because its types and functions are
+identified with those of the meta-logic.

Choose a logic that you already understand.  Isabelle is a proof
tool, not a teaching tool; if you do not know how to do a particular proof
@@ -113,10 +112,10 @@
\Var{P}\bimp \Var{Q}  & \equiv &
(\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P})
\end{eqnarray*}
-\index{meta-rewriting}
+\index{meta-rewriting}%
Isabelle permits {\bf meta-level rewriting} using definitions such as
these.  {\bf Unfolding} replaces every instance
-of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$.  For
+of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$.  For
example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to
$\forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot.$
{\bf Folding} a definition replaces occurrences of the right-hand side by
@@ -124,7 +123,7 @@

When you define new concepts, you should derive rules asserting their
abstract properties, and then forget their definitions.  This supports
-modularity: if you later change the definitions, without affecting their
+modularity: if you later change the definitions without affecting their
abstract properties, then most of your proofs will carry through without
change.  Indiscriminate unfolding makes a subgoal grow exponentially,
becoming unreadable.
@@ -336,7 +335,7 @@
$$T$$ = $$S@1$$ + $$\cdots$$ + $$S@n$$ +
classes      {\it class declarations}
default      {\it sort}
-types        {\it type declarations}
+types        {\it type declarations and synonyms}
arities      {\it arity declarations}
consts       {\it constant declarations}
rules        {\it rule declarations}
@@ -361,30 +360,30 @@
or more other theories, inheriting their types, constants, syntax, etc.
The theory \thydx{Pure} contains nothing but Isabelle's meta-logic.

-Each theory definition must reside in a separate file, whose name is
-determined as follows: the theory name, say {\tt ListFn}, is converted to
-lower case and {\tt.thy} is appended, yielding the filename {\tt
-  listfn.thy}.  Isabelle uses this convention to locate the file containing
-a given theory; \ttindexbold{use_thy} automatically loads a theory's
-parents before loading the theory itself.
+Each theory definition must reside in a separate file, whose name is the
+theory's with {\tt.thy} appended.  For example, theory {\tt ListFn} resides
+on a file named {\tt ListFn.thy}.  Isabelle uses this convention to locate the
+file containing a given theory; \ttindexbold{use_thy} automatically loads a
+theory's parents before loading the theory itself.

-Calling \ttindexbold{use_thy}~{\tt"}{\it T\/}{\tt"} reads a theory from the
-file {\it t}{\tt.thy}, writes the corresponding {\ML} code to the file
-{\tt.}{\it t}{\tt.thy.ML}, reads the latter file, and deletes it if no errors
-occured.  This declares the {\ML} structure~$T$, which contains a component
+Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the
+file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file
+{\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors
+occurred.  This declares the {\ML} structure~$T$, which contains a component
{\tt thy} denoting the new theory, a component for each rule, and everything
declared in {\it ML code}.

Errors may arise during the translation to {\ML} (say, a misspelled keyword)
or during creation of the new theory (say, a type error in a rule).  But if
-all goes well, {\tt use_thy} will finally read the file {\it t}{\tt.ML}, if
+all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if
it exists.  This file typically begins with the {\ML} declaration {\tt
open}~$T$ and contains proofs that refer to the components of~$T$.

When a theory file is modified, many theories may have to be reloaded.
Isabelle records the modification times and dependencies of theory files.
-See the {\em Reference Manual\/}
-\iflabelundefined{sec:reloading-theories}{}{(\S\ref{sec:reloading-theories})}
+See
+\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
+                 {\S\ref{sec:reloading-theories}}
for more details.

@@ -491,7 +490,7 @@

A type constructor may be overloaded (subject to certain conditions) by
appearing in several arity declarations.  For instance, the function type
-constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order
+constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order
logic, it is declared also to have arity $(term,term)term$.

Theory {\tt List} declares the 1-place type constructor $list$, gives
@@ -521,7 +520,7 @@
translator passes them verbatim to the {\ML} output file.
\end{warn}

-\subsection{Type synonyms}\indexbold{types!synonyms}
+\subsection{Type synonyms}\indexbold{type synonyms}
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
to those found in \ML.  Such synonyms are defined in the type declaration part
and are fairly self explanatory:
@@ -791,7 +790,7 @@
\end{ttbox}

\subsection{Proving some recursion equations}
-File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the
+File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
natural numbers.  As a trivial example, let us derive recursion equations
for \verb$+$.  Here is the zero case:
\begin{ttbox}
@@ -969,7 +968,7 @@
number is exponential in the size of the formula.

\subsection{Proving that addition is associative}
-Let us invoke the induction rule properly properly, using~{\tt
+Let us invoke the induction rule properly, using~{\tt
res_inst_tac}.  At the same time, we shall have a glimpse at Isabelle's
simplification tactics, which are described in
\iflabelundefined{simp-chap}%
@@ -981,7 +980,7 @@
perhaps proving it.  For efficiency, the rewrite rules must be
packaged into a {\bf simplification set},\index{simplification sets}
or {\bf simpset}.  We take the standard simpset for first-order logic and
-insert the equations for~{\tt add} proved in the previous section, namely
+insert the equations proved in the previous section, namely
$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
\begin{ttbox}
val add_ss = FOL_ss addrews [add_0, add_Suc];
@@ -1003,7 +1002,7 @@
\end{ttbox}
The base case holds easily; both sides reduce to $m+n$.  The
tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
-set, applying the rewrite rules for~{\tt +}:
+set, applying the rewrite rules for addition:
\begin{ttbox}
by (simp_tac add_ss 1);
{\out Level 2}
@@ -1011,7 +1010,7 @@
{\out  1. !!x. x + m + n = x + (m + n) ==>}
{\out          Suc(x) + m + n = Suc(x) + (m + n)}
\end{ttbox}
-The inductive step requires rewriting by the equations for~{\tt add}
+The inductive step requires rewriting by the equations for addition
together the induction hypothesis, which is also an equation.  The
tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
useful assumptions:
@@ -1028,7 +1027,7 @@
\index{Prolog interpreter|bold}
To demonstrate the power of tacticals, let us construct a Prolog
interpreter and execute programs involving lists.\footnote{To run these
-examples, see the file {\tt FOL/ex/prolog.ML}.} The Prolog program
+examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program
consists of a theory.  We declare a type constructor for lists, with an
arity declaration to say that $(\tau)list$ is of class~$term$
provided~$\tau$ is:
@@ -1199,7 +1198,7 @@
{\out  1. app(Nil, ?x1 : Nil, a : b : c : Nil)}
\end{ttbox}
The tactic has failed to find a solution!  It reached a dead end at
-subgoal~1: there is no~$\Var{x1}$ such that [] appended with~$[\Var{x1}]$
+subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$
equals~$[a,b,c]$.  Backtracking explores other outcomes.
\begin{ttbox}
back();
--- a/doc-src/Intro/foundations.tex	Fri Apr 22 12:43:53 1994 +0200
+++ b/doc-src/Intro/foundations.tex	Fri Apr 22 18:08:57 1994 +0200
@@ -50,21 +50,24 @@
\end{figure}

\section{Formalizing logical syntax in Isabelle}\label{sec:logical-syntax}
+\index{first-order logic}
+
Figure~\ref{fol-fig} presents intuitionistic first-order logic,
including equality.  Let us see how to formalize
this logic in Isabelle, illustrating the main features of Isabelle's
polymorphic meta-logic.

+\index{lambda calc@$\lambda$-calculus}
Isabelle represents syntax using the simply typed $\lambda$-calculus.  We
declare a type for each syntactic category of the logic.  We declare a
constant for each symbol of the logic, giving each $n$-place operation an
$n$-argument curried function type.  Most importantly,
$\lambda$-abstraction represents variable binding in quantifiers.
-\index{lambda calc@$\lambda$-calculus} \index{lambda
-  abs@$\lambda$-abstractions}

-\index{types!syntax of}\index{types!function}\index{*fun type}
-Isabelle has \ML-style type constructors such as~$(\alpha)list$, where
+\index{types!syntax of}\index{types!function}\index{*fun type}
+\index{type constructors}
+Isabelle has \ML-style polymorphic types such as~$(\alpha)list$, where
+$list$ is a type constructor and $\alpha$ is a type variable; for example,
$(bool)list$ is the type of lists of booleans.  Function types have the
form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are
types.  Curried function types may be abbreviated:
@@ -116,8 +119,9 @@
precedences, so that we write $P\conj Q\disj R$ instead of
$\disj(\conj(P,Q), R)$.

-\S\ref{sec:defining-theories} below describes the syntax of Isabelle theory
-files and illustrates it by extending our logic with mathematical induction.
+Section~\ref{sec:defining-theories} below describes the syntax of Isabelle
+theory files and illustrates it by extending our logic with mathematical
+induction.

\subsection{Polymorphic types and constants} \label{polymorphic}
@@ -164,7 +168,7 @@
We give~$o$ and function types the class $logic$ rather than~$term$, since
they are not legal types for terms.  We may introduce new types of class
$term$ --- for instance, type $string$ or $real$ --- at any time.  We can
-even declare type constructors such as $(\alpha)list$, and state that type
+even declare type constructors such as~$list$, and state that type
$(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality
applies to lists of natural numbers but not to lists of formulae.  We may
summarize this paragraph by a set of {\bf arity declarations} for type
@@ -176,7 +180,7 @@
list          & :: & (term)term
\end{eqnarray*}
(Recall that $fun$ is the type constructor for function types.)
-In higher-order logic, equality does apply to truth values and
+In \rmindex{higher-order logic}, equality does apply to truth values and
functions;  this requires the arity declarations ${o::term}$
and ${fun::(term,term)term}$.  The class system can also handle
overloading.\index{overloading|bold} We could declare $arith$ to be the
@@ -186,7 +190,7 @@
{+},{-},{\times},{/}  & :: & [\alpha{::}arith,\alpha]\To \alpha
\end{eqnarray*}
If we declare new types $real$ and $complex$ of class $arith$, then we
-effectively have three sets of operators:
+in effect have three sets of operators:
\begin{eqnarray*}
{+},{-},{\times},{/}  & :: & [nat,nat]\To nat \\
{+},{-},{\times},{/}  & :: & [real,real]\To real \\
@@ -216,7 +220,10 @@

Even with overloading, each term has a unique, most general type.  For this
to be possible, the class and type declarations must satisfy certain
-technical constraints~\cite{nipkow-prehofer}.
+technical constraints; see
+\iflabelundefined{sec:ref-defining-theories}%
+           {Sect.\ Defining Theories in the {\em Reference Manual}}%
+           {\S\ref{sec:ref-defining-theories}}.

\subsection{Higher types and quantifiers}
@@ -338,10 +345,10 @@
\noindent
Next, consider the disjunction rules.  The discharge of assumption in
$(\disj E)$ is expressed  using $\Imp$:
+\index{assumptions!discharge of}%
$$P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2)$$
$$\List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E)$$
-
-\noindent\index{assumptions!discharge of}
+%
To understand this treatment of assumptions in natural
deduction, look at implication.  The rule $({\imp}I)$ is the classic
example of natural deduction: to prove that $P\imp Q$ is true, assume $P$
@@ -421,9 +428,8 @@

A {\bf signature} contains the information necessary for type checking,
parsing and pretty printing a term.  It specifies classes and their
-relationships; types, with their arities, and constants, with
-their types.  It also contains syntax rules, specified using mixfix
-declarations.
+relationships, types and their arities, constants and their types, etc.  It
+also contains syntax rules, specified using mixfix declarations.

Two signatures can be merged provided their specifications are compatible ---
they must not, for example, assign different types to the same constant.
@@ -457,13 +463,13 @@
{}   &     {}   &\hbox{Pure}&     {}  &     {}
\end{array}
\]
-\end{tt}
+\end{tt}%
Each Isabelle proof typically works within a single theory, which is
associated with the proof state.  However, many different theories may
coexist at the same time, and you may work in each of these during a single
session.

-\begin{warn}\index{constants!clashes with variables}
+\begin{warn}\index{constants!clashes with variables}%
Confusing problems arise if you work in the wrong theory.  Each theory
defines its own syntax.  An identifier may be regarded in one theory as a
constant and in another as a variable.
@@ -481,7 +487,7 @@
properties must be demonstrated separately for each object-logic.

The meta-logic is defined by a collection of inference rules, including
-equational rules for the $\lambda$-calculus, and logical rules.  The rules
+equational rules for the $\lambda$-calculus and logical rules.  The rules
for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in
Fig.\ts\ref{fol-fig}.  Proofs performed using the primitive meta-rules
would be lengthy; Isabelle proofs normally use certain derived rules.
@@ -562,7 +568,7 @@
equation
$t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k).  -\begin{warn}\index{unification!incompleteness of} +\begin{warn}\index{unification!incompleteness of}% Huet's unification procedure is complete. Isabelle's polymorphic version, which solves for type unknowns as well as for term unknowns, is incomplete. The problem is that projection requires type information. In @@ -637,7 +643,7 @@$
When resolving two rules, the unknowns in the first rule are renamed, by
subscripting, to make them distinct from the unknowns in the second rule.  To
-resolve $({\imp}E)$ with itself, the first copy of the rule would become
+resolve $({\imp}E)$ with itself, the first copy of the rule becomes
$\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}.$
Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with
$\Var{P}\imp \Var{Q}$, is the meta-level inference
@@ -647,9 +653,8 @@
\List{\Var{P}\imp \Var{Q}; \Var{P}}  \Imp \Var{Q}}
\]
Renaming the unknowns in the resolvent, we have derived the
-object-level rule
+object-level rule\index{rules!derived}
$\infer{Q.}{R\imp (P\imp Q) & R & P}$
-\index{rules!derived}
Joining rules in this fashion is a simple way of proving theorems.  The
derived rules are conservative extensions of the object-logic, and may permit
simpler proofs.  Let us consider another example.  Suppose we have the axiom
@@ -797,9 +802,10 @@
To refine subgoal~$i$ of a proof state by a rule, perform the following
resolution:
$\infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}}$
-If the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after lifting
-over subgoal~$i$, and the proof state is $\List{\phi@1; \ldots; \phi@n} -\Imp \phi$, then the new proof state is (for~$1\leq i\leq n$)
+Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after
+lifting over subgoal~$i$'s assumptions and parameters.  If the proof state
+is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is
+(for~$1\leq i\leq n$)
$(\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1; \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.$
Substitution~$s$ unifies $\psi'$ with~$\phi@i$.  In the proof state,
@@ -974,9 +980,8 @@
tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$.

\item[REPEAT $tac$] is a repetition tactic.  Applied to a state, it
-returns all states reachable by applying~$tac$ as long as possible (until
-it would fail).  $REPEAT$ can be expressed in a few lines of \ML{} using
-{\tt THEN} and~{\tt ORELSE}.
+returns all states reachable by applying~$tac$ as long as possible --- until
+it would fail.
\end{ttdescription}
For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving
$tac1$ priority:
@@ -999,7 +1004,7 @@
\index{elim-resolution|bold}\index{assumptions!deleting}

Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$.  By
-$({\imp}I)$, we prove $R$ from the assumption $((R\disj R)\disj R)\disj R$.
+$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$.
Applying $(\disj E)$ to this assumption yields two subgoals, one that
assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj R)\disj R$.  This subgoal admits another application of $(\disj E)$.  Since
@@ -1008,9 +1013,8 @@
$\List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R.$
In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new
subgoals with the additional assumption $P$ or~$Q$.  In these subgoals,
-$P\disj Q$ is redundant.  It wastes space; worse, it could make a theorem
-prover repeatedly apply~$(\disj E)$, looping.  Other elimination rules pose
-similar problems.  In first-order logic, only universally quantified
+$P\disj Q$ is redundant.  Other elimination rules behave
+similarly.  In first-order logic, only universally quantified
assumptions are sometimes needed more than once --- say, to prove
$P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$.

@@ -1053,7 +1057,7 @@
$\List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}} \Imp \Var{R}$
and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$.  The
-lifted rule would be
+lifted rule is
$\begin{array}{l@{}l} \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\ & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\ @@ -1061,10 +1065,10 @@ \rbrakk\;& \Imp \Var{R@1} \end{array}$
-Unification would take the simultaneous equations
+Unification takes the simultaneous equations
$P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding
$\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state
-would be simply
+is simply
$\List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P).$
Elim-resolution's simultaneous unification gives better control
@@ -1110,14 +1114,13 @@
$\infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}}$
-\index{destruct-resolution}
-{\bf Destruct-resolution} combines this transformation with
-elim-resolution.  It applies a destruction rule to some assumption of a
-subgoal.  Given the rule above, it replaces the assumption~$P@1$ by~$Q$,
-with new subgoals of showing instances of $P@2$, \ldots,~$P@m$.
-Destruct-resolution works forward from a subgoal's assumptions.  Ordinary
-resolution performs forward reasoning from theorems, as illustrated
-in~\S\ref{joining}.
+{\bf Destruct-resolution}\index{destruct-resolution} combines this
+transformation with elim-resolution.  It applies a destruction rule to some
+assumption of a subgoal.  Given the rule above, it replaces the
+assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$,
+\ldots,~$P@m$.  Destruct-resolution works forward from a subgoal's
+assumptions.  Ordinary resolution performs forward reasoning from theorems,
+as illustrated in~\S\ref{joining}.

\subsection{Deriving rules by resolution}  \label{deriving}
@@ -1149,10 +1152,14 @@
state
$\phantom{\List{P\conj Q;\; P\conj Q}} \llap{\List{P;Q}}\Imp R \quad [\,\List{P;Q}\Imp R\,].$
-Resolving subgoals~1 and~2 with $({\conj}E1)$ and $({\conj}E2)$,
+Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$,
respectively, yields the state
-$\List{P\conj Q;\; P\conj Q}\Imp R \quad [\,\List{P;Q}\Imp R\,].$
-Resolving both subgoals with the assumption $P\conj Q$ yields
+$\List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R + \quad [\,\List{P;Q}\Imp R\,]. +$
+The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained
+subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$.  Resolving
+both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield
$R \quad [\, \List{P;Q}\Imp R, P\conj Q \,].$
The proof may use the meta-assumptions in any order, and as often as
necessary; when finished, we discharge them in the correct order to
@@ -1163,7 +1170,7 @@
schematic variables.

\begin{warn}
-Schematic variables are not allowed in meta-assumptions because they would
-complicate lifting.  Meta-assumptions remain fixed throughout a proof.
+  Schematic variables are not allowed in meta-assumptions, for a variety of
+  reasons.  Meta-assumptions remain fixed throughout a proof.
\end{warn}

--- a/doc-src/Intro/getting.tex	Fri Apr 22 12:43:53 1994 +0200
+++ b/doc-src/Intro/getting.tex	Fri Apr 22 18:08:57 1994 +0200
@@ -38,12 +38,15 @@
symbols.

Identifiers that are not reserved words may serve as free variables or
-constants.  A type identifier consists of an identifier prefixed by a
-prime, for example {\tt'a} and \hbox{\tt'hello}.  An unknown (or type
-unknown) consists of a question mark, an identifier (or type identifier),
-and a subscript.  The subscript, a non-negative integer, allows the
-renaming of unknowns prior to unification.%
-%
+constants.  A {\bf type identifier} consists of an identifier prefixed by a
+prime, for example {\tt'a} and \hbox{\tt'hello}.  Type identifiers stand
+for (free) type variables, which remain fixed during a proof.
+\index{type identifiers}
+
+An {\bf unknown}\index{unknowns} (or type unknown) consists of a question
+mark, an identifier (or type identifier), and a subscript.  The subscript,
+a non-negative integer,
+allows the renaming of unknowns prior to unification.%
\footnote{The subscript may appear after the identifier, separated by a
dot; this prevents ambiguity when the identifier ends with a digit.  Thus
{\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5}
@@ -62,7 +65,7 @@
contains the logical' types.  Sorts are lists of classes enclosed in
braces~\} and \{; singleton sorts may be abbreviated by dropping the braces.

-\index{types!syntax of|bold}
+\index{types!syntax of|bold}\index{sort constraints}
Types are written with a syntax like \ML's.  The built-in type \tydx{prop}
is the type of propositions.  Type variables can be constrained to particular
classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\{ord,arith\}}.
@@ -72,10 +75,10 @@
\index{*[ symbol}\index{*] symbol}
\begin{array}{lll}
\multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
-  t "::" C              & t :: C        & \hbox{class constraint} \\
-  t "::" "\{"   C@1 "," \ldots "," C@n "\}" &
-     t :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
-  \sigma"=>"\tau        & \sigma\To\tau & \hbox{function type} \\
+  \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
+  \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" &
+     \alpha :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
+  \sigma " => " \tau        & \sigma\To\tau & \hbox{function type} \\
"[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
[\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
"(" \tau@1"," \ldots "," \tau@n ")" tycon &
@@ -83,7 +86,7 @@
\end{array}
\]
Terms are those of the typed $\lambda$-calculus.
-\index{terms!syntax of|bold}
+\index{terms!syntax of|bold}\index{type constraints}
\[\dquotes
\index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
\index{*:: symbol}
@@ -180,11 +183,11 @@
\subsection{Basic operations on theorems}
\index{theorems!basic operations on|bold}
\index{LCF system}
-Meta-level theorems have type \mltydx{thm} and represent the theorems and
-inference rules of object-logics.  Isabelle's meta-logic is implemented
-using the {\sc lcf} approach: each meta-level inference rule is represented by
-a function from theorems to theorems.  Object-level rules are taken as
-axioms.
+Meta-level theorems have the \ML{} type \mltydx{thm}.  They represent the
+theorems and inference rules of object-logics.  Isabelle's meta-logic is
+implemented using the {\sc lcf} approach: each meta-level inference rule is
+represented by a function from theorems to theorems.  Object-level rules
+are taken as axioms.

The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt
prthq}.  Of the other operations on theorems, most useful are {\tt RS}
@@ -214,9 +217,14 @@
growth.
\end{ttdescription}
The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
-are running an Isabelle session containing natural deduction first-order
-logic.  Let us try an example given in~\S\ref{joining}.  We first print
-\tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with itself.
+are running an Isabelle session containing theory~\FOL, natural deduction
+first-order logic.\footnote{For a listing of the \FOL{} rules and their
+  \ML{} names, turn to
+\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
+           {page~\pageref{fol-rules}}.}
+Let us try an example given in~\S\ref{joining}.  We
+first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with
+itself.
\begin{ttbox}
prth mp;
{\out [| ?P --> ?Q; ?P |] ==> ?Q}
@@ -225,14 +233,14 @@
{\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q}
{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
\end{ttbox}
-User input appears in {\tt typewriter characters}, and output appears in
-{\sltt slanted typewriter characters}.  \ML's response {\out val }~\ldots{}
-is compiler-dependent and will sometimes be suppressed.  This session
-illustrates two formats for the display of theorems.  Isabelle's top-level
-displays theorems as ML values, enclosed in quotes.\footnote{This works
-  under both Poly/ML and Standard ML of New Jersey.}  Printing commands
-like {\tt prth} omit the quotes and the surrounding {\tt val \ldots :\
-  thm}.  Ignoring their side-effects, the commands are identity functions.
+User input appears in {\footnotesize\tt typewriter characters}, and output
+appears in {\sltt slanted typewriter characters}.  \ML's response {\out val
+  }~\ldots{} is compiler-dependent and will sometimes be suppressed.  This
+session illustrates two formats for the display of theorems.  Isabelle's
+top-level displays theorems as \ML{} values, enclosed in quotes.  Printing
+commands like {\tt prth} omit the quotes and the surrounding {\tt val
+  \ldots :\ thm}.  Ignoring their side-effects, the commands are identity
+functions.

To contrast {\tt RS} with {\tt RSN}, we resolve
\tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}.
@@ -568,11 +576,15 @@

\section{Quantifier reasoning}
-\index{quantifiers}\index{parameters}\index{unknowns}
+\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function}
This section illustrates how Isabelle enforces quantifier provisos.
-Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a
-function unknown and $x$ and~$z$ are parameters.  This may be replaced by
-any term, possibly containing free occurrences of $x$ and~$z$.
+Suppose that $x$, $y$ and~$z$ are parameters of a subgoal.  Quantifier
+rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
+unknown.  Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of
+replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free
+occurrences of~$x$ and~$z$.  On the other hand, no instantiation
+of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free
+occurrences of~$y$, since parameters are bound variables.

\subsection{Two quantifier proofs: a success and a failure}
\index{examples!with quantifiers}
@@ -721,7 +733,7 @@

\paragraph{The right approach.}
To do this proof, the rules must be applied in the correct order.
-Eigenvariables should be created before unknowns.  The
+Parameters should be created before unknowns.  The
\ttindex{choplev} command returns to an earlier stage of the proof;
let us return to the result of applying~$({\imp}I)$:
\begin{ttbox}
@@ -768,8 +780,8 @@
\index{tacticals} \index{examples!of tacticals}

Repeated application of rules can be effective, but the rules should be
-attempted in an order that delays the creation of unknowns.  Let us return
-to the original goal using \ttindex{choplev}:
+attempted in the correct order.  Let us return to the original goal using
+\ttindex{choplev}:
\begin{ttbox}
choplev 0;
{\out Level 0}
@@ -853,12 +865,13 @@
\index{classical reasoner}
Although Isabelle cannot compete with fully automatic theorem provers, it
provides enough automation to tackle substantial examples.  The classical
-reasoner can be set up for any classical natural deduction logic
---- see the {\em Reference Manual}.
+reasoner can be set up for any classical natural deduction logic;
+see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+        {Chap.\ts\ref{chap:classical}}.

-Rules are packaged into bundles called {\bf classical sets}.  The package
-provides several tactics, which apply rules using naive algorithms, using
-unification to handle quantifiers.  The most useful tactic
+Rules are packaged into {\bf classical sets}.  The classical reasoner
+provides several tactics, which apply rules using naive algorithms.
+Unification handles quantifiers as shown above.  The most useful tactic
is~\ttindex{fast_tac}.

Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}.  (The
@@ -900,8 +913,9 @@
{\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}
{\out No subgoals!}
\end{ttbox}
-The classical reasoner is not restricted to the usual logical
-connectives.  The natural deduction rules for unions and intersections in
-set theory resemble those for disjunction and conjunction, and in the
-infinitary case, for quantifiers.  The package is valuable for reasoning in
-set theory.
+The classical reasoner is not restricted to the usual logical connectives.
+The natural deduction rules for unions and intersections resemble those for
+disjunction and conjunction.  The rules for infinite unions and
+intersections resemble those for quantifiers.  Given such rules, the classical
+reasoner is effective for reasoning in set theory.
+  `