src/Doc/Tutorial/Types/Pairs.thy
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 58860 fee7cfa69c50
child 67399 eab6ce8368fa
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
     1 (*<*)theory Pairs imports Main begin(*>*)
     2 
     3 section{*Pairs and Tuples*}
     4 
     5 text{*\label{sec:products}
     6 Ordered 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 non-trivial application of pairs you will find that this
     9 quickly leads to unreadable nests of projections. This
    10 section introduces syntactic sugar to overcome this
    11 problem: pattern matching with tuples.
    12 *}
    13 
    14 subsection{*Pattern Matching with Tuples*}
    15 
    16 text{*
    17 Tuples may be used 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,
    20 and they can be nested. Here are
    21 some typical examples:
    22 \begin{quote}
    23 @{term"let (x,y) = f z in (y,x)"}\\
    24 @{term"case xs of [] => (0::nat) | (x,y)#zs => x+y"}\\
    25 @{text"\<forall>(x,y)\<in>A. x=y"}\\
    26 @{text"{(x,y,z). x=z}"}\\
    27 @{term"\<Union>(x,y)\<in>A. {x+y}"}
    28 \end{quote}
    29 The intuitive meanings of these expressions should be obvious.
    30 Unfortunately, we need to know in more detail what the notation really stands
    31 for once we have to reason about it.  Abstraction
    32 over pairs and tuples is merely a convenient shorthand for a more complex
    33 internal representation.  Thus the internal and external form of a term may
    34 differ, which can affect proofs. If you want to avoid this complication,
    35 stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"}
    36 instead of @{text"\<lambda>(x,y). x+y"}.  These terms are distinct even though they
    37 denote the same function.
    38 
    39 Internally, @{term"%(x,y). t"} becomes @{text"case_prod (\<lambda>x y. t)"}, where
    40 \cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
    41 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
    42 \begin{center}
    43 @{thm split_def}
    44 \hfill(@{thm[source]split_def})
    45 \end{center}
    46 Pattern matching in
    47 other variable binding constructs is translated similarly. Thus we need to
    48 understand how to reason about such constructs.
    49 *}
    50 
    51 subsection{*Theorem Proving*}
    52 
    53 text{*
    54 The most obvious approach is the brute force expansion of @{term split}:
    55 *}
    56 
    57 lemma "(\<lambda>(x,y).x) p = fst p"
    58 by(simp add: split_def)
    59 
    60 text{* \noindent
    61 This works well if rewriting with @{thm[source]split_def} finishes the
    62 proof, as it does above.  But if it does not, you end up with exactly what
    63 we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
    64 approach is neither elegant nor very practical in large examples, although it
    65 can be effective in small ones.
    66 
    67 If we consider why this lemma presents a problem, 
    68 we realize that we need to replace variable~@{term
    69 p} by some pair @{term"(a,b)"}.  Then both sides of the
    70 equation would simplify to @{term a} by the simplification rules
    71 @{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.  
    72 To reason about tuple patterns requires some way of
    73 converting a variable of product type into a pair.
    74 In case of a subterm of the form @{term"case_prod f p"} this is easy: the split
    75 rule @{thm[source]prod.split} replaces @{term p} by a pair:%
    76 \index{*split (method)}
    77 *}
    78 
    79 lemma "(\<lambda>(x,y).y) p = snd p"
    80 apply(split prod.split)
    81 
    82 txt{*
    83 @{subgoals[display,indent=0]}
    84 This subgoal is easily proved by simplification. Thus we could have combined
    85 simplification and splitting in one command that proves the goal outright:
    86 *}
    87 (*<*)
    88 by simp
    89 lemma "(\<lambda>(x,y).y) p = snd p"(*>*)
    90 by(simp split: prod.split)
    91 
    92 text{*
    93 Let us look at a second example:
    94 *}
    95 
    96 lemma "let (x,y) = p in fst p = x"
    97 apply(simp only: Let_def)
    98 
    99 txt{*
   100 @{subgoals[display,indent=0]}
   101 A paired @{text let} reduces to a paired $\lambda$-abstraction, which
   102 can be split as above. The same is true for paired set comprehension:
   103 *}
   104 
   105 (*<*)by(simp split: prod.split)(*>*)
   106 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
   107 apply simp
   108 
   109 txt{*
   110 @{subgoals[display,indent=0]}
   111 Again, simplification produces a term suitable for @{thm[source]prod.split}
   112 as above. If you are worried about the strange form of the premise:
   113 @{text"case_prod (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
   114 The same proof procedure works for
   115 *}
   116 
   117 (*<*)by(simp split: prod.split)(*>*)
   118 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
   119 
   120 txt{*\noindent
   121 except that we now have to use @{thm[source]prod.split_asm}, because
   122 @{term split} occurs in the assumptions.
   123 
   124 However, splitting @{term split} is not always a solution, as no @{term split}
   125 may be present in the goal. Consider the following function:
   126 *}
   127 
   128 (*<*)by(simp split: prod.split_asm)(*>*)
   129 primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "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
   140 @{const[source] swap} expects a pair. Again, we need to turn @{term p}
   141 into a pair first, but this time there is no @{term split} in sight.
   142 The only thing we can do is to split the term by hand:
   143 *}
   144 apply(case_tac p)
   145 
   146 txt{*\noindent
   147 @{subgoals[display,indent=0]}
   148 Again, \methdx{case_tac} is applicable because @{text"\<times>"} is a datatype.
   149 The subgoal is easily proved by @{text simp}.
   150 
   151 Splitting by @{text case_tac} also solves the previous examples and may thus
   152 appear preferable to the more arcane methods introduced first. However, see
   153 the warning about @{text case_tac} in \S\ref{sec:struct-ind-case}.
   154 
   155 Alternatively, you can split \emph{all} @{text"\<And>"}-quantified variables
   156 in a goal with the rewrite rule @{thm[source]split_paired_all}:
   157 *}
   158 
   159 (*<*)by simp(*>*)
   160 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
   161 apply(simp only: split_paired_all)
   162 
   163 txt{*\noindent
   164 @{subgoals[display,indent=0,margin=70]}
   165 *}
   166 
   167 apply simp
   168 done
   169 
   170 text{*\noindent
   171 Note that we have intentionally included only @{thm[source]split_paired_all}
   172 in the first simplification step, and then we simplify again. 
   173 This time the reason was not merely
   174 pedagogical:
   175 @{thm[source]split_paired_all} may interfere with other functions
   176 of the simplifier.
   177 The following command could fail (here it does not)
   178 where two separate \isa{simp} applications succeed.
   179 *}
   180 
   181 (*<*)
   182 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
   183 (*>*)
   184 apply(simp add: split_paired_all)
   185 (*<*)done(*>*)
   186 text{*\noindent
   187 Finally, the simplifier automatically splits all @{text"\<forall>"} and
   188 @{text"\<exists>"}-quantified variables:
   189 *}
   190 
   191 lemma "\<forall>p. \<exists>q. swap p = swap q"
   192 by simp
   193 
   194 text{*\noindent
   195 To turn off this automatic splitting, disable the
   196 responsible simplification rules:
   197 \begin{center}
   198 @{thm split_paired_All[no_vars]}
   199 \hfill
   200 (@{thm[source]split_paired_All})\\
   201 @{thm split_paired_Ex[no_vars]}
   202 \hfill
   203 (@{thm[source]split_paired_Ex})
   204 \end{center}
   205 *}
   206 (*<*)
   207 end
   208 (*>*)