1.1 --- a/doc-src/Intro/advanced.tex Wed Mar 30 17:31:18 1994 +0200
1.2 +++ b/doc-src/Intro/advanced.tex Mon Apr 04 17:09:45 1994 +0200
1.3 @@ -36,15 +36,15 @@
1.4 \label{deriving-example}
1.5 \index{examples!of deriving rules}
1.6
1.7 -The subgoal module supports the derivation of rules. The \ttindex{goal}
1.8 -command, when supplied a goal of the form $\List{\theta@1; \ldots;
1.9 -\theta@k} \Imp \phi$, creates $\phi\Imp\phi$ as the initial proof state and
1.10 -returns a list consisting of the theorems
1.11 -${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions are
1.12 -also recorded internally, allowing \ttindex{result} to discharge them in the
1.13 -original order.
1.14 +The subgoal module supports the derivation of rules, as discussed in
1.15 +\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of the
1.16 +form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates $\phi\Imp\phi$
1.17 +as the initial proof state and returns a list consisting of the theorems
1.18 +${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. These meta-assumptions
1.19 +are also recorded internally, allowing \ttindex{result} to discharge them
1.20 +in the original order.
1.21
1.22 -Let us derive $\conj$ elimination~(\S\ref{deriving}) using Isabelle.
1.23 +Let us derive $\conj$ elimination using Isabelle.
1.24 Until now, calling \ttindex{goal} has returned an empty list, which we have
1.25 thrown away. In this example, the list contains the two premises of the
1.26 rule. We bind them to the \ML\ identifiers {\tt major} and {\tt
1.27 @@ -353,7 +353,7 @@
1.28 The {\ML} section contains code to perform arbitrary syntactic
1.29 transformations. The main declaration forms are discussed below.
1.30 The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
1.31 - appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}.
1.32 + appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.
1.33
1.34 All the declaration parts can be omitted. In the simplest case, $T$ is
1.35 just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one
1.36 @@ -518,28 +518,26 @@
1.37 translator passes them verbatim to the {\ML} output file.
1.38 \end{warn}
1.39
1.40 -\subsection{Type synonyms}
1.41 -\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}}
1.42 -
1.43 +\subsection{Type synonyms}\indexbold{types!synonyms}
1.44 Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
1.45 -to those found in ML. Such synonyms are defined in the type declaration part
1.46 +to those found in \ML. Such synonyms are defined in the type declaration part
1.47 and are fairly self explanatory:
1.48 \begin{ttbox}
1.49 -types gate = "[o,o] => o"
1.50 - 'a pred = "'a => o"
1.51 +types gate = "[o,o] => o"
1.52 + 'a pred = "'a => o"
1.53 ('a,'b)nuf = "'b => 'a"
1.54 \end{ttbox}
1.55 Type declarations and synonyms can be mixed arbitrarily:
1.56 \begin{ttbox}
1.57 types nat
1.58 'a stream = "nat => 'a"
1.59 - signal = "nat stream"
1.60 + signal = "nat stream"
1.61 'a list
1.62 \end{ttbox}
1.63 -A synonym is merely an abbreviation for some existing type expression. Hence
1.64 -synonyms may not be recursive! Internally all synonyms are fully expanded. As
1.65 -a consequence Isabelle output never contains synonyms. Their main purpose is
1.66 -to improve the readability of theories. Synonyms can be used just like any
1.67 +A synonym is merely an abbreviation for some existing type expression. Hence
1.68 +synonyms may not be recursive! Internally all synonyms are fully expanded. As
1.69 +a consequence Isabelle output never contains synonyms. Their main purpose is
1.70 +to improve the readability of theories. Synonyms can be used just like any
1.71 other type:
1.72 \begin{ttbox}
1.73 consts and,or :: "gate"
1.74 @@ -641,7 +639,7 @@
1.75 \(id\) < \(c@1\), \ldots, \(c@k\)
1.76 \end{ttbox}
1.77 Type classes allow constants to be overloaded. As suggested in
1.78 -\S\ref{polymorphic}, let us define the class $arith$ of ``arithmetic''
1.79 +\S\ref{polymorphic}, let us define the class $arith$ of arithmetic
1.80 types with the constants ${+} :: [\alpha,\alpha]\To \alpha$ and $0,1 {::}
1.81 \alpha$, for $\alpha{::}arith$. We introduce $arith$ as a subclass of
1.82 $term$ and add the three polymorphic constants of this class.
1.83 @@ -699,7 +697,7 @@
1.84 including a type~$nat$ and the constants $0::nat$ and $Suc::nat\To nat$.
1.85 Let us introduce the Peano axioms for mathematical induction and the
1.86 freeness of $0$ and~$Suc$:
1.87 -\[ \vcenter{\infer[(induct)*]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
1.88 +\[ \vcenter{\infer[(induct)]{P[n/x]}{P[0/x] & \infer*{P[Suc(x)/x]}{[P]}}}
1.89 \qquad \parbox{4.5cm}{provided $x$ is not free in any assumption except~$P$}
1.90 \]
1.91 \[ \infer[(Suc\_inject)]{m=n}{Suc(m)=Suc(n)} \qquad
1.92 @@ -752,7 +750,9 @@
1.93 \index{examples!of theories}
1.94 Let us create the theory \ttindexbold{Nat} starting from theory~\verb$FOL$,
1.95 which contains only classical logic with no natural numbers. We declare
1.96 -the 0-place type constructor $nat$ and the constants $rec$ and~$Suc$:
1.97 +the 0-place type constructor $nat$ and the associated constants. Note that
1.98 +the constant~0 requires a mixfix annotation because~0 is not a legal
1.99 +identifier, and could not otherwise be written in terms:
1.100 \begin{ttbox}
1.101 Nat = FOL +
1.102 types nat
1.103 @@ -835,7 +835,7 @@
1.104 \end{description}
1.105 The list {\it insts} consists of pairs $[(v@1,e@1), \ldots, (v@n,e@n)]$,
1.106 where $v@1$, \ldots, $v@n$ are names of schematic variables in the rule ---
1.107 -with no leading question marks!! --- and $e@1$, \ldots, $e@n$ are
1.108 +with no leading question marks! --- and $e@1$, \ldots, $e@n$ are
1.109 expressions giving their instantiations. The expressions are type-checked
1.110 in the context of a particular subgoal: free variables receive the same
1.111 types as they have in the subgoal, and parameters may appear. Type