10560
|
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 |
%
|
10608
|
18 |
\isamarkupsubsection{Pattern matching with tuples%
|
10560
|
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
|
10654
|
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
|
10560
|
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
|
10654
|
84 |
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}%
|
10560
|
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}%
|
10577
|
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}%
|
10560
|
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}
|
10654
|
188 |
\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
|
10560
|
189 |
\hfill
|
|
190 |
(\isa{split{\isacharunderscore}paired{\isacharunderscore}All})\\
|
10654
|
191 |
\isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
|
10560
|
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:
|