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