--- 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|)}