%
\begin{isabellebody}%
\def\isabellecontext{pairs}%
%
\begin{isamarkuptext}%
HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
$\tau@i$. The components of a pair are extracted by \isa{fst} and
\isa{snd}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
It is possible to use (nested) tuples as patterns in abstractions, for
example \isa{\isasymlambda(x,y,z).x+y+z} and
\isa{\isasymlambda((x,y),z).x+y+z}.
In addition to explicit $\lambda$-abstractions, tuple patterns can be used in
most variable binding constructs. Typical examples are
\begin{quote}
\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}
\end{quote}
Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: