--- a/doc-src/Intro/foundations.tex Mon May 05 12:15:53 1997 +0200
+++ b/doc-src/Intro/foundations.tex Mon May 05 13:24:11 1997 +0200
@@ -72,11 +72,13 @@
form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are
types. Curried function types may be abbreviated:
\[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad
- [\sigma@1, \ldots, \sigma@n] \To \tau \]
+[\sigma@1, \ldots, \sigma@n] \To \tau \]
-\index{terms!syntax of}
-The syntax for terms is summarised below. Note that function application is
-written $t(u)$ rather than the usual $t\,u$.
+\index{terms!syntax of} The syntax for terms is summarised below.
+Note that there are two versions of function application syntax
+available in Isabelle: either $t\,u$, which is the usual form for
+higher-order languages, or $t(u)$, trying to look more like
+first-order. The latter syntax is used throughout the manual.
\[
\index{lambda abs@$\lambda$-abstractions}\index{function applications}
\begin{array}{ll}
@@ -322,7 +324,9 @@
One of the simplest rules is $(\conj E1)$. Making
everything explicit, its formalization in the meta-logic is
-$$ \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) $$
+$$
+\Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1)
+$$
This may look formidable, but it has an obvious reading: for all object-level
truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The
reading is correct because the meta-logic has simple models, where
@@ -400,13 +404,13 @@
The $\forall E$ rule exploits $\beta$-conversion. Hiding $Trueprop$, the
$\forall$ axioms are
$$ \left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I) $$
-$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E)$$
+$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E) $$
\noindent
We have defined the object-level universal quantifier~($\forall$)
using~$\Forall$. But we do not require meta-level counterparts of all the
connectives of the object-logic! Consider the existential quantifier:
-$$ P(t) \Imp \exists x.P(x) \eqno(\exists I)$$
+$$ P(t) \Imp \exists x.P(x) \eqno(\exists I) $$
$$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$
Let us verify $(\exists E)$ semantically. Suppose that the premises
hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is
@@ -420,47 +424,48 @@
rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$
from~$P[t/x]$. When we formalize this as an axiom, the template becomes a
function variable:
-$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst)$$
+$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst) $$
\subsection{Signatures and theories}
\index{signatures|bold}
A {\bf signature} contains the information necessary for type checking,
-parsing and pretty printing a term. It specifies classes and their
+parsing and pretty printing a term. It specifies type classes and their
relationships, types and their arities, constants and their types, etc. It
-also contains syntax rules, specified using mixfix declarations.
+also contains grammar 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.
Under similar conditions, a signature can be extended. Signatures are
managed internally by Isabelle; users seldom encounter them.
-\index{theories|bold}
-A {\bf theory} consists of a signature plus a collection of axioms. The
-{\bf pure} theory contains only the meta-logic. Theories can be combined
-provided their signatures are compatible. A theory definition extends an
-existing theory with further signature specifications --- classes, types,
-constants and mixfix declarations --- plus a list of axioms, expressed as
-strings to be parsed. A theory can formalize a small piece of mathematics,
-such as lists and their operations, or an entire logic. A mathematical
-development typically involves many theories in a hierarchy. For example,
-the pure theory could be extended to form a theory for
-Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form a
-theory for natural numbers and a theory for lists; the union of these two
-could be extended into a theory defining the length of a list:
+\index{theories|bold} A {\bf theory} consists of a signature plus a
+collection of axioms. The {\Pure} theory contains only the
+meta-logic. Theories can be combined provided their signatures are
+compatible. A theory definition extends an existing theory with
+further signature specifications --- classes, types, constants and
+mixfix declarations --- plus lists of axioms and definitions etc.,
+expressed as strings to be parsed. A theory can formalize a small
+piece of mathematics, such as lists and their operations, or an entire
+logic. A mathematical development typically involves many theories in
+a hierarchy. For example, the {\Pure} theory could be extended to
+form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two
+separate ways to form a theory for natural numbers and a theory for
+lists; the union of these two could be extended into a theory defining
+the length of a list:
\begin{tt}
\[
\begin{array}{c@{}c@{}c@{}c@{}c}
- {} & {} & \hbox{Length} & {} & {} \\
- {} & {} & \uparrow & {} & {} \\
- {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\
- {} & \nearrow & {} & \nwarrow & {} \\
+ {} & {} &\hbox{Pure}& {} & {} \\
+ {} & {} & \downarrow & {} & {} \\
+ {} & {} &\hbox{FOL} & {} & {} \\
+ {} & \swarrow & {} & \searrow & {} \\
\hbox{Nat} & {} & {} & {} & \hbox{List} \\
- {} & \nwarrow & {} & \nearrow & {} \\
- {} & {} &\hbox{FOL} & {} & {} \\
- {} & {} & \uparrow & {} & {} \\
- {} & {} &\hbox{Pure}& {} & {}
+ {} & \searrow & {} & \swarrow & {} \\
+ {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\
+ {} & {} & \downarrow & {} & {} \\
+ {} & {} & \hbox{Length} & {} & {}
\end{array}
\]
\end{tt}%
@@ -472,7 +477,7 @@
\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.
+ constant and in another as a variable, for example.
\end{warn}
\section{Proof construction in Isabelle}
@@ -566,7 +571,7 @@
where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no
other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the
equation
-\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$
+\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). \]
\begin{warn}\index{unification!incompleteness of}%
Huet's unification procedure is complete. Isabelle's polymorphic version,
@@ -634,11 +639,11 @@
one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these
conclusions as a sequence (lazy list).
-Resolution expects the rules to have no outer quantifiers~($\Forall$). It
-may rename or instantiate any schematic variables, but leaves free
-variables unchanged. When constructing a theory, Isabelle puts the rules
-into a standard form containing no free variables; for instance, $({\imp}E)$
-becomes
+Resolution expects the rules to have no outer quantifiers~($\Forall$).
+It may rename or instantiate any schematic variables, but leaves free
+variables unchanged. When constructing a theory, Isabelle puts the
+rules into a standard form containing only schematic variables;
+for instance, $({\imp}E)$ becomes
\[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}.
\]
When resolving two rules, the unknowns in the first rule are renamed, by
@@ -770,7 +775,7 @@
forward from facts. It can also support backward proof, where we start
with a goal and refine it to progressively simpler subgoals until all have
been solved. {\sc lcf} and its descendants {\sc hol} and Nuprl provide
-tactics and tacticals, which constitute a high-level language for
+tactics and tacticals, which constitute a sophisticated language for
expressing proof searches. {\bf Tactics} refine subgoals while {\bf
tacticals} combine tactics.
@@ -1074,7 +1079,7 @@
Elim-resolution's simultaneous unification gives better control
than ordinary resolution. Recall the substitution rule:
$$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u})
- \eqno(subst) $$
+\eqno(subst) $$
Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many
unifiers, $(subst)$ works well with elim-resolution. It deletes some
assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal
@@ -1146,7 +1151,7 @@
meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no
assumptions. This represents the desired rule.
Let us derive the general $\conj$ elimination rule:
-$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E)$$
+$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E) $$
We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in
the state $R\Imp R$. Resolving this with the second assumption yields the
state