author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
27170 | 1 |
(*<*)theory Pairs imports Main begin(*>*) |
10560 | 2 |
|
67406 | 3 |
section\<open>Pairs and Tuples\<close> |
10560 | 4 |
|
67406 | 5 |
text\<open>\label{sec:products} |
11428 | 6 |
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal |
69597 | 7 |
repertoire of operations: pairing and the two projections \<^term>\<open>fst\<close> and |
8 |
\<^term>\<open>snd\<close>. 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. |
67406 | 12 |
\<close> |
10560 | 13 |
|
67406 | 14 |
subsection\<open>Pattern Matching with Tuples\<close> |
10560 | 15 |
|
67406 | 16 |
text\<open> |
10885 | 17 |
Tuples may be used as patterns in $\lambda$-abstractions, |
69505 | 18 |
for example \<open>\<lambda>(x,y,z).x+y+z\<close> and \<open>\<lambda>((x,y),z).x+y+z\<close>. 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} |
|
69597 | 23 |
\<^term>\<open>let (x,y) = f z in (y,x)\<close>\\ |
24 |
\<^term>\<open>case xs of [] => (0::nat) | (x,y)#zs => x+y\<close>\\ |
|
69505 | 25 |
\<open>\<forall>(x,y)\<in>A. x=y\<close>\\ |
26 |
\<open>{(x,y,z). x=z}\<close>\\ |
|
69597 | 27 |
\<^term>\<open>\<Union>(x,y)\<in>A. {x+y}\<close> |
10560 | 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, |
|
69597 | 35 |
stick to \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close> and write \<^term>\<open>%p. fst p + snd p\<close> |
69505 | 36 |
instead of \<open>\<lambda>(x,y). x+y\<close>. These terms are distinct even though they |
11494 | 37 |
denote the same function. |
10560 | 38 |
|
69597 | 39 |
Internally, \<^term>\<open>%(x,y). t\<close> becomes \<open>case_prod (\<lambda>x y. t)\<close>, where |
69505 | 40 |
\cdx{split} is the uncurrying function of type \<open>('a \<Rightarrow> 'b |
41 |
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c\<close> defined as |
|
10560 | 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. |
|
67406 | 49 |
\<close> |
10560 | 50 |
|
67406 | 51 |
subsection\<open>Theorem Proving\<close> |
10560 | 52 |
|
67406 | 53 |
text\<open> |
69597 | 54 |
The most obvious approach is the brute force expansion of \<^term>\<open>split\<close>: |
67406 | 55 |
\<close> |
10560 | 56 |
|
57 |
lemma "(\<lambda>(x,y).x) p = fst p" |
|
12815 | 58 |
by(simp add: split_def) |
10560 | 59 |
|
67406 | 60 |
text\<open>\noindent |
27027 | 61 |
This works well if rewriting with @{thm[source]split_def} finishes the |
11149 | 62 |
proof, as it does above. But if it does not, you end up with exactly what |
69597 | 63 |
we are trying to avoid: nests of \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>. Thus this |
10560 | 64 |
approach is neither elegant nor very practical in large examples, although it |
65 |
can be effective in small ones. |
|
66 |
||
11494 | 67 |
If we consider why this lemma presents a problem, |
69597 | 68 |
we realize that we need to replace variable~\<^term>\<open>p\<close> by some pair \<^term>\<open>(a,b)\<close>. Then both sides of the |
69 |
equation would simplify to \<^term>\<open>a\<close> by the simplification rules |
|
11494 | 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. |
|
69597 | 73 |
In case of a subterm of the form \<^term>\<open>case_prod f p\<close> this is easy: the split |
74 |
rule @{thm[source]prod.split} replaces \<^term>\<open>p\<close> by a pair:% |
|
11494 | 75 |
\index{*split (method)} |
67406 | 76 |
\<close> |
10560 | 77 |
|
78 |
lemma "(\<lambda>(x,y).y) p = snd p" |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
79 |
apply(split prod.split) |
10560 | 80 |
|
67406 | 81 |
txt\<open> |
10560 | 82 |
@{subgoals[display,indent=0]} |
10824 | 83 |
This subgoal is easily proved by simplification. Thus we could have combined |
84 |
simplification and splitting in one command that proves the goal outright: |
|
67406 | 85 |
\<close> |
10824 | 86 |
(*<*) |
87 |
by simp |
|
88 |
lemma "(\<lambda>(x,y).y) p = snd p"(*>*) |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
89 |
by(simp split: prod.split) |
10560 | 90 |
|
67406 | 91 |
text\<open> |
10560 | 92 |
Let us look at a second example: |
67406 | 93 |
\<close> |
10560 | 94 |
|
58860 | 95 |
lemma "let (x,y) = p in fst p = x" |
10824 | 96 |
apply(simp only: Let_def) |
10560 | 97 |
|
67406 | 98 |
txt\<open> |
10560 | 99 |
@{subgoals[display,indent=0]} |
69505 | 100 |
A paired \<open>let\<close> reduces to a paired $\lambda$-abstraction, which |
10560 | 101 |
can be split as above. The same is true for paired set comprehension: |
67406 | 102 |
\<close> |
10560 | 103 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
104 |
(*<*)by(simp split: prod.split)(*>*) |
10560 | 105 |
lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p" |
106 |
apply simp |
|
107 |
||
67406 | 108 |
txt\<open> |
10560 | 109 |
@{subgoals[display,indent=0]} |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
110 |
Again, simplification produces a term suitable for @{thm[source]prod.split} |
11277 | 111 |
as above. If you are worried about the strange form of the premise: |
69597 | 112 |
\<open>case_prod (=)\<close> is short for \<^term>\<open>\<lambda>(x,y). x=y\<close>. |
11277 | 113 |
The same proof procedure works for |
67406 | 114 |
\<close> |
10560 | 115 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
116 |
(*<*)by(simp split: prod.split)(*>*) |
10560 | 117 |
lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p" |
118 |
||
67406 | 119 |
txt\<open>\noindent |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
120 |
except that we now have to use @{thm[source]prod.split_asm}, because |
69597 | 121 |
\<^term>\<open>split\<close> occurs in the assumptions. |
10560 | 122 |
|
69597 | 123 |
However, splitting \<^term>\<open>split\<close> is not always a solution, as no \<^term>\<open>split\<close> |
10560 | 124 |
may be present in the goal. Consider the following function: |
67406 | 125 |
\<close> |
10560 | 126 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
58860
diff
changeset
|
127 |
(*<*)by(simp split: prod.split_asm)(*>*) |
27027 | 128 |
primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" where "swap (x,y) = (y,x)" |
10560 | 129 |
|
67406 | 130 |
text\<open>\noindent |
10560 | 131 |
Note that the above \isacommand{primrec} definition is admissible |
69505 | 132 |
because \<open>\<times>\<close> is a datatype. When we now try to prove |
67406 | 133 |
\<close> |
10560 | 134 |
|
135 |
lemma "swap(swap p) = p" |
|
136 |
||
67406 | 137 |
txt\<open>\noindent |
27027 | 138 |
simplification will do nothing, because the defining equation for |
69597 | 139 |
@{const[source] swap} expects a pair. Again, we need to turn \<^term>\<open>p\<close> |
140 |
into a pair first, but this time there is no \<^term>\<open>split\<close> in sight. |
|
27027 | 141 |
The only thing we can do is to split the term by hand: |
67406 | 142 |
\<close> |
10560 | 143 |
apply(case_tac p) |
144 |
||
67406 | 145 |
txt\<open>\noindent |
10560 | 146 |
@{subgoals[display,indent=0]} |
69505 | 147 |
Again, \methdx{case_tac} is applicable because \<open>\<times>\<close> is a datatype. |
148 |
The subgoal is easily proved by \<open>simp\<close>. |
|
10560 | 149 |
|
69505 | 150 |
Splitting by \<open>case_tac\<close> also solves the previous examples and may thus |
10824 | 151 |
appear preferable to the more arcane methods introduced first. However, see |
69505 | 152 |
the warning about \<open>case_tac\<close> in \S\ref{sec:struct-ind-case}. |
10824 | 153 |
|
69505 | 154 |
Alternatively, you can split \emph{all} \<open>\<And>\<close>-quantified variables |
27027 | 155 |
in a goal with the rewrite rule @{thm[source]split_paired_all}: |
67406 | 156 |
\<close> |
10560 | 157 |
|
158 |
(*<*)by simp(*>*) |
|
159 |
lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q" |
|
12631 | 160 |
apply(simp only: split_paired_all) |
10560 | 161 |
|
67406 | 162 |
txt\<open>\noindent |
27027 | 163 |
@{subgoals[display,indent=0,margin=70]} |
67406 | 164 |
\<close> |
10560 | 165 |
|
166 |
apply simp |
|
167 |
done |
|
168 |
||
67406 | 169 |
text\<open>\noindent |
10560 | 170 |
Note that we have intentionally included only @{thm[source]split_paired_all} |
11494 | 171 |
in the first simplification step, and then we simplify again. |
172 |
This time the reason was not merely |
|
10560 | 173 |
pedagogical: |
11494 | 174 |
@{thm[source]split_paired_all} may interfere with other functions |
175 |
of the simplifier. |
|
176 |
The following command could fail (here it does not) |
|
177 |
where two separate \isa{simp} applications succeed. |
|
67406 | 178 |
\<close> |
10560 | 179 |
|
180 |
(*<*) |
|
181 |
lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q" |
|
182 |
(*>*) |
|
12815 | 183 |
apply(simp add: split_paired_all) |
10560 | 184 |
(*<*)done(*>*) |
67406 | 185 |
text\<open>\noindent |
69505 | 186 |
Finally, the simplifier automatically splits all \<open>\<forall>\<close> and |
187 |
\<open>\<exists>\<close>-quantified variables: |
|
67406 | 188 |
\<close> |
10560 | 189 |
|
190 |
lemma "\<forall>p. \<exists>q. swap p = swap q" |
|
58860 | 191 |
by simp |
10560 | 192 |
|
67406 | 193 |
text\<open>\noindent |
27027 | 194 |
To turn off this automatic splitting, disable the |
10560 | 195 |
responsible simplification rules: |
196 |
\begin{center} |
|
10654 | 197 |
@{thm split_paired_All[no_vars]} |
10560 | 198 |
\hfill |
199 |
(@{thm[source]split_paired_All})\\ |
|
10654 | 200 |
@{thm split_paired_Ex[no_vars]} |
10560 | 201 |
\hfill |
202 |
(@{thm[source]split_paired_Ex}) |
|
203 |
\end{center} |
|
67406 | 204 |
\<close> |
10560 | 205 |
(*<*) |
206 |
end |
|
207 |
(*>*) |