author nipkow Wed, 31 Aug 1994 17:34:12 +0200 changeset 580 909e00299009 parent 579 08f465e23dc5 child 581 465075fd257b
Updated datatype documentation with a few hints
--- a/doc-src/Logics/Old_HOL.tex	Thu Aug 25 12:21:00 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Wed Aug 31 17:34:12 1994 +0200
@@ -1247,10 +1247,10 @@

A datatype declaration has the following general structure:
$\mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ - c_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~ - c_m(\tau_{m1},\dots,\tau_{mk_m}) + C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~ + C_m(\tau_{m1},\dots,\tau_{mk_m})$
-where $\alpha_i$ are type variables, $c_i$ are distinct constructor names and
+where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
$\tau_{ij}$ are one of the following:
\begin{itemize}
\item type variables $\alpha_1,\dots,\alpha_n$,
@@ -1262,17 +1262,24 @@
least one constructor must consist of only non-recursive type
components.}
\end{itemize}
+If you would like one of the $\tau_{ij}$ to be a complex type expression
+$\tau$ you need to declare a new type synonym $syn = \tau$ first and use
+$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the
+recursive type itself, thus ruling out problematic cases like $\mbox{\tt + datatype}~ t ~=~ C(t \To t)$ together with unproblematic ones like $+\mbox{\tt datatype}~ t ~=~ C(t~list).$
+
The constructors are automatically defined as functions of their respective
type:
-$c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t$
+$C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t$
These functions have certain {\em freeness} properties:
\begin{description}
\item[\tt distinct] They are distinct:
-$c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad +\[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad \mbox{for all}~ i \neq j.$
\item[\tt inject] They are injective:
-$(c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) = +\[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) = (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})$
\end{description}
@@ -1282,9 +1289,9 @@
natural number
$\begin{array}{lcl} -\mbox{\it t\_ord}(c_1(x_1,\dots,x_{k_1})) & = & 0 \\ +\mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\ & \vdots & \\ -\mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1 +\mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1 \end{array}$
and distinctness of constructors is expressed by:
@@ -1297,11 +1304,11 @@
{\begin{array}{lcl}
\Forall x_1\dots x_{k_1}.
\List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &
-  \Imp  & P(c_1(x_1,\dots,x_{k_1})) \\
+  \Imp  & P(C_1(x_1,\dots,x_{k_1})) \\
& \vdots & \\
\Forall x_1\dots x_{k_m}.
\List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &
-  \Imp & P(c_m(x_1,\dots,x_{k_m}))
+  \Imp & P(C_m(x_1,\dots,x_{k_m}))
\end{array}}
\]
where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} @@ -1311,9 +1318,9 @@ The type also comes with an \ML-like \sdx{case}-construct: $\begin{array}{rrcl} -\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ +\mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ \vdots \\ - \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m + \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m \end{array}$ In contrast to \ML, {\em all} constructors must be present, their order is @@ -1553,7 +1560,7 @@ \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness proofs about insertion sort and quick sort. -\item[HOL/ex/PL.ML] proves the soundness and completeness of classical +\item[HOL/ex/PropLog.ML] proves the soundness and completeness of classical propositional logic, given a truth table semantics. The only connective is$\imp\$.  A Hilbert-style axiom system is specified, and its set of
theorems defined inductively.  A similar proof in \ZF{} is described