doc-src/TutorialI/Types/Pairs.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10560 f4da791d4850
child 10654 458068404143
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} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
    43 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
    44 \begin{center}
    45 @{thm split_def}
    46 \hfill(@{thm[source]split_def})
    47 \end{center}
    48 Pattern matching in
    49 other variable binding constructs is translated similarly. Thus we need to
    50 understand how to reason about such constructs.
    51 *}
    52 
    53 subsection{*Theorem proving*}
    54 
    55 text{*
    56 The most obvious approach is the brute force expansion of @{term split}:
    57 *}
    58 
    59 lemma "(\<lambda>(x,y).x) p = fst p"
    60 by(simp add:split_def)
    61 
    62 text{* This works well if rewriting with @{thm[source]split_def} finishes the
    63 proof, as in the above lemma. But if it doesn't, you end up with exactly what
    64 we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
    65 approach is neither elegant nor very practical in large examples, although it
    66 can be effective in small ones.
    67 
    68 If we step back and ponder why the above lemma presented a problem in the
    69 first place, we quickly realize that what we would like is to replace @{term
    70 p} with some concrete pair @{term"(a,b)"}, in which case both sides of the
    71 equation would simplify to @{term a} because of the simplification rules
    72 @{thm Product_Type.split[no_vars]} and @{thm fst_conv[no_vars]}.  This is the
    73 key problem one faces when reasoning about pattern matching with pairs: how to
    74 convert some atomic term into a pair.
    75 
    76 In case of a subterm of the form @{term"split f p"} this is easy: the split
    77 rule @{thm[source]split_split} replaces @{term p} by a pair:
    78 *}
    79 
    80 lemma "(\<lambda>(x,y).y) p = snd p"
    81 apply(simp only: split:split_split);
    82 
    83 txt{*
    84 @{subgoals[display,indent=0]}
    85 This subgoal is easily proved by simplification. The @{text"only:"} above
    86 merely serves to show the effect of splitting and to avoid solving the goal
    87 outright.
    88 
    89 Let us look at a second example:
    90 *}
    91 
    92 (*<*)by simp(*>*)
    93 lemma "let (x,y) = p in fst p = x";
    94 apply(simp only:Let_def)
    95 
    96 txt{*
    97 @{subgoals[display,indent=0]}
    98 A paired @{text let} reduces to a paired $\lambda$-abstraction, which
    99 can be split as above. The same is true for paired set comprehension:
   100 *}
   101 
   102 (*<*)by(simp split:split_split)(*>*)
   103 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
   104 apply simp
   105 
   106 txt{*
   107 @{subgoals[display,indent=0]}
   108 Again, simplification produces a term suitable for @{thm[source]split_split}
   109 as above. If you are worried about the funny form of the premise:
   110 @{term"split (op =)"} is the same as @{text"\<lambda>(x,y). x=y"}.
   111 The same procedure works for
   112 *}
   113 
   114 (*<*)by(simp split:split_split)(*>*)
   115 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
   116 
   117 txt{*\noindent
   118 except that we now have to use @{thm[source]split_split_asm}, because
   119 @{term split} occurs in the assumptions.
   120 
   121 However, splitting @{term split} is not always a solution, as no @{term split}
   122 may be present in the goal. Consider the following function:
   123 *}
   124 
   125 (*<*)by(simp split:split_split_asm)(*>*)
   126 consts swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
   127 primrec
   128   "swap (x,y) = (y,x)"
   129 
   130 text{*\noindent
   131 Note that the above \isacommand{primrec} definition is admissible
   132 because @{text"\<times>"} is a datatype. When we now try to prove
   133 *}
   134 
   135 lemma "swap(swap p) = p"
   136 
   137 txt{*\noindent
   138 simplification will do nothing, because the defining equation for @{term swap}
   139 expects a pair. Again, we need to turn @{term p} into a pair first, but this
   140 time there is no @{term split} in sight. In this case the only thing we can do
   141 is to split the term by hand:
   142 *}
   143 apply(case_tac p)
   144 
   145 txt{*\noindent
   146 @{subgoals[display,indent=0]}
   147 Again, @{text case_tac} is applicable because @{text"\<times>"} is a datatype.
   148 The subgoal is easily proved by @{text simp}.
   149 
   150 In case the term to be split is a quantified variable, there are more options.
   151 You can split \emph{all} @{text"\<And>"}-quantified variables in a goal
   152 with the rewrite rule @{thm[source]split_paired_all}:
   153 *}
   154 
   155 (*<*)by simp(*>*)
   156 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
   157 apply(simp only:split_paired_all)
   158 
   159 txt{*\noindent
   160 @{subgoals[display,indent=0]}
   161 *}
   162 
   163 apply simp
   164 done
   165 
   166 text{*\noindent
   167 Note that we have intentionally included only @{thm[source]split_paired_all}
   168 in the first simplification step. This time the reason was not merely
   169 pedagogical:
   170 @{thm[source]split_paired_all} may interfere with certain congruence
   171 rules of the simplifier, i.e.
   172 *}
   173 
   174 (*<*)
   175 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
   176 (*>*)
   177 apply(simp add:split_paired_all)
   178 (*<*)done(*>*)
   179 text{*\noindent
   180 may fail (here it does not) where the above two stages succeed.
   181 
   182 Finally, all @{text"\<forall>"} and @{text"\<exists>"}-quantified variables are split
   183 automatically by the simplifier:
   184 *}
   185 
   186 lemma "\<forall>p. \<exists>q. swap p = swap q"
   187 apply simp;
   188 done
   189 
   190 text{*\noindent
   191 In case you would like to turn off this automatic splitting, just disable the
   192 responsible simplification rules:
   193 \begin{center}
   194 @{thm split_paired_All}
   195 \hfill
   196 (@{thm[source]split_paired_All})\\
   197 @{thm split_paired_Ex}
   198 \hfill
   199 (@{thm[source]split_paired_Ex})
   200 \end{center}
   201 *}
   202 (*<*)
   203 end
   204 (*>*)