5 HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
6 $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
7 are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
8 \isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
9 \isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
10 \isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
11 $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
13 It is possible to use (nested) tuples as patterns in abstractions, for
14 example \isa{\isasymlambda(x,y,z).x+y+z} and
15 \isa{\isasymlambda((x,y),z).x+y+z}.
16 In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
17 most variable binding constructs. Typical examples are
19 \isa{let\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharequal}\ \mbox{f}\ \mbox{z}\ in\ {\isacharparenleft}\mbox{y}{\isacharcomma}\ \mbox{x}{\isacharparenright}}\\
20 \isa{case\ \mbox{xs}\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ {\isacharparenleft}\mbox{x}{\isacharcomma}\ \mbox{y}{\isacharparenright}\ {\isacharhash}\ \mbox{zs}\ {\isasymRightarrow}\ \mbox{x}\ {\isacharplus}\ \mbox{y}}
22 Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
27 %%% TeX-master: "root"