summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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