8745
|
1 |
(*<*)
|
|
2 |
theory pairs = Main:;
|
9541
|
3 |
(*>*)
|
|
4 |
text{*
|
9933
|
5 |
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
|
|
6 |
\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
|
|
7 |
$\tau@i$. The components of a pair are extracted by @{term"fst"} and
|
|
8 |
@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
|
|
9 |
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
|
|
10 |
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
|
|
11 |
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
|
|
12 |
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
|
9541
|
13 |
|
|
14 |
It is possible to use (nested) tuples as patterns in abstractions, for
|
|
15 |
example \isa{\isasymlambda(x,y,z).x+y+z} and
|
|
16 |
\isa{\isasymlambda((x,y),z).x+y+z}.
|
|
17 |
In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
|
|
18 |
most variable binding constructs. Typical examples are
|
|
19 |
\begin{quote}
|
|
20 |
@{term"let (x,y) = f z in (y,x)"}\\
|
|
21 |
@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
|
|
22 |
\end{quote}
|
|
23 |
Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
|
|
24 |
*}
|
8745
|
25 |
(*<*)
|
|
26 |
end
|
|
27 |
(*>*)
|