author lcp Mon, 04 Apr 1994 17:09:45 +0200 changeset 307 994dbab40849 parent 306 eee166d4a532 child 308 f4cecad9b6a0
modifications towards final draft
--- a/doc-src/Intro/advanced.tex	Wed Mar 30 17:31:18 1994 +0200
+++ b/doc-src/Intro/advanced.tex	Mon Apr 04 17:09:45 1994 +0200
@@ -36,15 +36,15 @@
\label{deriving-example}
\index{examples!of deriving rules}

-The subgoal module supports the derivation of rules.  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 \ttindex{result} to discharge them in the
-original order.
+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 \ttindex{result} to discharge them
+in the original order.

-Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle.
+Let us derive $\conj$ elimination using Isabelle.
Until now, calling \ttindex{goal} has returned an empty list, which we have
thrown away.  In this example, the list contains the two premises of the
rule.  We bind them to the \ML\ identifiers {\tt major} and {\tt
@@ -353,7 +353,7 @@
The {\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}}{Appendix~\ref{app:TheorySyntax}}.
+  appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.

All the declaration parts can be omitted.  In the simplest case, $T$ is
just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
@@ -518,28 +518,26 @@
translator passes them verbatim to the {\ML} output file.
\end{warn}

-\subsection{Type synonyms}
-\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}}
-
+\subsection{Type synonyms}\indexbold{types!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
+to those found in \ML.  Such synonyms are defined in the type declaration part
and are fairly self explanatory:
\begin{ttbox}
-types gate = "[o,o] => o"
-      'a pred = "'a => o"
+types gate       = "[o,o] => o"
+      'a pred    = "'a => o"
('a,'b)nuf = "'b => 'a"
\end{ttbox}
Type declarations and synonyms can be mixed arbitrarily:
\begin{ttbox}
types nat
'a stream = "nat => 'a"
-      signal = "nat stream"
+      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
+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:
\begin{ttbox}
consts and,or :: "gate"
@@ -641,7 +639,7 @@
$$id$$ < $$c@1$$, \ldots, $$c@k$$
\end{ttbox}
Type classes allow constants to be overloaded.  As suggested in
-\S\ref{polymorphic}, let us define the class $arith$ of arithmetic''
+\S\ref{polymorphic}, let us define the class $arith$ of arithmetic
types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::} \alpha$, for $\alpha{::}arith$.  We introduce $arith$ as a subclass of
$term$ and add the three polymorphic constants of this class.
@@ -699,7 +697,7 @@
including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
Let us introduce the Peano axioms for mathematical induction and the
freeness of $0$ and~$Suc$:
-$\vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} +\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}} \qquad \parbox{4.5cm}{provided x is not free in any assumption except~P}$
@@ -752,7 +750,9 @@
\index{examples!of theories}
Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
which contains only classical logic with no natural numbers.  We declare
-the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:
+the 0-place type constructor $nat$ and the associated constants.  Note that
+the constant~0 requires a mixfix annotation because~0 is not a legal
+identifier, and could not otherwise be written in terms:
\begin{ttbox}
Nat = FOL +
types   nat
@@ -835,7 +835,7 @@
\end{description}
The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
-with no leading question marks!! --- and $e@1$, \ldots, $e@n$ are
+with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
expressions giving their instantiations.  The expressions are type-checked
in the context of a particular subgoal: free variables receive the same
types as they have in the subgoal, and parameters may appear.  Type