src/Doc/Tutorial/Misc/pairs2.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
permissions -rw-r--r--
eliminated spurious semicolons;
nipkow@8745
     1
(*<*)
wenzelm@58860
     2
theory pairs2 imports Main begin
nipkow@9541
     3
(*>*)
paulson@11428
     4
text{*\label{sec:pairs}\index{pairs and tuples}
paulson@11428
     5
HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
nipkow@10538
     6
\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
paulson@11428
     7
$\tau@i$. The functions \cdx{fst} and
paulson@11428
     8
\cdx{snd} extract the components of a pair:
nipkow@10538
     9
 \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
nipkow@9933
    10
are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
nipkow@9933
    11
for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
nipkow@9933
    12
$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
nipkow@9933
    13
\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
nipkow@9541
    14
nipkow@10539
    15
Remarks:
nipkow@10539
    16
\begin{itemize}
nipkow@10539
    17
\item
paulson@11428
    18
There is also the type \tydx{unit}, which contains exactly one
paulson@11456
    19
element denoted by~\cdx{()}.  This type can be viewed
nipkow@10539
    20
as a degenerate product with 0 components.
nipkow@10539
    21
\item
nipkow@10539
    22
Products, like type @{typ nat}, are datatypes, which means
nipkow@10538
    23
in particular that @{text induct_tac} and @{text case_tac} are applicable to
nipkow@10539
    24
terms of product type.
wenzelm@27321
    25
Both split the term into a number of variables corresponding to the tuple structure
wenzelm@27321
    26
(up to 7 components).
nipkow@10539
    27
\item
paulson@10795
    28
Tuples with more than two or three components become unwieldy;
paulson@10795
    29
records are preferable.
nipkow@10539
    30
\end{itemize}
nipkow@10539
    31
For more information on pairs and records see Chapter~\ref{ch:more-types}.
nipkow@9541
    32
*}
nipkow@8745
    33
(*<*)
nipkow@8745
    34
end
nipkow@8745
    35
(*>*)