author | wenzelm |
Thu, 20 Dec 2001 21:11:04 +0100 | |
changeset 12567 | 614ef5ca41ed |
parent 12409 | 25bf458af885 |
child 12586 | 6bf380202adb |
permissions | -rw-r--r-- |
12567 | 1 |
|
2 |
header {* Records \label{sec:records} *} |
|
3 |
||
4 |
(*<*) |
|
5 |
theory Records = Main: |
|
6 |
(*>*) |
|
7 |
||
8 |
text {* |
|
9 |
\index{records|(}% |
|
10 |
Records are familiar from programming languages. A record of $n$ |
|
11 |
fields is essentially an $n$-tuple, but the record's components have |
|
12 |
names, which can make expressions easier to read and reduces the |
|
13 |
risk of confusing one field for another. |
|
11387 | 14 |
|
12567 | 15 |
A basic Isabelle record covers a certain set of fields, with select |
16 |
and update operations. Each field has a specified type, which may |
|
17 |
be polymorphic. The field names are part of the record type, and |
|
18 |
the order of the fields is significant --- as it is in Pascal but |
|
19 |
not in Standard ML. If two different record types have field names |
|
20 |
in common, then the ambiguity is resolved in the usual way, by |
|
21 |
qualified names. |
|
11387 | 22 |
|
12567 | 23 |
Record types can also be defined by extending other record types. |
24 |
Extensible records make use of the reserved pseudo-field \cdx{more}, |
|
25 |
which is present in every record type. Generic record operations |
|
26 |
work on all possible extensions of a given type scheme; naive |
|
27 |
polymorphism takes care of structural sub-typing behind the scenes. |
|
28 |
There are also explicit coercion functions between fixed record |
|
29 |
types. |
|
30 |
*} |
|
31 |
||
11387 | 32 |
|
12567 | 33 |
subsection {* Record Basics *} |
34 |
||
35 |
text {* |
|
36 |
Record types are not primitive in Isabelle and have a subtle |
|
37 |
internal representation based on nested copies of the primitive |
|
38 |
product type. A \commdx{record} declaration introduces a new record |
|
39 |
type scheme by specifying its fields, which are packaged internally |
|
40 |
to hold up the perception of records as a separate concept. |
|
41 |
*} |
|
11387 | 42 |
|
43 |
record point = |
|
44 |
Xcoord :: int |
|
45 |
Ycoord :: int |
|
46 |
||
47 |
text {* |
|
12567 | 48 |
Records of type @{typ point} have two fields named @{text Xcoord} |
49 |
and @{text Ycoord}, both of type~@{typ int}. We now define a |
|
50 |
constant of type @{typ point}: |
|
51 |
*} |
|
52 |
||
53 |
constdefs |
|
54 |
pt1 :: point |
|
55 |
"pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)" |
|
56 |
||
57 |
text {* |
|
58 |
We see above the ASCII notation for record brackets. You can also |
|
59 |
use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}. Record type |
|
60 |
expressions can be written directly as well, without referring to |
|
61 |
previously declared names (which happen to be mere type |
|
62 |
abbreviations): |
|
63 |
*} |
|
64 |
||
65 |
constdefs |
|
66 |
pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>" |
|
67 |
"pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>" |
|
68 |
||
69 |
text {* |
|
70 |
For each field, there is a \emph{selector} function of the same |
|
71 |
name. For example, if @{text p} has type @{typ point} then @{text |
|
72 |
"Xcoord p"} denotes the value of the @{text Xcoord} field of~@{text |
|
73 |
p}. Expressions involving field selection of explicit records are |
|
74 |
simplified automatically: |
|
75 |
*} |
|
76 |
||
77 |
lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a" |
|
78 |
by simp |
|
79 |
||
80 |
text {* |
|
81 |
The \emph{update} operation is functional. For example, @{term |
|
82 |
"p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord} value is zero |
|
83 |
and whose @{text Ycoord} value is copied from~@{text p}. Updates |
|
84 |
are also simplified automatically: |
|
85 |
*} |
|
86 |
||
87 |
lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> = |
|
88 |
\<lparr>Xcoord = 0, Ycoord = b\<rparr>" |
|
89 |
by simp |
|
90 |
||
91 |
text {* |
|
92 |
\begin{warn} |
|
93 |
Field names are declared as constants and can no longer be used as |
|
94 |
variables. It would be unwise, for example, to call the fields of |
|
95 |
type @{typ point} simply @{text x} and~@{text y}. Each record |
|
96 |
declaration introduces a constant \cdx{more}. |
|
97 |
\end{warn} |
|
11387 | 98 |
*} |
99 |
||
11428 | 100 |
|
12567 | 101 |
subsection {* Extensible Records and Generic Operations *} |
11387 | 102 |
|
103 |
text {* |
|
12567 | 104 |
\index{records!extensible|(}% |
11387 | 105 |
|
12567 | 106 |
Now, let us define coloured points (type @{text cpoint}) to be |
107 |
points extended with a field @{text col} of type @{text colour}: |
|
11387 | 108 |
*} |
109 |
||
110 |
datatype colour = Red | Green | Blue |
|
111 |
||
112 |
record cpoint = point + |
|
113 |
col :: colour |
|
114 |
||
12567 | 115 |
text {* |
116 |
The fields of this new type are @{text Xcoord}, @{text Ycoord} and |
|
117 |
@{text col}, in that order: |
|
118 |
*} |
|
11387 | 119 |
|
12567 | 120 |
constdefs |
11387 | 121 |
cpt1 :: cpoint |
12567 | 122 |
"cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>" |
11387 | 123 |
|
12567 | 124 |
text {* |
125 |
We can define generic operations that work on arbitrary instances of |
|
126 |
a record scheme, e.g.\ covering @{typ point}, @{typ cpoint} and any |
|
127 |
further extensions. Every record structure has an implicit |
|
128 |
pseudo-field, \cdx{more}, that keeps the extension as an explicit |
|
129 |
value. Its type is declared as completely polymorphic:~@{typ 'a}. |
|
130 |
When a fixed record value is expressed using just its standard |
|
131 |
fields, the value of @{text more} is implicitly set to @{text "()"}, |
|
132 |
the empty tuple, which has type @{typ unit}. Within the record |
|
133 |
brackets, you can refer to the @{text more} field by writing @{text |
|
134 |
"\<dots>"} (three dots): |
|
135 |
*} |
|
11387 | 136 |
|
12567 | 137 |
lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a" |
138 |
by simp |
|
11387 | 139 |
|
12567 | 140 |
text {* |
141 |
This lemma applies to any record whose first two fields are @{text |
|
142 |
Xcoord} and~@{text Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord |
|
143 |
= b, \<dots> = ()\<rparr>"} is actually the same as @{text "\<lparr>Xcoord = a, |
|
144 |
Ycoord = b\<rparr>"}. |
|
145 |
||
146 |
The pseudo-field @{text more} can be selected in the usual way, but |
|
147 |
the identifier must be qualified: |
|
148 |
*} |
|
11387 | 149 |
|
150 |
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>" |
|
12567 | 151 |
by (simp add: cpt1_def) |
11387 | 152 |
|
153 |
text {* |
|
12567 | 154 |
We see that the colour attached to this @{typ point} is a |
155 |
(rudimentary) record in its own right, namely @{text "\<lparr>col = |
|
156 |
Green\<rparr>"}. In order to select or update @{text col} in the above |
|
157 |
fragment, @{text "\<lparr>col = Green\<rparr>"} needs to be put back into the |
|
158 |
context of its parent type scheme, say as @{text more} part of a |
|
159 |
@{typ point}. |
|
160 |
||
161 |
To define generic operations, we need to know a bit more about |
|
162 |
records. Our declaration of @{typ point} above generated two type |
|
163 |
abbreviations: |
|
164 |
||
165 |
\smallskip |
|
166 |
\begin{tabular}{l} |
|
167 |
@{typ point}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\ |
|
168 |
@{typ "'a point_scheme"}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\ |
|
169 |
\end{tabular} |
|
170 |
\smallskip |
|
171 |
||
172 |
Type @{typ point} is for rigid records having exactly the two fields |
|
173 |
@{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ |
|
174 |
"'a point_scheme"} comprises all possible extensions to those two |
|
175 |
fields, recall that @{typ "unit point_scheme"} coincides with @{typ |
|
176 |
point}. For example, let us define two operations --- methods, if |
|
177 |
we regard records as objects --- to get and set any point's @{text |
|
178 |
Xcoord} field. |
|
11387 | 179 |
*} |
180 |
||
181 |
constdefs |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
182 |
getX :: "'a point_scheme \<Rightarrow> int" |
12567 | 183 |
"getX r \<equiv> Xcoord r" |
184 |
setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme" |
|
185 |
"setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>" |
|
11387 | 186 |
|
187 |
text {* |
|
12567 | 188 |
Here is a generic method that modifies a point, incrementing its |
189 |
@{text Xcoord} field. The @{text Ycoord} and @{text more} fields |
|
190 |
are copied across. It works for any record type scheme derived from |
|
191 |
@{typ point}, such as @{typ cpoint}: |
|
11387 | 192 |
*} |
193 |
||
194 |
constdefs |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
195 |
incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" |
12567 | 196 |
"incX r \<equiv> \<lparr>Xcoord = Xcoord r + 1, |
197 |
Ycoord = Ycoord r, \<dots> = point.more r\<rparr>" |
|
11387 | 198 |
|
199 |
text {* |
|
12567 | 200 |
Generic theorems can be proved about generic methods. This trivial |
201 |
lemma relates @{text incX} to @{text getX} and @{text setX}: |
|
202 |
*} |
|
11387 | 203 |
|
12567 | 204 |
lemma "incX r = setX r (getX r + 1)" |
205 |
by (simp add: getX_def setX_def incX_def) |
|
11387 | 206 |
|
207 |
text {* |
|
12567 | 208 |
\begin{warn} |
209 |
If you use the symbolic record brackets @{text \<lparr>} and @{text \<rparr>}, |
|
210 |
then you must also use the symbolic ellipsis, ``@{text \<dots>}'', rather |
|
211 |
than three consecutive periods, ``@{text "..."}''. Mixing the ASCII |
|
212 |
and symbolic versions causes a syntax error. (The two versions are |
|
213 |
more distinct on screen than they are on paper.) |
|
214 |
\end{warn}%\index{records!extensible|)} |
|
215 |
*} |
|
11387 | 216 |
|
217 |
||
12567 | 218 |
subsection {* Record Equality *} |
219 |
||
220 |
text {* |
|
221 |
Two records are equal\index{equality!of records} if all pairs of |
|
222 |
corresponding fields are equal. Record equalities are simplified |
|
223 |
automatically: |
|
224 |
*} |
|
225 |
||
226 |
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = |
|
227 |
(a = a' \<and> b = b')" |
|
228 |
by simp |
|
11387 | 229 |
|
12567 | 230 |
text {* |
231 |
The following equality is similar, but generic, in that @{text r} |
|
232 |
can be any instance of @{text point_scheme}: |
|
233 |
*} |
|
234 |
||
235 |
lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>" |
|
236 |
by simp |
|
11387 | 237 |
|
12567 | 238 |
text {* |
239 |
We see above the syntax for iterated updates. We could equivalently |
|
240 |
have written the left-hand side as @{term "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord |
|
241 |
:= b\<rparr>"}. |
|
242 |
||
243 |
Record equality is \emph{extensional}: \index{extensionality!for |
|
244 |
records} a record is determined entirely by the values of its |
|
245 |
fields. |
|
246 |
*} |
|
11387 | 247 |
|
248 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>" |
|
12567 | 249 |
by simp |
11387 | 250 |
|
12567 | 251 |
text {* |
252 |
The generic version of this equality includes the field @{text |
|
253 |
more}: |
|
254 |
*} |
|
11387 | 255 |
|
12567 | 256 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>" |
257 |
by simp |
|
11387 | 258 |
|
259 |
text {* |
|
12567 | 260 |
Note that the @{text r} is of a different (more general) type than |
261 |
the previous one. |
|
262 |
||
263 |
\medskip The simplifier can prove many record equalities |
|
264 |
automatically, but general equality reasoning can be tricky. |
|
265 |
Consider proving this obvious fact: |
|
266 |
*} |
|
267 |
||
268 |
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'" |
|
269 |
apply simp? |
|
270 |
oops |
|
271 |
||
272 |
text {* |
|
273 |
The simplifier can do nothing, since general record equality is not |
|
274 |
eliminated automatically. One way to proceed is by an explicit |
|
275 |
forward step that applies the selector @{text Xcoord} to both sides |
|
276 |
of the assumed record equality: |
|
11387 | 277 |
*} |
278 |
||
12567 | 279 |
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'" |
280 |
apply (drule_tac f = Xcoord in arg_cong) |
|
281 |
txt {* @{subgoals [display, indent = 0, margin = 65]} |
|
282 |
Now, @{text simp} will reduce the assumption to the desired |
|
283 |
conclusion. *} |
|
284 |
apply simp |
|
285 |
done |
|
286 |
||
287 |
text {* |
|
288 |
The @{text cases} method is preferable to such a forward proof. |
|
289 |
State the desired lemma again: |
|
290 |
*} |
|
11387 | 291 |
|
12567 | 292 |
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'" |
293 |
txt {* |
|
294 |
The \methdx{cases} method adds an equality to replace the named |
|
295 |
record variable by an explicit record, listing all fields. It |
|
296 |
even includes the pseudo-field @{text more}, since the record |
|
297 |
equality stated above is generic. *} |
|
298 |
apply (cases r) |
|
11387 | 299 |
|
12567 | 300 |
txt {* @{subgoals [display, indent = 0, margin = 65]} |
301 |
Again, @{text simp} finishes the proof. Because @{text r} has |
|
302 |
become an explicit record expression, the updates can be applied |
|
303 |
and the record equality can be replaced by equality of the |
|
304 |
corresponding fields (due to injectivity). *} |
|
305 |
apply simp |
|
306 |
done |
|
11387 | 307 |
|
308 |
||
12567 | 309 |
subsection {* Extending and Truncating Records *} |
11387 | 310 |
|
311 |
text {* |
|
12567 | 312 |
Each record declaration introduces functions to refer collectively |
313 |
to a record's fields and to convert between related record types. |
|
314 |
They can, for instance, convert between types @{typ point} and @{typ |
|
315 |
cpoint}. We can add a colour to a point or to convert a @{typ |
|
316 |
cpoint} to a @{typ point} by forgetting its colour. |
|
317 |
||
318 |
\begin{itemize} |
|
319 |
||
320 |
\item Function \cdx{make} takes as arguments all of the record's |
|
321 |
fields. It returns the corresponding record. |
|
322 |
||
323 |
\item Function \cdx{fields} takes the record's new fields and |
|
324 |
returns a record fragment consisting of just those fields. This may |
|
325 |
be filled into the @{text more} part of the parent record scheme. |
|
326 |
||
327 |
\item Function \cdx{extend} takes two arguments: a record to be |
|
328 |
extended and a record containing the new fields. |
|
329 |
||
330 |
\item Function \cdx{truncate} takes a record (possibly an extension |
|
331 |
of the original record type) and returns a fixed record, removing |
|
332 |
any additional fields. |
|
333 |
||
334 |
\end{itemize} |
|
11387 | 335 |
|
12567 | 336 |
These functions merely provide handsome abbreviations for standard |
337 |
record expressions involving constructors and selectors. The |
|
338 |
definitions, which are \emph{not} unfolded by default, are made |
|
339 |
available by the collective name of @{text defs} (e.g.\ @{text |
|
340 |
point.defs} or @{text cpoint.defs}). |
|
341 |
||
342 |
For example, here are the versions of those functions generated for |
|
343 |
record @{typ point}. We omit @{text point.fields}, which happens to |
|
344 |
be the same as @{text point.make}. |
|
11387 | 345 |
|
12567 | 346 |
@{thm [display, indent = 0, margin = 65] point.make_def |
347 |
point.extend_def point.truncate_def} |
|
348 |
||
349 |
Contrast those with the corresponding functions for record @{typ |
|
350 |
cpoint}. Observe @{text cpoint.fields} in particular. |
|
351 |
||
352 |
@{thm [display, indent = 0, margin = 65] cpoint.make_def |
|
353 |
cpoint.extend_def cpoint.truncate_def} |
|
354 |
||
355 |
To demonstrate these functions, we declare a new coloured point by |
|
356 |
extending an ordinary point. Function @{text point.extend} augments |
|
357 |
@{text pt1} with a colour, which is converted into an appropriate |
|
358 |
record fragment by @{text cpoint.fields}. |
|
359 |
*} |
|
11387 | 360 |
|
12407 | 361 |
constdefs |
362 |
cpt2 :: cpoint |
|
12567 | 363 |
"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)" |
12407 | 364 |
|
365 |
text {* |
|
12567 | 366 |
The coloured points @{text cpt1} and @{text cpt2} are equal. The |
367 |
proof is trivial, by unfolding all the definitions. We deliberately |
|
368 |
omit the definition of~@{text pt1} in order to reveal the underlying |
|
369 |
comparison on type @{typ point}. |
|
370 |
*} |
|
371 |
||
372 |
lemma "cpt1 = cpt2" |
|
373 |
apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs) |
|
374 |
txt {* @{subgoals [display, indent = 0, margin = 65]} *} |
|
375 |
apply (simp add: pt1_def) |
|
376 |
done |
|
12407 | 377 |
|
378 |
text {* |
|
12567 | 379 |
In the example below, a coloured point is truncated to leave a |
380 |
point. We must use the @{text truncate} function of the shorter |
|
381 |
record. |
|
382 |
*} |
|
12407 | 383 |
|
384 |
lemma "point.truncate cpt2 = pt1" |
|
12567 | 385 |
by (simp add: pt1_def cpt2_def point.defs) |
386 |
||
387 |
text {* |
|
388 |
\begin{exercise} |
|
389 |
Extend record @{typ cpoint} to have a further field, @{text |
|
390 |
intensity}, of type~@{typ nat}. Experiment with coercions among the |
|
391 |
three record types. |
|
392 |
\end{exercise} |
|
12407 | 393 |
|
12567 | 394 |
\begin{exercise} |
395 |
(For Java programmers.) |
|
396 |
Model a small class hierarchy using records. |
|
397 |
\end{exercise} |
|
398 |
\index{records|)} |
|
399 |
*} |
|
400 |
||
401 |
(*<*) |
|
11387 | 402 |
end |
12567 | 403 |
(*>*) |