doc-src/TutorialI/Types/Pairs.thy
 author nipkow Fri Dec 01 12:15:47 2000 +0100 (2000-12-01) changeset 10560 f4da791d4850 child 10608 620647438780 permissions -rw-r--r--
*** empty log message ***
 nipkow@10560  1 (*<*)theory Pairs = Main:(*>*)  nipkow@10560  2 nipkow@10560  3 section{*Pairs*}  nipkow@10560  4 nipkow@10560  5 text{*\label{sec:products}  nipkow@10560  6 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal  nipkow@10560  7 repertoire of operations: pairing and the two projections @{term fst} and  nipkow@10560  8 @{term snd}. In any nontrivial application of pairs you will find that this  nipkow@10560  9 quickly leads to unreadable formulae involvings nests of projections. This  nipkow@10560  10 section is concerned with introducing some syntactic sugar to overcome this  nipkow@10560  11 problem: pattern matching with tuples.  nipkow@10560  12 *}  nipkow@10560  13 nipkow@10560  14 subsection{*Notation*}  nipkow@10560  15 nipkow@10560  16 text{*  nipkow@10560  17 It is possible to use (nested) tuples as patterns in $\lambda$-abstractions,  nipkow@10560  18 for example @{text"\(x,y,z).x+y+z"} and @{text"\((x,y),z).x+y+z"}. In fact,  nipkow@10560  19 tuple patterns can be used in most variable binding constructs. Here are  nipkow@10560  20 some typical examples:  nipkow@10560  21 \begin{quote}  nipkow@10560  22 @{term"let (x,y) = f z in (y,x)"}\\  nipkow@10560  23 @{term"case xs of [] => 0 | (x,y)#zs => x+y"}\\  nipkow@10560  24 @{text"\(x,y)\A. x=y"}\\  nipkow@10560  25 @{text"{(x,y). x=y}"}\\  nipkow@10560  26 @{term"\(x,y)\A. {x+y}"}  nipkow@10560  27 \end{quote}  nipkow@10560  28 *}  nipkow@10560  29 nipkow@10560  30 text{*  nipkow@10560  31 The intuitive meaning of this notations should be pretty obvious.  nipkow@10560  32 Unfortunately, we need to know in more detail what the notation really stands  nipkow@10560  33 for once we have to reason about it. The fact of the matter is that abstraction  nipkow@10560  34 over pairs and tuples is merely a convenient shorthand for a more complex  nipkow@10560  35 internal representation. Thus the internal and external form of a term may  nipkow@10560  36 differ, which can affect proofs. If you want to avoid this complication,  nipkow@10560  37 stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"}  nipkow@10560  38 instead of @{text"\(x,y). x+y"} (which denote the same function but are quite  nipkow@10560  39 different terms).  nipkow@10560  40 nipkow@10560  41 Internally, @{term"%(x,y). t"} becomes @{text"split (\x y. t)"}, where  nipkow@10560  42 @{term split} is the uncurrying function of type @{text"('a \ 'b  nipkow@10560  43 \ 'c) \ 'a \ 'b \ 'c"} defined as  nipkow@10560  44 \begin{center}  nipkow@10560  45 @{thm split_def}  nipkow@10560  46 \hfill(@{thm[source]split_def})  nipkow@10560  47 \end{center}  nipkow@10560  48 Pattern matching in  nipkow@10560  49 other variable binding constructs is translated similarly. Thus we need to  nipkow@10560  50 understand how to reason about such constructs.  nipkow@10560  51 *}  nipkow@10560  52 nipkow@10560  53 subsection{*Theorem proving*}  nipkow@10560  54 nipkow@10560  55 text{*  nipkow@10560  56 The most obvious approach is the brute force expansion of @{term split}:  nipkow@10560  57 *}  nipkow@10560  58 nipkow@10560  59 lemma "(\(x,y).x) p = fst p"  nipkow@10560  60 by(simp add:split_def)  nipkow@10560  61 nipkow@10560  62 text{* This works well if rewriting with @{thm[source]split_def} finishes the  nipkow@10560  63 proof, as in the above lemma. But if it doesn't, you end up with exactly what  nipkow@10560  64 we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this  nipkow@10560  65 approach is neither elegant nor very practical in large examples, although it  nipkow@10560  66 can be effective in small ones.  nipkow@10560  67 nipkow@10560  68 If we step back and ponder why the above lemma presented a problem in the  nipkow@10560  69 first place, we quickly realize that what we would like is to replace @{term  nipkow@10560  70 p} with some concrete pair @{term"(a,b)"}, in which case both sides of the  nipkow@10560  71 equation would simplify to @{term a} because of the simplification rules  nipkow@10560  72 @{thm Product_Type.split[no_vars]} and @{thm fst_conv[no_vars]}. This is the  nipkow@10560  73 key problem one faces when reasoning about pattern matching with pairs: how to  nipkow@10560  74 convert some atomic term into a pair.  nipkow@10560  75 nipkow@10560  76 In case of a subterm of the form @{term"split f p"} this is easy: the split  nipkow@10560  77 rule @{thm[source]split_split} replaces @{term p} by a pair:  nipkow@10560  78 *}  nipkow@10560  79 nipkow@10560  80 lemma "(\(x,y).y) p = snd p"  nipkow@10560  81 apply(simp only: split:split_split);  nipkow@10560  82 nipkow@10560  83 txt{*  nipkow@10560  84 @{subgoals[display,indent=0]}  nipkow@10560  85 This subgoal is easily proved by simplification. The @{text"only:"} above  nipkow@10560  86 merely serves to show the effect of splitting and to avoid solving the goal  nipkow@10560  87 outright.  nipkow@10560  88 nipkow@10560  89 Let us look at a second example:  nipkow@10560  90 *}  nipkow@10560  91 nipkow@10560  92 (*<*)by simp(*>*)  nipkow@10560  93 lemma "let (x,y) = p in fst p = x";  nipkow@10560  94 apply(simp only:Let_def)  nipkow@10560  95 nipkow@10560  96 txt{*  nipkow@10560  97 @{subgoals[display,indent=0]}  nipkow@10560  98 A paired @{text let} reduces to a paired $\lambda$-abstraction, which  nipkow@10560  99 can be split as above. The same is true for paired set comprehension:  nipkow@10560  100 *}  nipkow@10560  101 nipkow@10560  102 (*<*)by(simp split:split_split)(*>*)  nipkow@10560  103 lemma "p \ {(x,y). x=y} \ fst p = snd p"  nipkow@10560  104 apply simp  nipkow@10560  105 nipkow@10560  106 txt{*  nipkow@10560  107 @{subgoals[display,indent=0]}  nipkow@10560  108 Again, simplification produces a term suitable for @{thm[source]split_split}  nipkow@10560  109 as above. If you are worried about the funny form of the premise:  nipkow@10560  110 @{term"split (op =)"} is the same as @{text"\(x,y). x=y"}.  nipkow@10560  111 The same procedure works for  nipkow@10560  112 *}  nipkow@10560  113 nipkow@10560  114 (*<*)by(simp split:split_split)(*>*)  nipkow@10560  115 lemma "p \ {(x,y). x=y} \ fst p = snd p"  nipkow@10560  116 nipkow@10560  117 txt{*\noindent  nipkow@10560  118 except that we now have to use @{thm[source]split_split_asm}, because  nipkow@10560  119 @{term split} occurs in the assumptions.  nipkow@10560  120 nipkow@10560  121 However, splitting @{term split} is not always a solution, as no @{term split}  nipkow@10560  122 may be present in the goal. Consider the following function:  nipkow@10560  123 *}  nipkow@10560  124 nipkow@10560  125 (*<*)by(simp split:split_split_asm)(*>*)  nipkow@10560  126 consts swap :: "'a \ 'b \ 'b \ 'a"  nipkow@10560  127 primrec  nipkow@10560  128  "swap (x,y) = (y,x)"  nipkow@10560  129 nipkow@10560  130 text{*\noindent  nipkow@10560  131 Note that the above \isacommand{primrec} definition is admissible  nipkow@10560  132 because @{text"\"} is a datatype. When we now try to prove  nipkow@10560  133 *}  nipkow@10560  134 nipkow@10560  135 lemma "swap(swap p) = p"  nipkow@10560  136 nipkow@10560  137 txt{*\noindent  nipkow@10560  138 simplification will do nothing, because the defining equation for @{term swap}  nipkow@10560  139 expects a pair. Again, we need to turn @{term p} into a pair first, but this  nipkow@10560  140 time there is no @{term split} in sight. In this case the only thing we can do  nipkow@10560  141 is to split the term by hand:  nipkow@10560  142 *}  nipkow@10560  143 apply(case_tac p)  nipkow@10560  144 nipkow@10560  145 txt{*\noindent  nipkow@10560  146 @{subgoals[display,indent=0]}  nipkow@10560  147 Again, @{text case_tac} is applicable because @{text"\"} is a datatype.  nipkow@10560  148 The subgoal is easily proved by @{text simp}.  nipkow@10560  149 nipkow@10560  150 In case the term to be split is a quantified variable, there are more options.  nipkow@10560  151 You can split \emph{all} @{text"\"}-quantified variables in a goal  nipkow@10560  152 with the rewrite rule @{thm[source]split_paired_all}:  nipkow@10560  153 *}  nipkow@10560  154 nipkow@10560  155 (*<*)by simp(*>*)  nipkow@10560  156 lemma "\p q. swap(swap p) = q \ p = q"  nipkow@10560  157 apply(simp only:split_paired_all)  nipkow@10560  158 nipkow@10560  159 txt{*\noindent  nipkow@10560  160 @{subgoals[display,indent=0]}  nipkow@10560  161 *}  nipkow@10560  162 nipkow@10560  163 apply simp  nipkow@10560  164 done  nipkow@10560  165 nipkow@10560  166 text{*\noindent  nipkow@10560  167 Note that we have intentionally included only @{thm[source]split_paired_all}  nipkow@10560  168 in the first simplification step. This time the reason was not merely  nipkow@10560  169 pedagogical:  nipkow@10560  170 @{thm[source]split_paired_all} may interfere with certain congruence  nipkow@10560  171 rules of the simplifier, i.e.  nipkow@10560  172 *}  nipkow@10560  173 nipkow@10560  174 (*<*)  nipkow@10560  175 lemma "\p q. swap(swap p) = q \ p = q"  nipkow@10560  176 (*>*)  nipkow@10560  177 apply(simp add:split_paired_all)  nipkow@10560  178 (*<*)done(*>*)  nipkow@10560  179 text{*\noindent  nipkow@10560  180 may fail (here it does not) where the above two stages succeed.  nipkow@10560  181 nipkow@10560  182 Finally, all @{text"\"} and @{text"\"}-quantified variables are split  nipkow@10560  183 automatically by the simplifier:  nipkow@10560  184 *}  nipkow@10560  185 nipkow@10560  186 lemma "\p. \q. swap p = swap q"  nipkow@10560  187 apply simp;  nipkow@10560  188 done  nipkow@10560  189 nipkow@10560  190 text{*\noindent  nipkow@10560  191 In case you would like to turn off this automatic splitting, just disable the  nipkow@10560  192 responsible simplification rules:  nipkow@10560  193 \begin{center}  nipkow@10560  194 @{thm split_paired_All}  nipkow@10560  195 \hfill  nipkow@10560  196 (@{thm[source]split_paired_All})\\  nipkow@10560  197 @{thm split_paired_Ex}  nipkow@10560  198 \hfill  nipkow@10560  199 (@{thm[source]split_paired_Ex})  nipkow@10560  200 \end{center}  nipkow@10560  201 *}  nipkow@10560  202 (*<*)  nipkow@10560  203 end  nipkow@10560  204 (*>*)