--- a/doc-src/Logics/HOL.tex Wed Jan 13 15:18:02 1999 +0100
+++ b/doc-src/Logics/HOL.tex Wed Jan 13 16:29:50 1999 +0100
@@ -1871,15 +1871,19 @@
itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
list)} is non-empty as well.
+
+\subsubsection{Freeness of the constructors}
+
The datatype constructors are automatically defined as functions of their
respective type:
\[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
-These functions have certain {\em freeness} properties. They are distinct:
+These functions have certain {\em freeness} properties. They construct
+distinct values:
\[
C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
\mbox{for all}~ i \neq i'.
\]
-and they are injective:
+The constructor functions are injective:
\[
(C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
(x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
@@ -1895,7 +1899,9 @@
t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y.
\]
-\medskip The datatype package also provides structural induction rules. For
+\subsubsection{Structural induction}
+
+The datatype package also provides structural induction rules. For
datatypes without nested recursion, this is of the following form:
\[
\infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
@@ -2183,7 +2189,7 @@
{\out No subgoals!}
\ttbreak
qed_spec_mp "not_Cons_self";
-{\out val not_Cons_self = "Cons x xs ~= xs";}
+{\out val not_Cons_self = "Cons x xs ~= xs" : thm}
\end{ttbox}
Because both subgoals could have been proved by \texttt{Asm_simp_tac}
we could have done that in one step:
@@ -2266,9 +2272,8 @@
Datatypes come with a uniform way of defining functions, {\bf primitive
recursion}. In principle, one could introduce primitive recursive functions
-by asserting their reduction rules as new axioms. Here is a counter-example
-(you should not do such things yourself):
-\begin{ttbox}
+by asserting their reduction rules as new axioms, but this is not recommended:
+\begin{ttbox}\slshape
Append = Main +
consts app :: ['a list, 'a list] => 'a list
rules
@@ -2276,7 +2281,7 @@
app_Cons "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
-But asserting axioms brings the danger of accidentally asserting nonsense, as
+Asserting axioms brings the danger of accidentally asserting nonsense, as
in \verb$app [] ys = us$.
The \ttindex{primrec} declaration is a safe means of defining primitive
@@ -2311,24 +2316,21 @@
calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
must be at most one reduction rule for each constructor. The order is
immaterial. For missing constructors, the function is defined to return a
-default value. Also note that all reduction rules are added to the default
-simpset.
-
+default value.
+
If you would like to refer to some rule by name, then you must prefix
the rule with an identifier. These identifiers, like those in the
\texttt{rules} section of a theory, will be visible at the \ML\ level.
The primitive recursive function can have infix or mixfix syntax:
\begin{ttbox}\underscoreon
-Append = List +
consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
primrec
"[] @ ys = ys"
"(x#xs) @ ys = x#(xs @ ys)"
-end
\end{ttbox}
-The reduction rules for {\tt\at} become part of the default simpset, which
+The reduction rules become part of the default simpset, which
leads to short proof scripts:
\begin{ttbox}\underscoreon
Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";