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