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