|
1 (*<*) |
|
2 theory pairs2 imports Main begin; |
|
3 (*>*) |
|
4 text{*\label{sec:pairs}\index{pairs and tuples} |
|
5 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
|
6 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
|
7 $\tau@i$. The functions \cdx{fst} and |
|
8 \cdx{snd} extract the components of a pair: |
|
9 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |
|
10 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands |
|
11 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for |
|
12 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have |
|
13 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. |
|
14 |
|
15 Remarks: |
|
16 \begin{itemize} |
|
17 \item |
|
18 There is also the type \tydx{unit}, which contains exactly one |
|
19 element denoted by~\cdx{()}. This type can be viewed |
|
20 as a degenerate product with 0 components. |
|
21 \item |
|
22 Products, like type @{typ nat}, are datatypes, which means |
|
23 in particular that @{text induct_tac} and @{text case_tac} are applicable to |
|
24 terms of product type. |
|
25 Both split the term into a number of variables corresponding to the tuple structure |
|
26 (up to 7 components). |
|
27 \item |
|
28 Tuples with more than two or three components become unwieldy; |
|
29 records are preferable. |
|
30 \end{itemize} |
|
31 For more information on pairs and records see Chapter~\ref{ch:more-types}. |
|
32 *} |
|
33 (*<*) |
|
34 end |
|
35 (*>*) |