summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 13 Jan 1999 16:29:50 +0100 | |

changeset 6119 | 7e3eb9b4df8e |

parent 6118 | caa439435666 |

child 6120 | f40d61cd6b32 |

minor updates on inductive definitions and datatypes

--- 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)";