doc-src/Logics/HOL.tex
changeset 6119 7e3eb9b4df8e
parent 6076 560396301672
child 6141 a6922171b396
     1.1 --- a/doc-src/Logics/HOL.tex	Wed Jan 13 15:18:02 1999 +0100
     1.2 +++ b/doc-src/Logics/HOL.tex	Wed Jan 13 16:29:50 1999 +0100
     1.3 @@ -1871,15 +1871,19 @@
     1.4  itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t
     1.5    list)} is non-empty as well.
     1.6  
     1.7 +
     1.8 +\subsubsection{Freeness of the constructors}
     1.9 +
    1.10  The datatype constructors are automatically defined as functions of their
    1.11  respective type:
    1.12  \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]
    1.13 -These functions have certain {\em freeness} properties.  They are distinct:
    1.14 +These functions have certain {\em freeness} properties.  They construct
    1.15 +distinct values:
    1.16  \[
    1.17  C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad
    1.18  \mbox{for all}~ i \neq i'.
    1.19  \]
    1.20 -and they are injective:
    1.21 +The constructor functions are injective:
    1.22  \[
    1.23  (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =
    1.24  (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})
    1.25 @@ -1895,7 +1899,9 @@
    1.26  t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y.
    1.27  \]
    1.28  
    1.29 -\medskip The datatype package also provides structural induction rules.  For
    1.30 +\subsubsection{Structural induction}
    1.31 +
    1.32 +The datatype package also provides structural induction rules.  For
    1.33  datatypes without nested recursion, this is of the following form:
    1.34  \[
    1.35  \infer{P@1~x@1 \wedge \dots \wedge P@n~x@n}
    1.36 @@ -2183,7 +2189,7 @@
    1.37  {\out No subgoals!}
    1.38  \ttbreak
    1.39  qed_spec_mp "not_Cons_self";
    1.40 -{\out val not_Cons_self = "Cons x xs ~= xs";}
    1.41 +{\out val not_Cons_self = "Cons x xs ~= xs" : thm}
    1.42  \end{ttbox}
    1.43  Because both subgoals could have been proved by \texttt{Asm_simp_tac}
    1.44  we could have done that in one step:
    1.45 @@ -2266,9 +2272,8 @@
    1.46  
    1.47  Datatypes come with a uniform way of defining functions, {\bf primitive
    1.48    recursion}.  In principle, one could introduce primitive recursive functions
    1.49 -by asserting their reduction rules as new axioms.  Here is a counter-example
    1.50 -(you should not do such things yourself):
    1.51 -\begin{ttbox}
    1.52 +by asserting their reduction rules as new axioms, but this is not recommended:
    1.53 +\begin{ttbox}\slshape
    1.54  Append = Main +
    1.55  consts app :: ['a list, 'a list] => 'a list
    1.56  rules 
    1.57 @@ -2276,7 +2281,7 @@
    1.58     app_Cons  "app (x#xs) ys = x#app xs ys"
    1.59  end
    1.60  \end{ttbox}
    1.61 -But asserting axioms brings the danger of accidentally asserting nonsense, as
    1.62 +Asserting axioms brings the danger of accidentally asserting nonsense, as
    1.63  in \verb$app [] ys = us$.
    1.64  
    1.65  The \ttindex{primrec} declaration is a safe means of defining primitive
    1.66 @@ -2311,24 +2316,21 @@
    1.67  calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$.  There
    1.68  must be at most one reduction rule for each constructor.  The order is
    1.69  immaterial.  For missing constructors, the function is defined to return a
    1.70 -default value.  Also note that all reduction rules are added to the default
    1.71 -simpset.
    1.72 -  
    1.73 +default value.  
    1.74 +
    1.75  If you would like to refer to some rule by name, then you must prefix
    1.76  the rule with an identifier.  These identifiers, like those in the
    1.77  \texttt{rules} section of a theory, will be visible at the \ML\ level.
    1.78  
    1.79  The primitive recursive function can have infix or mixfix syntax:
    1.80  \begin{ttbox}\underscoreon
    1.81 -Append = List +
    1.82  consts "@"  :: ['a list, 'a list] => 'a list  (infixr 60)
    1.83  primrec
    1.84     "[] @ ys = ys"
    1.85     "(x#xs) @ ys = x#(xs @ ys)"
    1.86 -end
    1.87  \end{ttbox}
    1.88  
    1.89 -The reduction rules for {\tt\at} become part of the default simpset, which
    1.90 +The reduction rules become part of the default simpset, which
    1.91  leads to short proof scripts:
    1.92  \begin{ttbox}\underscoreon
    1.93  Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";