10560
|
1 |
(*<*)theory Pairs = Main:(*>*)
|
|
2 |
|
11428
|
3 |
section{*Pairs and Tuples*}
|
10560
|
4 |
|
|
5 |
text{*\label{sec:products}
|
11428
|
6 |
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
|
10560
|
7 |
repertoire of operations: pairing and the two projections @{term fst} and
|
11149
|
8 |
@{term snd}. In any non-trivial application of pairs you will find that this
|
11494
|
9 |
quickly leads to unreadable nests of projections. This
|
|
10 |
section introduces syntactic sugar to overcome this
|
10560
|
11 |
problem: pattern matching with tuples.
|
|
12 |
*}
|
|
13 |
|
10885
|
14 |
subsection{*Pattern Matching with Tuples*}
|
10560
|
15 |
|
|
16 |
text{*
|
10885
|
17 |
Tuples may be used as patterns in $\lambda$-abstractions,
|
10560
|
18 |
for example @{text"\<lambda>(x,y,z).x+y+z"} and @{text"\<lambda>((x,y),z).x+y+z"}. In fact,
|
10885
|
19 |
tuple patterns can be used in most variable binding constructs,
|
|
20 |
and they can be nested. Here are
|
10560
|
21 |
some typical examples:
|
|
22 |
\begin{quote}
|
|
23 |
@{term"let (x,y) = f z in (y,x)"}\\
|
12699
|
24 |
@{term"case xs of [] => (0::nat) | (x,y)#zs => x+y"}\\
|
10560
|
25 |
@{text"\<forall>(x,y)\<in>A. x=y"}\\
|
10885
|
26 |
@{text"{(x,y,z). x=z}"}\\
|
10560
|
27 |
@{term"\<Union>(x,y)\<in>A. {x+y}"}
|
|
28 |
\end{quote}
|
10885
|
29 |
The intuitive meanings of these expressions should be obvious.
|
10560
|
30 |
Unfortunately, we need to know in more detail what the notation really stands
|
10885
|
31 |
for once we have to reason about it. Abstraction
|
10560
|
32 |
over pairs and tuples is merely a convenient shorthand for a more complex
|
|
33 |
internal representation. Thus the internal and external form of a term may
|
|
34 |
differ, which can affect proofs. If you want to avoid this complication,
|
|
35 |
stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"}
|
11494
|
36 |
instead of @{text"\<lambda>(x,y). x+y"}. These terms are distinct even though they
|
|
37 |
denote the same function.
|
10560
|
38 |
|
|
39 |
Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
|
11494
|
40 |
\cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
|
10560
|
41 |
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
|
|
42 |
\begin{center}
|
|
43 |
@{thm split_def}
|
|
44 |
\hfill(@{thm[source]split_def})
|
|
45 |
\end{center}
|
|
46 |
Pattern matching in
|
|
47 |
other variable binding constructs is translated similarly. Thus we need to
|
|
48 |
understand how to reason about such constructs.
|
|
49 |
*}
|
|
50 |
|
10885
|
51 |
subsection{*Theorem Proving*}
|
10560
|
52 |
|
|
53 |
text{*
|
|
54 |
The most obvious approach is the brute force expansion of @{term split}:
|
|
55 |
*}
|
|
56 |
|
|
57 |
lemma "(\<lambda>(x,y).x) p = fst p"
|
12815
|
58 |
by(simp add: split_def)
|
10560
|
59 |
|
|
60 |
text{* This works well if rewriting with @{thm[source]split_def} finishes the
|
11149
|
61 |
proof, as it does above. But if it does not, you end up with exactly what
|
10560
|
62 |
we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
|
|
63 |
approach is neither elegant nor very practical in large examples, although it
|
|
64 |
can be effective in small ones.
|
|
65 |
|
11494
|
66 |
If we consider why this lemma presents a problem,
|
|
67 |
we quickly realize that we need to replace the variable~@{term
|
|
68 |
p} by some pair @{term"(a,b)"}. Then both sides of the
|
|
69 |
equation would simplify to @{term a} by the simplification rules
|
|
70 |
@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.
|
|
71 |
To reason about tuple patterns requires some way of
|
|
72 |
converting a variable of product type into a pair.
|
10560
|
73 |
|
|
74 |
In case of a subterm of the form @{term"split f p"} this is easy: the split
|
11494
|
75 |
rule @{thm[source]split_split} replaces @{term p} by a pair:%
|
|
76 |
\index{*split (method)}
|
10560
|
77 |
*}
|
|
78 |
|
|
79 |
lemma "(\<lambda>(x,y).y) p = snd p"
|
10654
|
80 |
apply(split split_split);
|
10560
|
81 |
|
|
82 |
txt{*
|
|
83 |
@{subgoals[display,indent=0]}
|
10824
|
84 |
This subgoal is easily proved by simplification. Thus we could have combined
|
|
85 |
simplification and splitting in one command that proves the goal outright:
|
|
86 |
*}
|
|
87 |
(*<*)
|
|
88 |
by simp
|
|
89 |
lemma "(\<lambda>(x,y).y) p = snd p"(*>*)
|
|
90 |
by(simp split: split_split)
|
10560
|
91 |
|
10824
|
92 |
text{*
|
10560
|
93 |
Let us look at a second example:
|
|
94 |
*}
|
|
95 |
|
|
96 |
lemma "let (x,y) = p in fst p = x";
|
10824
|
97 |
apply(simp only: Let_def)
|
10560
|
98 |
|
|
99 |
txt{*
|
|
100 |
@{subgoals[display,indent=0]}
|
|
101 |
A paired @{text let} reduces to a paired $\lambda$-abstraction, which
|
|
102 |
can be split as above. The same is true for paired set comprehension:
|
|
103 |
*}
|
|
104 |
|
12815
|
105 |
(*<*)by(simp split: split_split)(*>*)
|
10560
|
106 |
lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
|
|
107 |
apply simp
|
|
108 |
|
|
109 |
txt{*
|
|
110 |
@{subgoals[display,indent=0]}
|
|
111 |
Again, simplification produces a term suitable for @{thm[source]split_split}
|
11277
|
112 |
as above. If you are worried about the strange form of the premise:
|
|
113 |
@{term"split (op =)"} is short for @{text"\<lambda>(x,y). x=y"}.
|
|
114 |
The same proof procedure works for
|
10560
|
115 |
*}
|
|
116 |
|
12815
|
117 |
(*<*)by(simp split: split_split)(*>*)
|
10560
|
118 |
lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
|
|
119 |
|
|
120 |
txt{*\noindent
|
|
121 |
except that we now have to use @{thm[source]split_split_asm}, because
|
|
122 |
@{term split} occurs in the assumptions.
|
|
123 |
|
|
124 |
However, splitting @{term split} is not always a solution, as no @{term split}
|
|
125 |
may be present in the goal. Consider the following function:
|
|
126 |
*}
|
|
127 |
|
12815
|
128 |
(*<*)by(simp split: split_split_asm)(*>*)
|
10560
|
129 |
consts swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
|
|
130 |
primrec
|
|
131 |
"swap (x,y) = (y,x)"
|
|
132 |
|
|
133 |
text{*\noindent
|
|
134 |
Note that the above \isacommand{primrec} definition is admissible
|
|
135 |
because @{text"\<times>"} is a datatype. When we now try to prove
|
|
136 |
*}
|
|
137 |
|
|
138 |
lemma "swap(swap p) = p"
|
|
139 |
|
|
140 |
txt{*\noindent
|
|
141 |
simplification will do nothing, because the defining equation for @{term swap}
|
|
142 |
expects a pair. Again, we need to turn @{term p} into a pair first, but this
|
|
143 |
time there is no @{term split} in sight. In this case the only thing we can do
|
|
144 |
is to split the term by hand:
|
|
145 |
*}
|
|
146 |
apply(case_tac p)
|
|
147 |
|
|
148 |
txt{*\noindent
|
|
149 |
@{subgoals[display,indent=0]}
|
11494
|
150 |
Again, \methdx{case_tac} is applicable because @{text"\<times>"} is a datatype.
|
10560
|
151 |
The subgoal is easily proved by @{text simp}.
|
|
152 |
|
10824
|
153 |
Splitting by @{text case_tac} also solves the previous examples and may thus
|
|
154 |
appear preferable to the more arcane methods introduced first. However, see
|
|
155 |
the warning about @{text case_tac} in \S\ref{sec:struct-ind-case}.
|
|
156 |
|
10560
|
157 |
In case the term to be split is a quantified variable, there are more options.
|
|
158 |
You can split \emph{all} @{text"\<And>"}-quantified variables in a goal
|
|
159 |
with the rewrite rule @{thm[source]split_paired_all}:
|
|
160 |
*}
|
|
161 |
|
|
162 |
(*<*)by simp(*>*)
|
|
163 |
lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
|
12631
|
164 |
apply(simp only: split_paired_all)
|
10560
|
165 |
|
|
166 |
txt{*\noindent
|
|
167 |
@{subgoals[display,indent=0]}
|
|
168 |
*}
|
|
169 |
|
|
170 |
apply simp
|
|
171 |
done
|
|
172 |
|
|
173 |
text{*\noindent
|
|
174 |
Note that we have intentionally included only @{thm[source]split_paired_all}
|
11494
|
175 |
in the first simplification step, and then we simplify again.
|
|
176 |
This time the reason was not merely
|
10560
|
177 |
pedagogical:
|
11494
|
178 |
@{thm[source]split_paired_all} may interfere with other functions
|
|
179 |
of the simplifier.
|
|
180 |
The following command could fail (here it does not)
|
|
181 |
where two separate \isa{simp} applications succeed.
|
10560
|
182 |
*}
|
|
183 |
|
|
184 |
(*<*)
|
|
185 |
lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
|
|
186 |
(*>*)
|
12815
|
187 |
apply(simp add: split_paired_all)
|
10560
|
188 |
(*<*)done(*>*)
|
|
189 |
text{*\noindent
|
11494
|
190 |
Finally, the simplifier automatically splits all @{text"\<forall>"} and
|
|
191 |
@{text"\<exists>"}-quantified variables:
|
10560
|
192 |
*}
|
|
193 |
|
|
194 |
lemma "\<forall>p. \<exists>q. swap p = swap q"
|
11494
|
195 |
by simp;
|
10560
|
196 |
|
|
197 |
text{*\noindent
|
11494
|
198 |
To turn off this automatic splitting, just disable the
|
10560
|
199 |
responsible simplification rules:
|
|
200 |
\begin{center}
|
10654
|
201 |
@{thm split_paired_All[no_vars]}
|
10560
|
202 |
\hfill
|
|
203 |
(@{thm[source]split_paired_All})\\
|
10654
|
204 |
@{thm split_paired_Ex[no_vars]}
|
10560
|
205 |
\hfill
|
|
206 |
(@{thm[source]split_paired_Ex})
|
|
207 |
\end{center}
|
|
208 |
*}
|
|
209 |
(*<*)
|
|
210 |
end
|
|
211 |
(*>*)
|