|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{pairs}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \label{sec:pairs}\index{pairs and tuples} |
|
20 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
|
21 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
|
22 $\tau@i$. The functions \cdx{fst} and |
|
23 \cdx{snd} extract the components of a pair: |
|
24 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |
|
25 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands |
|
26 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for |
|
27 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have |
|
28 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. |
|
29 |
|
30 Remarks: |
|
31 \begin{itemize} |
|
32 \item |
|
33 There is also the type \tydx{unit}, which contains exactly one |
|
34 element denoted by~\cdx{()}. This type can be viewed |
|
35 as a degenerate product with 0 components. |
|
36 \item |
|
37 Products, like type \isa{nat}, are datatypes, which means |
|
38 in particular that \isa{induct{\isaliteral{5F}{\isacharunderscore}}tac} and \isa{case{\isaliteral{5F}{\isacharunderscore}}tac} are applicable to |
|
39 terms of product type. |
|
40 Both split the term into a number of variables corresponding to the tuple structure |
|
41 (up to 7 components). |
|
42 \item |
|
43 Tuples with more than two or three components become unwieldy; |
|
44 records are preferable. |
|
45 \end{itemize} |
|
46 For more information on pairs and records see Chapter~\ref{ch:more-types}.% |
|
47 \end{isamarkuptext}% |
|
48 \isamarkuptrue% |
|
49 % |
|
50 \isadelimtheory |
|
51 % |
|
52 \endisadelimtheory |
|
53 % |
|
54 \isatagtheory |
|
55 % |
|
56 \endisatagtheory |
|
57 {\isafoldtheory}% |
|
58 % |
|
59 \isadelimtheory |
|
60 % |
|
61 \endisadelimtheory |
|
62 \end{isabellebody}% |
|
63 %%% Local Variables: |
|
64 %%% mode: latex |
|
65 %%% TeX-master: "root" |
|
66 %%% End: |