author | wenzelm |
Mon, 19 Nov 2001 20:46:05 +0100 | |
changeset 12240 | 0760eda193c4 |
parent 12156 | d2758965362e |
child 12407 | 70ebb59264f1 |
permissions | -rw-r--r-- |
11388 | 1 |
\section{Records} |
2 |
\label{sec:records} |
|
3 |
||
11427 | 4 |
\index{records|(}% |
11388 | 5 |
Records are familiar from programming languages. A record of $n$ |
6 |
fields is essentially an $n$-tuple, but the record's components have |
|
7 |
names, which can make expressions easier to read and reduces the risk |
|
8 |
of confusing one field for another. |
|
9 |
||
10 |
A basic Isabelle record has a fixed set of fields, with access |
|
11 |
and update operations. Each field has a specified type, which may be |
|
12 |
polymorphic. The field names are part of the record type, and the |
|
13 |
order of the fields is significant --- as it is in Pascal but not in |
|
14 |
Standard ML. If two different record types have fields in common, |
|
15 |
then the ambiguity is resolved in the usual way, by qualified names. |
|
16 |
||
17 |
Record types can also be defined by extending other record types. |
|
11427 | 18 |
Extensible records make use of the reserved field \cdx{more}, which is |
11388 | 19 |
present in every record type. Generic methods, or operations that |
20 |
work on all possible extensions of a given record, can be expressed by |
|
21 |
definitions involving \isa{more}, but the details are complicated. |
|
22 |
||
23 |
\subsection{Record Basics} |
|
24 |
||
25 |
Record types are not primitive in Isabelle and have a complex internal |
|
11427 | 26 |
representation. A \commdx{record} declaration |
11388 | 27 |
introduces a new record type: |
28 |
\begin{isabelle} |
|
29 |
\isacommand{record}\ point\ =\isanewline |
|
30 |
\ \ Xcoord\ ::\ int\isanewline |
|
31 |
\ \ Ycoord\ ::\ int |
|
32 |
\end{isabelle} |
|
33 |
||
34 |
Records of type \isa{point} have two fields named \isa{Xcoord} and \isa{Ycoord}, |
|
35 |
both of type~\isa{int}. We now declare a constant of type |
|
36 |
\isa{point}: |
|
37 |
\begin{isabelle} |
|
38 |
\isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
39 |
\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)" |
11388 | 40 |
\end{isabelle} |
41 |
We see above the ASCII notation for record brackets. You can also use |
|
42 |
the symbolic brackets \isa{\isasymlparr} and \isa{\isasymrparr}. |
|
43 |
Record types can be written directly, rather than referring to |
|
44 |
previously declared names: |
|
45 |
\begin{isabelle} |
|
46 |
\isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\ |
|
47 |
|)"\ \isanewline |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
48 |
\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)" |
11388 | 49 |
\end{isabelle} |
50 |
||
51 |
For each field, there is a \emph{selector} function of the same name. For |
|
52 |
example, if \isa{p} has type \isa{point} then \isa{Xcoord p} denotes the |
|
53 |
value of the \isa{Xcoord} field of~\isa{p}. Expressions involving field |
|
54 |
selection are simplified automatically: |
|
55 |
\begin{isabelle} |
|
56 |
\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ =\ a"\isanewline |
|
57 |
\isacommand{by}\ simp |
|
58 |
\end{isabelle} |
|
59 |
The \emph{update} operation is functional. For example, |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
60 |
\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value |
11388 | 61 |
is zero and whose |
62 |
\isa{Ycoord} value is copied from~\isa{p}. Updates are also simplified |
|
63 |
automatically: |
|
64 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
65 |
\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\ |
11388 | 66 |
=\isanewline |
67 |
\ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline |
|
68 |
\isacommand{by}\ simp |
|
69 |
\end{isabelle} |
|
70 |
||
71 |
\begin{warn} |
|
72 |
Field names are declared as constants and can no longer be |
|
73 |
used as variables. It would be unwise, for example, to call the fields |
|
11427 | 74 |
of type \isa{point} simply \isa{x} and~\isa{y}. Each record |
75 |
declaration introduces a constant \cdx{more}. |
|
11388 | 76 |
\end{warn} |
77 |
||
78 |
||
79 |
\subsection{Extensible Records and Generic Operations} |
|
80 |
||
11427 | 81 |
\index{records!extensible|(}% |
11388 | 82 |
Now, let us define coloured points |
83 |
(type \isa{cpoint}) to be points extended with a field \isa{col} of type |
|
84 |
\isa{colour}: |
|
85 |
\begin{isabelle} |
|
86 |
\isacommand{datatype}\ colour\ =\ Red\ |\ Green\ |\ |
|
87 |
Blue\isanewline |
|
88 |
\isanewline |
|
89 |
\isacommand{record}\ cpoint\ =\ point\ +\isanewline |
|
90 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ col\ ::\ colour |
|
91 |
\end{isabelle} |
|
92 |
||
93 |
The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and \isa{col}, in that |
|
94 |
order: |
|
95 |
\begin{isabelle} |
|
96 |
\isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
97 |
\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\ |
11388 | 98 |
=\ Green\ |)" |
99 |
\end{isabelle} |
|
100 |
||
101 |
Unfortunately, there are no built-in conversions between types |
|
102 |
\isa{point} and \isa{cpoint}: to add a colour to |
|
103 |
a point, or to convert a \isa{cpoint} to a \isa{point} by forgetting |
|
104 |
its colour, we must define operations that copy across the other |
|
105 |
fields. However, we can define generic operations |
|
106 |
that work on type |
|
107 |
\isa{point} and all extensions of it. |
|
108 |
||
11427 | 109 |
Every record structure has an implicit field, \cdx{more}, to allow |
11388 | 110 |
extension. Its type is completely polymorphic:~\isa{'a}. When a |
111 |
record value is expressed using just its standard fields, the value of |
|
112 |
\isa{more} is implicitly set to \isa{()}, the empty tuple, which has |
|
113 |
type \isa{unit}. Within the record brackets, you can refer to the |
|
11427 | 114 |
\isa{more} field by writing \isa{...} (three periods): |
11388 | 115 |
\begin{isabelle} |
116 |
\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b,\ ...\ =\ p\ |)\ =\ a" |
|
117 |
\end{isabelle} |
|
118 |
This lemma (trivially proved using \isa{simp}) applies to any |
|
119 |
record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Field |
|
120 |
\isa{more} can be selected in the usual way, but as all records share |
|
121 |
this field, the identifier must be qualified: |
|
122 |
\begin{isabelle} |
|
123 |
\isacommand{lemma}\ "point.more\ cpt1\ =\ \isasymlparr col\ =\ Green\isasymrparr "\isanewline |
|
124 |
\isacommand{by}\ (simp\ add:\ cpt1_def) |
|
125 |
\end{isabelle} |
|
126 |
% |
|
127 |
We see that the colour attached to this \isa{point} is a record in its |
|
128 |
own right, namely |
|
129 |
\isa{\isasymlparr col\ =\ Green\isasymrparr}. |
|
130 |
||
131 |
To define generic operations, we need to know a bit more about records. |
|
132 |
Our declaration of \isa{point} above generated two type |
|
133 |
abbreviations: |
|
134 |
\begin{isabelle} |
|
135 |
\ \ \ \ point\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\ |)\isanewline |
|
136 |
\ \ \ \ 'a\ point_scheme\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int,\ ...\ ::\ 'a\ |) |
|
137 |
\end{isabelle} |
|
138 |
% |
|
139 |
Type \isa{point} is for rigid records having the two fields |
|
140 |
\isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{'a\ point_scheme} |
|
141 |
comprises all possible extensions to those two fields. For example, |
|
11427 | 142 |
let us define two operations --- methods, if we regard records as |
143 |
objects --- to get and set any point's |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
144 |
\isa{Xcoord} field. |
11388 | 145 |
\begin{isabelle} |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
146 |
\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline |
11388 | 147 |
\ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline |
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
148 |
\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline |
11388 | 149 |
\ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)" |
150 |
\end{isabelle} |
|
151 |
||
152 |
Here is a generic method that modifies a point, incrementing its |
|
153 |
\isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields |
|
154 |
are copied across. It works for type \isa{point} and any of its |
|
155 |
extensions, such as \isa{cpoint}: |
|
156 |
\begin{isabelle} |
|
157 |
\isacommand{constdefs}\isanewline |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
158 |
\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline |
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
159 |
\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline |
11388 | 160 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline |
161 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\ |
|
162 |
r\isasymrparr" |
|
163 |
\end{isabelle} |
|
164 |
||
165 |
Generic theorems can be proved about generic methods. This trivial |
|
166 |
lemma relates \isa{incX} to \isa{getX} and \isa{setX}: |
|
167 |
\begin{isabelle} |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11427
diff
changeset
|
168 |
\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline |
11388 | 169 |
\isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def) |
170 |
\end{isabelle} |
|
171 |
||
172 |
\begin{warn} |
|
173 |
If you use the symbolic record brackets \isa{\isasymlparr} and |
|
174 |
\isa{\isasymrparr}, then you must also use the symbolic ellipsis, |
|
175 |
\isa{\isasymdots}, rather than three consecutive periods, |
|
176 |
\isa{...}. Mixing the ASCII and symbolic versions |
|
177 |
causes a syntax error. (The two versions are more |
|
178 |
distinct on screen than they are on paper.) |
|
11427 | 179 |
\end{warn}% |
180 |
\index{records!extensible|)} |
|
11388 | 181 |
|
182 |
||
183 |
\subsection{Record Equality} |
|
184 |
||
11427 | 185 |
Two records are equal\index{equality!of records} |
186 |
if all pairs of corresponding fields are equal. |
|
11388 | 187 |
Record equalities are simplified automatically: |
188 |
\begin{isabelle} |
|
189 |
\isacommand{lemma}\ "(\isasymlparr Xcoord\ =\ a,\ Ycoord\ =\ b\isasymrparr \ =\ \isasymlparr Xcoord\ =\ a',\ Ycoord\ =\ b'\isasymrparr )\ |
|
190 |
=\isanewline |
|
191 |
\ \ \ \ \ \ \ \ (a\ =\ a'\ \&\ b\ =\ b')"\isanewline |
|
192 |
\isacommand{by}\ simp |
|
193 |
\end{isabelle} |
|
194 |
||
195 |
The following equality is similar, but generic, in that \isa{r} can |
|
196 |
be any instance of \isa{point_scheme}: |
|
197 |
\begin{isabelle} |
|
198 |
\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a,\ Ycoord\ :=\ |
|
199 |
b\isasymrparr \ =\ r\ \isasymlparr Ycoord\ :=\ b,\ Xcoord\ :=\ |
|
200 |
a\isasymrparr "\isanewline |
|
201 |
\isacommand{by}\ simp |
|
202 |
\end{isabelle} |
|
203 |
We see above the syntax for iterated updates. We could equivalently |
|
204 |
have written the left-hand side as |
|
205 |
\isa{r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ \isasymlparr |
|
206 |
Ycoord\ :=\ b\isasymrparr}. |
|
207 |
||
11427 | 208 |
Record equality is \emph{extensional}: |
209 |
\index{extensionality!for records} |
|
210 |
a record is determined entirely by the values of its fields. |
|
11388 | 211 |
\begin{isabelle} |
212 |
\isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ |
|
213 |
Ycoord\ r\isasymrparr "\isanewline |
|
214 |
\isacommand{by}\ simp |
|
215 |
\end{isabelle} |
|
216 |
The generic version of this equality includes the field \isa{more}: |
|
217 |
\begin{isabelle} |
|
218 |
\isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ Ycoord\ r,\ \isasymdots \ =\ point.more\ |
|
219 |
r\isasymrparr" |
|
220 |
\end{isabelle} |
|
221 |
||
222 |
\medskip |
|
223 |
The simplifier can prove many record equalities automatically, |
|
224 |
but general equality reasoning can be tricky. Consider proving this |
|
225 |
obvious fact: |
|
226 |
\begin{isabelle} |
|
227 |
\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\ |
|
228 |
a'" |
|
229 |
\end{isabelle} |
|
230 |
The simplifier can do nothing. One way to proceed is by an explicit |
|
231 |
forward step that applies the selector \isa{Xcoord} to both sides |
|
232 |
of the assumed record equality: |
|
233 |
\begin{isabelle} |
|
234 |
\isacommand{apply}\ (drule_tac\ f=Xcoord\ \isakeyword{in}\ arg_cong)\isanewline |
|
235 |
\ 1.\ Xcoord\ (r\isasymlparr Xcoord\ :=\ a\isasymrparr )\ =\ Xcoord\ |
|
236 |
(r\isasymlparr Xcoord\ :=\ a'\isasymrparr )\ \isasymLongrightarrow \ |
|
237 |
a\ =\ a' |
|
238 |
\end{isabelle} |
|
239 |
Now, \isa{simp} will reduce the assumption to the desired |
|
240 |
conclusion. |
|
241 |
||
242 |
An alternative to such forward steps is record splitting. A record |
|
243 |
variable can be split only if it is bound in the subgoal by the |
|
244 |
meta-quantifier \isa{\isasymAnd}, or \isa{!!} in ASCII\@. So, |
|
245 |
we enter the lemma again: |
|
246 |
\begin{isabelle} |
|
247 |
\isacommand{lemma}\ "!!r.\ r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\ |
|
248 |
a'"\isanewline |
|
249 |
\end{isabelle} |
|
11427 | 250 |
The \methdx{record_split} method replaces the record variable by an |
11388 | 251 |
explicit record, listing all fields. Even the field \isa{more} is |
252 |
included, since the record equality is generic. |
|
253 |
\begin{isabelle} |
|
254 |
\isacommand{apply}\ record_split\isanewline |
|
255 |
\ 1.\ \isasymAnd Xcoord\ Ycoord\ more.\isanewline |
|
256 |
\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isanewline |
|
257 |
\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ :=\ a\isasymrparr \ =\isanewline |
|
258 |
\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isanewline |
|
259 |
\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \isanewline |
|
260 |
\isaindent{\ 1.\ \ \ \ }a\ =\ a' |
|
261 |
\end{isabelle} |
|
262 |
Again, \isa{simp} finishes the proof. Because the records have |
|
263 |
been split, the updates can be applied and the record equality can be |
|
264 |
replaced by equality of the corresponding fields. |
|
265 |
||
266 |
\begin{exercise} |
|
267 |
\REMARK{There should be some, but I can't think of any.} |
|
268 |
\end{exercise} |
|
11427 | 269 |
\index{records|)} |
11388 | 270 |
|
271 |
\endinput |
|
272 |