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