--- a/doc-src/Intro/advanced.tex Mon May 05 12:15:53 1997 +0200
+++ b/doc-src/Intro/advanced.tex Mon May 05 13:24:11 1997 +0200
@@ -3,14 +3,15 @@
Before continuing, it might be wise to try some of your own examples in
Isabelle, reinforcing your knowledge of the basic functions.
-Look through {\em Isabelle's Object-Logics\/} and try proving some simple
-theorems. You probably should begin with first-order logic ({\tt FOL}
-or~{\tt LK}). Try working some of the examples provided, and others from
-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.
+Look through {\em Isabelle's Object-Logics\/} and try proving some
+simple theorems. You probably should begin with first-order logic
+({\tt FOL} or~{\tt LK}). Try working some of the examples provided,
+and others from 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
+elaborate logic. 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
@@ -36,11 +37,12 @@
\index{examples!of deriving rules}\index{assumptions!of main goal}
The subgoal module supports the derivation of rules, as discussed in
-\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the
-form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
-as the initial proof state and returns a list consisting of the theorems
-${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions
-are also recorded internally, allowing {\tt result} to discharge them
+\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of
+the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates
+$\phi\Imp\phi$ as the initial proof state and returns a list
+consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$,
+\ldots,~$k$. These meta-assumptions are also recorded internally,
+allowing {\tt result} (which is called by {\tt qed}) to discharge them
in the original order.
Let us derive $\conj$ elimination using Isabelle.
@@ -91,13 +93,13 @@
{\out No subgoals!}
\end{ttbox}
Calling \ttindex{topthm} returns the current proof state as a theorem.
-Note that it contains assumptions. Calling \ttindex{result} discharges the
-assumptions --- both occurrences of $P\conj Q$ are discharged as one ---
-and makes the variables schematic.
+Note that it contains assumptions. Calling \ttindex{qed} discharges
+the assumptions --- both occurrences of $P\conj Q$ are discharged as
+one --- and makes the variables schematic.
\begin{ttbox}
topthm();
{\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm}
-val conjE = result();
+qed "conjE";
{\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm}
\end{ttbox}
@@ -139,8 +141,8 @@
\[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad
\infer[({\neg}E)]{Q}{\neg P & P} \]
This requires proving the following meta-formulae:
-$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I)$$
-$$ \List{\neg P; P} \Imp Q. \eqno(\neg E)$$
+$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$
+$$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$
\subsection{Deriving the $\neg$ introduction rule}
@@ -185,7 +187,7 @@
{\out ~P}
{\out No subgoals!}
\ttbreak
-val notI = result();
+qed "notI";
{\out val notI = "(?P ==> False) ==> ~?P" : thm}
\end{ttbox}
\indexbold{*notI theorem}
@@ -251,7 +253,7 @@
{\out Level 4}
{\out R}
{\out No subgoals!}
-val notE = result();
+qed "notE";
{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
\end{ttbox}
\indexbold{*notE theorem}
@@ -313,10 +315,10 @@
{\out !!P R. [| ~ P; P |] ==> R}
{\out No subgoals!}
\end{ttbox}
-Calling \ttindex{result} strips the meta-quantifiers, so the resulting
+Calling \ttindex{qed} strips the meta-quantifiers, so the resulting
theorem is the same as before.
\begin{ttbox}
-val notE = result();
+qed "notE";
{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm}
\end{ttbox}
Do not use the {\tt!!}\ trick if the premises contain meta-level
@@ -328,62 +330,67 @@
\section{Defining theories}\label{sec:defining-theories}
\index{theories!defining|(}
-Isabelle makes no distinction between simple extensions of a logic --- like
-defining a type~$bool$ with constants~$true$ and~$false$ --- and defining
-an entire logic. A theory definition has the form
+Isabelle makes no distinction between simple extensions of a logic ---
+like specifying a type~$bool$ with constants~$true$ and~$false$ ---
+and defining an entire logic. A theory definition has a form like
\begin{ttbox}
\(T\) = \(S@1\) + \(\cdots\) + \(S@n\) +
classes {\it class declarations}
default {\it sort}
types {\it type declarations and synonyms}
-arities {\it arity declarations}
+arities {\it type arity declarations}
consts {\it constant declarations}
-translations {\it translation declarations}
-defs {\it definitions}
+syntax {\it syntactic constant declarations}
+translations {\it ast translation rules}
+defs {\it meta-logical definitions}
rules {\it rule declarations}
end
ML {\it ML code}
\end{ttbox}
This declares the theory $T$ to extend the existing theories
-$S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities
-(overloadings of existing types), constants and rules; it can specify the
-default sort for type variables. A constant declaration can specify an
-associated concrete syntax. The translations section specifies rewrite
-rules on abstract syntax trees, for defining notations and abbreviations.
-\index{*ML section}
-The {\tt ML} section contains code to perform arbitrary syntactic
-transformations. The main declaration forms are discussed below.
-The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
- appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
+$S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities
+(of existing types), constants and rules; it can specify the default
+sort for type variables. A constant declaration can specify an
+associated concrete syntax. The translations section specifies
+rewrite rules on abstract syntax trees, handling notations and
+abbreviations. \index{*ML section} The {\tt ML} section may contain
+code to perform arbitrary syntactic transformations. The main
+declaration forms are discussed below. The full syntax can be found
+in \iflabelundefined{app:TheorySyntax}{an appendix of the {\it
+ Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that
+object-logics may add further theory sections, for example {\tt
+ typedef}, {\tt datatype} in \HOL.
-All the declaration parts can be omitted or repeated and may appear in any
-order, except that the {\ML} section must be last. In the simplest case, $T$
-is just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one or
-more other theories, inheriting their types, constants, syntax, etc. The
-theory \thydx{Pure} contains nothing but Isabelle's meta-logic.
+All the declaration parts can be omitted or repeated and may appear in
+any order, except that the {\ML} section must be last (after the {\tt
+ end} keyword). In the simplest case, $T$ is just the union of
+$S@1$,~\ldots,~$S@n$. New theories always extend one or more other
+theories, inheriting their types, constants, syntax, etc. The theory
+\thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
+\thydx{CPure} offers the more usual higher-order function application
+syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$.
-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.
+Each theory definition must reside in a separate file, whose name is
+the theory's with {\tt.thy} appended. Calling
+\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it
+ T}{\tt.thy}, writes a corresponding file of {\ML} code {\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}.
-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 it exists). This file typically contains proofs
+that refer to the components of~$T$. The structure is automatically
+opened, so its components may be referred to by unqualified names,
+e.g.\ just {\tt thy} instead of $T${\tt .thy}.
-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
-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
+\ttindexbold{use_thy} automatically loads a theory's parents before
+loading the theory itself. When a theory file is modified, many
+theories may have to be reloaded. Isabelle records the modification
+times and dependencies of theory files. See
\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}%
{\S\ref{sec:reloading-theories}}
for more details.
@@ -418,23 +425,23 @@
$rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be
enclosed in quotation marks.
-\indexbold{definitions} The {\bf definition part} is similar, but with the
-keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are rules of the
-form $s \equiv t$, and should serve only as abbreviations. The simplest form
-of a definition is $f \equiv t$, where $f$ is a constant. Isabelle also
-allows a derived form where the arguments of~$f$ appear on the left:
-\begin{itemize}
-\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots)
-\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF)
-\end{itemize}
-Isabelle checks for common errors in definitions, such as extra variables on
-the right-hand side. Determined users can write non-conservative
-`definitions' by using mutual recursion, for example; the consequences of
-such actions are their responsibility.
+\indexbold{definitions} The {\bf definition part} is similar, but with
+the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are
+rules of the form $s \equiv t$, and should serve only as
+abbreviations. The simplest form of a definition is $f \equiv t$,
+where $f$ is a constant. Also allowed are $\eta$-equivalent forms,
+where the arguments of~$f$ appear applied on the left-hand side of the
+equation instead of abstracted on the right-hand side.
-\index{examples!of theories}
-This theory extends first-order logic by declaring and defining two constants,
-{\em nand} and {\em xor}:
+Isabelle checks for common errors in definitions, such as extra
+variables on the right-hand side, but currently does not a complete
+test of well-formedness. Thus determined users can write
+non-conservative `definitions' by using mutual recursion, for example;
+the consequences of such actions are their responsibility.
+
+\index{examples!of theories} This example theory extends first-order
+logic by declaring and defining two constants, {\em nand} and {\em
+ xor}:
\begin{ttbox}
Gate = FOL +
consts nand,xor :: [o,o] => o
@@ -557,11 +564,11 @@
arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\)
\end{ttbox}
-\begin{warn}
-Arity declarations resemble constant declarations, but there are {\it no\/}
-quotation marks! Types and rules must be quoted because the theory
-translator passes them verbatim to the {\ML} output file.
-\end{warn}
+%\begin{warn}
+%Arity declarations resemble constant declarations, but there are {\it no\/}
+%quotation marks! Types and rules must be quoted because the theory
+%translator passes them verbatim to the {\ML} output file.
+%\end{warn}
\subsection{Type synonyms}\indexbold{type synonyms}
Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
@@ -579,11 +586,11 @@
signal = nat stream
'a list
\end{ttbox}
-A synonym is merely an abbreviation for some existing type expression. Hence
-synonyms may not be recursive! Internally all synonyms are fully expanded. As
-a consequence Isabelle output never contains synonyms. Their main purpose is
-to improve the readability of theories. Synonyms can be used just like any
-other type:
+A synonym is merely an abbreviation for some existing type expression.
+Hence synonyms may not be recursive! Internally all synonyms are
+fully expanded. As a consequence Isabelle output never contains
+synonyms. Their main purpose is to improve the readability of theory
+definitions. Synonyms can be used just like any other type:
\begin{ttbox}
consts and,or :: gate
negate :: signal => signal
@@ -623,10 +630,10 @@
if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
denote argument positions.
-The declaration above does not allow the {\tt if}-{\tt then}-{\tt else}
-construct to be split across several lines, even if it is too long to fit
-on one line. Pretty-printing information can be added to specify the
-layout of mixfix operators. For details, see
+The declaration above does not allow the {\tt if}-{\tt then}-{\tt
+ else} construct to be printed split across several lines, even if it
+is too long to fit on one line. Pretty-printing information can be
+added to specify the layout of mixfix operators. For details, see
\iflabelundefined{Defining-Logics}%
{the {\it Reference Manual}, chapter `Defining Logics'}%
{Chap.\ts\ref{Defining-Logics}}.
@@ -672,9 +679,11 @@
\end{ttbox}
\begin{warn}
-The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would
-be in the case of an infix constant. Only infix type constructors can have
-symbolic names like~{\tt *}. There is no general mixfix syntax for types.
+ The name of the type constructor is~{\tt *} and not {\tt op~*}, as
+ it would be in the case of an infix constant. Only infix type
+ constructors can have symbolic names like~{\tt *}. General mixfix
+ syntax for types may be introduced via appropriate {\tt syntax}
+ declarations.
\end{warn}
@@ -826,11 +835,7 @@
\end{ttbox}
In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$.
Loading this theory file creates the \ML\ structure {\tt Nat}, which
-contains the theory and axioms. Opening structure {\tt Nat} lets us write
-{\tt induct} instead of {\tt Nat.induct}, and so forth.
-\begin{ttbox}
-open Nat;
-\end{ttbox}
+contains the theory and axioms.
\subsection{Proving some recursion equations}
File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the
@@ -846,7 +851,7 @@
{\out Level 1}
{\out 0 + n = n}
{\out No subgoals!}
-val add_0 = result();
+qed "add_0";
\end{ttbox}
And here is the successor case:
\begin{ttbox}
@@ -859,7 +864,7 @@
{\out Level 1}
{\out Suc(m) + n = Suc(m + n)}
{\out No subgoals!}
-val add_Suc = result();
+qed "add_Suc";
\end{ttbox}
The induction rule raises some complications, which are discussed next.
\index{theories!defining|)}
--- 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
--- a/doc-src/Intro/getting.tex Mon May 05 12:15:53 1997 +0200
+++ b/doc-src/Intro/getting.tex Mon May 05 13:24:11 1997 +0200
@@ -1,19 +1,25 @@
%% $Id$
\part{Getting Started with Isabelle}\label{chap:getting}
-Let us consider how to perform simple proofs using Isabelle. At present,
-Isabelle's user interface is \ML. Proofs are conducted by applying certain
-\ML{} functions, which update a stored proof state. All syntax must be
-expressed using {\sc ascii} characters. Menu-driven graphical interfaces
-are under construction, but Isabelle users will always need to know some
-\ML, at least to use tacticals.
+Let us consider how to perform simple proofs using Isabelle. At
+present, Isabelle's user interface is \ML. Proofs are conducted by
+applying certain \ML{} functions, which update a stored proof state.
+Basically, all syntax must be expressed using plain {\sc ascii}
+characters. There are also mechanisms built into Isabelle that support
+alternative syntaxes, for example using mathematical symbols from a
+special screen font. The meta-logic and major object-logics already
+provide such fancy output as an option.
-Object-logics are built upon Pure Isabelle, which implements the meta-logic
-and provides certain fundamental data structures: types, terms, signatures,
-theorems and theories, tactics and tacticals. These data structures have
-the corresponding \ML{} types {\tt typ}, {\tt term}, {\tt Sign.sg}, {\tt thm},
-{\tt theory} and {\tt tactic}; tacticals have function types such as {\tt
-tactic->tactic}. Isabelle users can operate on these data structures by
-writing \ML{} programs.
+%FIXME remove
+%Menu-driven graphical interfaces are under construction, but Isabelle
+%users will always need to know some \ML, at least to use tacticals.
+
+Object-logics are built upon Pure Isabelle, which implements the
+meta-logic and provides certain fundamental data structures: types,
+terms, signatures, theorems and theories, tactics and tacticals.
+These data structures have the corresponding \ML{} types {\tt typ},
+{\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic};
+tacticals have function types such as {\tt tactic->tactic}. Isabelle
+users can operate on these data structures by writing \ML{} programs.
\section{Forward proof}\label{sec:forward} \index{forward proof|(}
This section describes the concrete syntax for types, terms and theorems,
@@ -65,10 +71,11 @@
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{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\}}.
+\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::\ttlbrace
+ ord, arith\ttrbrace}.
\[\dquotes
\index{*:: symbol}\index{*=> symbol}
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
@@ -76,7 +83,7 @@
\begin{array}{lll}
\multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
\alpha "::" C & \alpha :: C & \hbox{class constraint} \\
- \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" &
+ \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
\alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\
\sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\
"[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
@@ -118,7 +125,7 @@
\List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\
"!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\
"!!" x@1\ldots x@n "." \phi &
- \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification}
+ \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification}
\end{array}
\]
Flex-flex constraints are meta-equalities arising from unification; they
@@ -138,8 +145,8 @@
PROP ?psi ==> PROP ?theta
\end{ttbox}
-Symbols of object-logics also must be rendered into {\sc ascii}, typically
-as follows:
+Symbols of object-logics are typically rendered into {\sc ascii} as
+follows:
\[ \begin{tabular}{l@{\quad}l@{\quad}l}
\tt True & $\top$ & true \\
\tt False & $\bot$ & false \\
@@ -154,9 +161,8 @@
\]
To illustrate the notation, consider two axioms for first-order logic:
$$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$
-$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
-Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates into
-{\sc ascii} characters as
+$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$
+$({\conj}I)$ translates into {\sc ascii} characters as
\begin{ttbox}
[| ?P; ?Q |] ==> ?P & ?Q
\end{ttbox}
@@ -406,14 +412,19 @@
applies the {\it tactic\/} to the current proof
state, raising an exception if the tactic fails.
-\item[\ttindex{undo}(); ]
+\item[\ttindex{undo}(); ]
reverts to the previous proof state. Undo can be repeated but cannot be
undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely
causes \ML\ to echo the value of that function.
-\item[\ttindex{result}()]
+\item[\ttindex{result}();]
returns the theorem just proved, in a standard format. It fails if
unproved subgoals are left, etc.
+
+\item[\ttindex{qed} {\it name};] is the usual way of ending a proof.
+ It gets the theorem using {\tt result}, stores it in Isabelle's
+ theorem database and binds it to an \ML{} identifier.
+
\end{ttdescription}
The commands and tactics given above are cumbersome for interactive use.
Although our examples will use the full commands, you may prefer Isabelle's
@@ -494,9 +505,9 @@
{\out No subgoals!}
\end{ttbox}
Isabelle tells us that there are no longer any subgoals: the proof is
-complete. Calling {\tt result} returns the theorem.
+complete. Calling {\tt qed} stores the theorem.
\begin{ttbox}
-val mythm = result();
+qed "mythm";
{\out val mythm = "?P | ?P --> ?P" : thm}
\end{ttbox}
Isabelle has replaced the free variable~{\tt P} by the scheme
@@ -664,7 +675,7 @@
The reflexivity axiom does not unify with subgoal~1.
\begin{ttbox}
by (resolve_tac [refl] 1);
-{\out by: tactic returned no results}
+{\out by: tactic failed}
\end{ttbox}
There can be no proof of $\exists y.\forall x.x=y$ by the soundness of
first-order logic. I have elsewhere proved the faithfulness of Isabelle's
@@ -727,7 +738,7 @@
proof by assumption will fail.
\begin{ttbox}
by (assume_tac 1);
-{\out by: tactic returned no results}
+{\out by: tactic failed}
{\out uncaught exception ERROR}
\end{ttbox}