doc-src/TutorialI/Misc/pairs.thy
 author wenzelm Mon, 23 Jun 2008 15:26:51 +0200 changeset 27321 464ac1c815ec parent 16417 9bc16273c2d4 permissions -rw-r--r--
induct_tac/case_tac: nested tuples are split as expected;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset  1 (*<*)  16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 11456 diff changeset  2 theory pairs imports Main begin;  9541 d17c0b34d5c8 *** empty log message *** nipkow parents: 8745 diff changeset  3 (*>*)  11428 332347b9b942 tidying the index paulson parents: 10839 diff changeset  4 text{*\label{sec:pairs}\index{pairs and tuples}  332347b9b942 tidying the index paulson parents: 10839 diff changeset  5 HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$  10538 d1bf9ca9008d *** empty log message *** nipkow parents: 9933 diff changeset  6 \indexboldpos{\isasymtimes}{$Isatype}$\tau@2$provided each$a@i$is of type  11428 332347b9b942 tidying the index paulson parents: 10839 diff changeset  7 $\tau@i$. The functions \cdx{fst} and  332347b9b942 tidying the index paulson parents: 10839 diff changeset  8 \cdx{snd} extract the components of a pair:  10538 d1bf9ca9008d *** empty log message *** nipkow parents: 9933 diff changeset  9  \isa{fst($x$,$y$) =$x$} and \isa{snd($x$,$y$) =$y$}. Tuples  9933 9feb1e0c4cb3 *** empty log message *** nipkow parents: 9792 diff changeset  10 are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands  9feb1e0c4cb3 *** empty log message *** nipkow parents: 9792 diff changeset  11 for \isa{($a@1$,($a@2$,$a@3$))} and$\tau@1 \times \tau@2 \times \tau@3$for  9feb1e0c4cb3 *** empty log message *** nipkow parents: 9792 diff changeset  12 $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have  9feb1e0c4cb3 *** empty log message *** nipkow parents: 9792 diff changeset  13 \isa{fst(snd($a@1$,$a@2$,$a@3$)) =$a@2\$}.  9541 d17c0b34d5c8 *** empty log message *** nipkow parents: 8745 diff changeset  14 10539 5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  15 Remarks:  5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  16 \begin{itemize}  5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  17 \item  11428 332347b9b942 tidying the index paulson parents: 10839 diff changeset  18 There is also the type \tydx{unit}, which contains exactly one  11456 7eb63f63e6c6 revisions and indexing paulson parents: 11428 diff changeset  19 element denoted by~\cdx{()}. This type can be viewed  10539 5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  20 as a degenerate product with 0 components.  5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  21 \item  5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  22 Products, like type @{typ nat}, are datatypes, which means  10538 d1bf9ca9008d *** empty log message *** nipkow parents: 9933 diff changeset  23 in particular that @{text induct_tac} and @{text case_tac} are applicable to  10539 5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  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 5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  27 \item  10795 9e888d60d3e5 minor edits to Chapters 1-3 paulson parents: 10543 diff changeset  28 Tuples with more than two or three components become unwieldy;  9e888d60d3e5 minor edits to Chapters 1-3 paulson parents: 10543 diff changeset  29 records are preferable.  10539 5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  30 \end{itemize}  5929460a41df *** empty log message *** nipkow parents: 10538 diff changeset  31 For more information on pairs and records see Chapter~\ref{ch:more-types}.  9541 d17c0b34d5c8 *** empty log message *** nipkow parents: 8745 diff changeset  32 *}  8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset  33 (*<*)  13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset  34 end  13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset  35 (*>*)