1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{pairs}% |
3 \def\isabellecontext{pairs}% |
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \label{sec:pairs}\indexbold{pair} |
6 \label{sec:pairs}\index{pairs and tuples} |
7 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
7 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$ |
8 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
8 \indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type |
9 $\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and |
9 $\tau@i$. The functions \cdx{fst} and |
10 \isaindexbold{snd}: |
10 \cdx{snd} extract the components of a pair: |
11 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |
11 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples |
12 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands |
12 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands |
13 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for |
13 for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for |
14 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have |
14 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have |
15 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. |
15 \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. |
16 |
16 |
17 Remarks: |
17 Remarks: |
18 \begin{itemize} |
18 \begin{itemize} |
19 \item |
19 \item |
20 There is also the type \isaindexbold{unit}, which contains exactly one |
20 There is also the type \tydx{unit}, which contains exactly one |
21 element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed |
21 element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed |
22 as a degenerate product with 0 components. |
22 as a degenerate product with 0 components. |
23 \item |
23 \item |
24 Products, like type \isa{nat}, are datatypes, which means |
24 Products, like type \isa{nat}, are datatypes, which means |
25 in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to |
25 in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to |