1245 |
1245 |
1246 \subsection{Foundations} |
1246 \subsection{Foundations} |
1247 |
1247 |
1248 A datatype declaration has the following general structure: |
1248 A datatype declaration has the following general structure: |
1249 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ |
1249 \[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ |
1250 c_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~ |
1250 C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~ |
1251 c_m(\tau_{m1},\dots,\tau_{mk_m}) |
1251 C_m(\tau_{m1},\dots,\tau_{mk_m}) |
1252 \] |
1252 \] |
1253 where $\alpha_i$ are type variables, $c_i$ are distinct constructor names and |
1253 where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and |
1254 $\tau_{ij}$ are one of the following: |
1254 $\tau_{ij}$ are one of the following: |
1255 \begin{itemize} |
1255 \begin{itemize} |
1256 \item type variables $\alpha_1,\dots,\alpha_n$, |
1256 \item type variables $\alpha_1,\dots,\alpha_n$, |
1257 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared |
1257 \item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared |
1258 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq |
1258 type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq |
1260 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This |
1260 \item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This |
1261 makes it a recursive type. To ensure that the new type is not empty at |
1261 makes it a recursive type. To ensure that the new type is not empty at |
1262 least one constructor must consist of only non-recursive type |
1262 least one constructor must consist of only non-recursive type |
1263 components.} |
1263 components.} |
1264 \end{itemize} |
1264 \end{itemize} |
|
1265 If you would like one of the $\tau_{ij}$ to be a complex type expression |
|
1266 $\tau$ you need to declare a new type synonym $syn = \tau$ first and use |
|
1267 $syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the |
|
1268 recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt |
|
1269 datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ |
|
1270 \mbox{\tt datatype}~ t ~=~ C(t~list). \] |
|
1271 |
1265 The constructors are automatically defined as functions of their respective |
1272 The constructors are automatically defined as functions of their respective |
1266 type: |
1273 type: |
1267 \[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] |
1274 \[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] |
1268 These functions have certain {\em freeness} properties: |
1275 These functions have certain {\em freeness} properties: |
1269 \begin{description} |
1276 \begin{description} |
1270 \item[\tt distinct] They are distinct: |
1277 \item[\tt distinct] They are distinct: |
1271 \[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad |
1278 \[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad |
1272 \mbox{for all}~ i \neq j. |
1279 \mbox{for all}~ i \neq j. |
1273 \] |
1280 \] |
1274 \item[\tt inject] They are injective: |
1281 \item[\tt inject] They are injective: |
1275 \[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) = |
1282 \[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) = |
1276 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) |
1283 (x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) |
1277 \] |
1284 \] |
1278 \end{description} |
1285 \end{description} |
1279 Because the number of inequalities is quadratic in the number of |
1286 Because the number of inequalities is quadratic in the number of |
1280 constructors, a different method is used if their number exceeds |
1287 constructors, a different method is used if their number exceeds |
1281 a certain value, currently 4. In that case every constructor is mapped to a |
1288 a certain value, currently 4. In that case every constructor is mapped to a |
1282 natural number |
1289 natural number |
1283 \[ |
1290 \[ |
1284 \begin{array}{lcl} |
1291 \begin{array}{lcl} |
1285 \mbox{\it t\_ord}(c_1(x_1,\dots,x_{k_1})) & = & 0 \\ |
1292 \mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\ |
1286 & \vdots & \\ |
1293 & \vdots & \\ |
1287 \mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m-1 |
1294 \mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m-1 |
1288 \end{array} |
1295 \end{array} |
1289 \] |
1296 \] |
1290 and distinctness of constructors is expressed by: |
1297 and distinctness of constructors is expressed by: |
1291 \[ |
1298 \[ |
1292 \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y. |
1299 \mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y. |
1295 \[ |
1302 \[ |
1296 \infer{P(x)} |
1303 \infer{P(x)} |
1297 {\begin{array}{lcl} |
1304 {\begin{array}{lcl} |
1298 \Forall x_1\dots x_{k_1}. |
1305 \Forall x_1\dots x_{k_1}. |
1299 \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} & |
1306 \List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} & |
1300 \Imp & P(c_1(x_1,\dots,x_{k_1})) \\ |
1307 \Imp & P(C_1(x_1,\dots,x_{k_1})) \\ |
1301 & \vdots & \\ |
1308 & \vdots & \\ |
1302 \Forall x_1\dots x_{k_m}. |
1309 \Forall x_1\dots x_{k_m}. |
1303 \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} & |
1310 \List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} & |
1304 \Imp & P(c_m(x_1,\dots,x_{k_m})) |
1311 \Imp & P(C_m(x_1,\dots,x_{k_m})) |
1305 \end{array}} |
1312 \end{array}} |
1306 \] |
1313 \] |
1307 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} |
1314 where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} |
1308 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for |
1315 = (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for |
1309 all arguments of the recursive type. |
1316 all arguments of the recursive type. |
1310 |
1317 |
1311 The type also comes with an \ML-like \sdx{case}-construct: |
1318 The type also comes with an \ML-like \sdx{case}-construct: |
1312 \[ |
1319 \[ |
1313 \begin{array}{rrcl} |
1320 \begin{array}{rrcl} |
1314 \mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ |
1321 \mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ |
1315 \vdots \\ |
1322 \vdots \\ |
1316 \mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m |
1323 \mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m |
1317 \end{array} |
1324 \end{array} |
1318 \] |
1325 \] |
1319 In contrast to \ML, {\em all} constructors must be present, their order is |
1326 In contrast to \ML, {\em all} constructors must be present, their order is |
1320 fixed, and nested patterns are not supported. |
1327 fixed, and nested patterns are not supported. |
1321 |
1328 |
1551 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. |
1558 \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem. |
1552 |
1559 |
1553 \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness |
1560 \item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness |
1554 proofs about insertion sort and quick sort. |
1561 proofs about insertion sort and quick sort. |
1555 |
1562 |
1556 \item[HOL/ex/PL.ML] proves the soundness and completeness of classical |
1563 \item[HOL/ex/PropLog.ML] proves the soundness and completeness of classical |
1557 propositional logic, given a truth table semantics. The only connective |
1564 propositional logic, given a truth table semantics. The only connective |
1558 is $\imp$. A Hilbert-style axiom system is specified, and its set of |
1565 is $\imp$. A Hilbert-style axiom system is specified, and its set of |
1559 theorems defined inductively. A similar proof in \ZF{} is described |
1566 theorems defined inductively. A similar proof in \ZF{} is described |
1560 elsewhere~\cite{paulson-set-II}. |
1567 elsewhere~\cite{paulson-set-II}. |
1561 |
1568 |