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