doc-src/Logics/HOL.tex

   case}, to ensure that the new types are non-empty. If there are nested
 occurrences, a datatype can even be non-empty without having a base case
 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})
 \]
 Because the number of distinctness inequalities is quadratic in the number of

 Then distinctness of constructor terms is expressed by:
 \[
 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}
   {\begin{array}{lcl}
      \Forall x@1 \dots x@{m^1@1}.

 {\out Level 3}
 {\out ! x. Cons x xs ~= xs}
 {\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:
 \begin{ttbox}
 by (ALLGOALS Asm_simp_tac);

 \index{recursion!primitive|(}
 \index{*primrec|(}
 
 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 
    app_Nil   "app [] ys = ys"
    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
 recursive functions on datatypes:
 \begin{ttbox}

 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
 contains only the free variables on the left-hand side, and all recursive
 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
+\end{ttbox}
+
+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)";
 by (induct\_tac "xs" 1);
 by (ALLGOALS Asm\_simp\_tac);