doc-src/TutorialI/Types/document/Pairs.tex
author paulson
Sun Feb 15 10:46:37 2004 +0100 (2004-02-15)
changeset 14387 e96d5c42c4b0
parent 13791 3b6ff7ceaf27
child 15446 b022b72ccc03
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Pairs}%
     4 \isamarkupfalse%
     5 %
     6 \isamarkupsection{Pairs and Tuples%
     7 }
     8 \isamarkuptrue%
     9 %
    10 \begin{isamarkuptext}%
    11 \label{sec:products}
    12 Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
    13 repertoire of operations: pairing and the two projections \isa{fst} and
    14 \isa{snd}. In any non-trivial application of pairs you will find that this
    15 quickly leads to unreadable nests of projections. This
    16 section introduces syntactic sugar to overcome this
    17 problem: pattern matching with tuples.%
    18 \end{isamarkuptext}%
    19 \isamarkuptrue%
    20 %
    21 \isamarkupsubsection{Pattern Matching with Tuples%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Tuples may be used as patterns in $\lambda$-abstractions,
    27 for example \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z} and \isa{{\isasymlambda}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z}. In fact,
    28 tuple patterns can be used in most variable binding constructs,
    29 and they can be nested. Here are
    30 some typical examples:
    31 \begin{quote}
    32 \isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
    33 \isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
    34 \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
    35 \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
    36 \isa{{\isasymUnion}\isactrlbsub {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\isactrlesub \ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
    37 \end{quote}
    38 The intuitive meanings of these expressions should be obvious.
    39 Unfortunately, we need to know in more detail what the notation really stands
    40 for once we have to reason about it.  Abstraction
    41 over pairs and tuples is merely a convenient shorthand for a more complex
    42 internal representation.  Thus the internal and external form of a term may
    43 differ, which can affect proofs. If you want to avoid this complication,
    44 stick to \isa{fst} and \isa{snd} and write \isa{{\isasymlambda}p{\isachardot}\ fst\ p\ {\isacharplus}\ snd\ p}
    45 instead of \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharplus}y}.  These terms are distinct even though they
    46 denote the same function.
    47 
    48 Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
    49 \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
    50 \begin{center}
    51 \isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
    52 \hfill(\isa{split{\isacharunderscore}def})
    53 \end{center}
    54 Pattern matching in
    55 other variable binding constructs is translated similarly. Thus we need to
    56 understand how to reason about such constructs.%
    57 \end{isamarkuptext}%
    58 \isamarkuptrue%
    59 %
    60 \isamarkupsubsection{Theorem Proving%
    61 }
    62 \isamarkuptrue%
    63 %
    64 \begin{isamarkuptext}%
    65 The most obvious approach is the brute force expansion of \isa{split}:%
    66 \end{isamarkuptext}%
    67 \isamarkuptrue%
    68 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline
    69 \isamarkupfalse%
    70 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
    71 %
    72 \begin{isamarkuptext}%
    73 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
    74 proof, as it does above.  But if it does not, you end up with exactly what
    75 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
    76 approach is neither elegant nor very practical in large examples, although it
    77 can be effective in small ones.
    78 
    79 If we consider why this lemma presents a problem, 
    80 we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}.  Then both sides of the
    81 equation would simplify to \isa{a} by the simplification rules
    82 \isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.  
    83 To reason about tuple patterns requires some way of
    84 converting a variable of product type into a pair.
    85 
    86 In case of a subterm of the form \isa{split\ f\ p} this is easy: the split
    87 rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:%
    88 \index{*split (method)}%
    89 \end{isamarkuptext}%
    90 \isamarkuptrue%
    91 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
    92 \isamarkupfalse%
    93 \isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
    94 %
    95 \begin{isamarkuptxt}%
    96 \begin{isabelle}%
    97 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p%
    98 \end{isabelle}
    99 This subgoal is easily proved by simplification. Thus we could have combined
   100 simplification and splitting in one command that proves the goal outright:%
   101 \end{isamarkuptxt}%
   102 \isamarkuptrue%
   103 \isamarkupfalse%
   104 \isamarkupfalse%
   105 \isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
   106 %
   107 \begin{isamarkuptext}%
   108 Let us look at a second example:%
   109 \end{isamarkuptext}%
   110 \isamarkuptrue%
   111 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline
   112 \isamarkupfalse%
   113 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
   114 %
   115 \begin{isamarkuptxt}%
   116 \begin{isabelle}%
   117 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p%
   118 \end{isabelle}
   119 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which
   120 can be split as above. The same is true for paired set comprehension:%
   121 \end{isamarkuptxt}%
   122 \isamarkuptrue%
   123 \isamarkupfalse%
   124 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
   125 \isamarkupfalse%
   126 \isacommand{apply}\ simp\isamarkupfalse%
   127 %
   128 \begin{isamarkuptxt}%
   129 \begin{isabelle}%
   130 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p%
   131 \end{isabelle}
   132 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
   133 as above. If you are worried about the strange form of the premise:
   134 \isa{split\ op\ {\isacharequal}} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
   135 The same proof procedure works for%
   136 \end{isamarkuptxt}%
   137 \isamarkuptrue%
   138 \isamarkupfalse%
   139 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%
   140 %
   141 \begin{isamarkuptxt}%
   142 \noindent
   143 except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because
   144 \isa{split} occurs in the assumptions.
   145 
   146 However, splitting \isa{split} is not always a solution, as no \isa{split}
   147 may be present in the goal. Consider the following function:%
   148 \end{isamarkuptxt}%
   149 \isamarkuptrue%
   150 \isamarkupfalse%
   151 \isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline
   152 \isamarkupfalse%
   153 \isacommand{primrec}\isanewline
   154 \ \ {\isachardoublequote}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
   155 %
   156 \begin{isamarkuptext}%
   157 \noindent
   158 Note that the above \isacommand{primrec} definition is admissible
   159 because \isa{{\isasymtimes}} is a datatype. When we now try to prove%
   160 \end{isamarkuptext}%
   161 \isamarkuptrue%
   162 \isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}\isamarkupfalse%
   163 %
   164 \begin{isamarkuptxt}%
   165 \noindent
   166 simplification will do nothing, because the defining equation for \isa{swap}
   167 expects a pair. Again, we need to turn \isa{p} into a pair first, but this
   168 time there is no \isa{split} in sight. In this case the only thing we can do
   169 is to split the term by hand:%
   170 \end{isamarkuptxt}%
   171 \isamarkuptrue%
   172 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}\isamarkupfalse%
   173 %
   174 \begin{isamarkuptxt}%
   175 \noindent
   176 \begin{isabelle}%
   177 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ swap\ {\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p%
   178 \end{isabelle}
   179 Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype.
   180 The subgoal is easily proved by \isa{simp}.
   181 
   182 Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus
   183 appear preferable to the more arcane methods introduced first. However, see
   184 the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}.
   185 
   186 In case the term to be split is a quantified variable, there are more options.
   187 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal
   188 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
   189 \end{isamarkuptxt}%
   190 \isamarkuptrue%
   191 \isamarkupfalse%
   192 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
   193 \isamarkupfalse%
   194 \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
   195 %
   196 \begin{isamarkuptxt}%
   197 \noindent
   198 \begin{isabelle}%
   199 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline
   200 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}%
   201 \end{isabelle}%
   202 \end{isamarkuptxt}%
   203 \isamarkuptrue%
   204 \isacommand{apply}\ simp\isanewline
   205 \isamarkupfalse%
   206 \isacommand{done}\isamarkupfalse%
   207 %
   208 \begin{isamarkuptext}%
   209 \noindent
   210 Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all}
   211 in the first simplification step, and then we simplify again. 
   212 This time the reason was not merely
   213 pedagogical:
   214 \isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with other functions
   215 of the simplifier.
   216 The following command could fail (here it does not)
   217 where two separate \isa{simp} applications succeed.%
   218 \end{isamarkuptext}%
   219 \isamarkuptrue%
   220 \isamarkupfalse%
   221 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
   222 \isamarkupfalse%
   223 %
   224 \begin{isamarkuptext}%
   225 \noindent
   226 Finally, the simplifier automatically splits all \isa{{\isasymforall}} and
   227 \isa{{\isasymexists}}-quantified variables:%
   228 \end{isamarkuptext}%
   229 \isamarkuptrue%
   230 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline
   231 \isamarkupfalse%
   232 \isacommand{by}\ simp\isamarkupfalse%
   233 %
   234 \begin{isamarkuptext}%
   235 \noindent
   236 To turn off this automatic splitting, just disable the
   237 responsible simplification rules:
   238 \begin{center}
   239 \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   240 \hfill
   241 (\isa{split{\isacharunderscore}paired{\isacharunderscore}All})\\
   242 \isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
   243 \hfill
   244 (\isa{split{\isacharunderscore}paired{\isacharunderscore}Ex})
   245 \end{center}%
   246 \end{isamarkuptext}%
   247 \isamarkuptrue%
   248 \isamarkupfalse%
   249 \end{isabellebody}%
   250 %%% Local Variables:
   251 %%% mode: latex
   252 %%% TeX-master: "root"
   253 %%% End: