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