--- a/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 10:22:38 2000 +0100
+++ b/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 13:44:26 2000 +0100
@@ -1,26 +1,28 @@
(*<*)
theory pairs = Main:;
(*>*)
-text{*
+text{*\label{sec:pairs}\indexbold{product type}
+\index{pair|see{product type}}\index{tuple|see{product type}}
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 @{term"fst"} and
-@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+\indexboldpos{\isasymtimes}{$Isatype} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by \isaindexbold{fst} and
+\isaindexbold{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}
-@{term"let (x,y) = f z in (y,x)"}\\
-@{term"case xs of [] => 0 | (x,y)#zs => x+y"}
-\end{quote}
-Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).
+There is also the type \isaindexbold{unit}, which contains exactly one
+element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+as a degenerate Cartesian product of 0 types.
+
+Note that products, like type @{typ nat}, are datatypes, which means
+in particular that @{text induct_tac} and @{text case_tac} are applicable to
+products (see \S\ref{sec:products}).
+
+Instead of tuples with many components (where ``many'' is not much above 2),
+it is far preferable to use records (see \S\ref{sec:records}).
*}
(*<*)
end