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