doc-src/Intro/foundations.tex
 changeset 3103 98af809fee46 parent 1878 ac8e534b4834 child 3106 5396e99c02af
--- 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