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