3 \def\isabellecontext{Records}%
5 \isamarkupheader{Records \label{sec:records}%
22 \begin{isamarkuptext}%
24 Records are familiar from programming languages. A record of $n$
25 fields is essentially an $n$-tuple, but the record's components have
26 names, which can make expressions easier to read and reduces the
27 risk of confusing one field for another.
29 A record of Isabelle/HOL covers a collection of fields, with select
30 and update operations. Each field has a specified type, which may
31 be polymorphic. The field names are part of the record type, and
32 the order of the fields is significant --- as it is in Pascal but
33 not in Standard ML. If two different record types have field names
34 in common, then the ambiguity is resolved in the usual way, by
37 Record types can also be defined by extending other record types.
38 Extensible records make use of the reserved pseudo-field \cdx{more},
39 which is present in every record type. Generic record operations
40 work on all possible extensions of a given type scheme; polymorphism
41 takes care of structural sub-typing behind the scenes. There are
42 also explicit coercion functions between fixed record types.%
46 \isamarkupsubsection{Record Basics%
50 \begin{isamarkuptext}%
51 Record types are not primitive in Isabelle and have a delicate
52 internal representation \cite{NaraschewskiW-TPHOLs98}, based on
53 nested copies of the primitive product type. A \commdx{record}
54 declaration introduces a new record type scheme by specifying its
55 fields, which are packaged internally to hold up the perception of
56 the record as a distinguished entity. Here is a simple example:%
59 \isacommand{record}\isamarkupfalse%
60 \ point\ {\isacharequal}\isanewline
61 \ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline
62 \ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int%
63 \begin{isamarkuptext}%
65 Records of type \isa{point} have two fields named \isa{Xcoord}
66 and \isa{Ycoord}, both of type~\isa{int}. We now define a
67 constant of type \isa{point}:%
70 \isacommand{definition}\isamarkupfalse%
71 \ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\ \isakeyword{where}\isanewline
72 {\isachardoublequoteopen}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequoteclose}%
73 \begin{isamarkuptext}%
75 We see above the ASCII notation for record brackets. You can also
76 use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}. Record type
77 expressions can be also written directly with individual fields.
78 The type name above is merely an abbreviation.%
81 \isacommand{definition}\isamarkupfalse%
82 \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
83 {\isachardoublequoteopen}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequoteclose}%
84 \begin{isamarkuptext}%
85 For each field, there is a \emph{selector}\index{selector!record}
86 function of the same name. For example, if \isa{p} has type \isa{point} then \isa{Xcoord\ p} denotes the value of the \isa{Xcoord} field of~\isa{p}. Expressions involving field selection
87 of explicit records are simplified automatically:%
90 \isacommand{lemma}\isamarkupfalse%
91 \ {\isachardoublequoteopen}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
98 \isacommand{by}\isamarkupfalse%
107 \begin{isamarkuptext}%
108 The \emph{update}\index{update!record} operation is functional. For
109 example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
110 value is zero and whose \isa{Ycoord} value is copied from~\isa{p}. Updates of explicit records are also simplified automatically:%
113 \isacommand{lemma}\isamarkupfalse%
114 \ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
115 \ \ \ \ \ \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequoteclose}\isanewline
122 \isacommand{by}\isamarkupfalse%
131 \begin{isamarkuptext}%
133 Field names are declared as constants and can no longer be used as
134 variables. It would be unwise, for example, to call the fields of
135 type \isa{point} simply \isa{x} and~\isa{y}.
140 \isamarkupsubsection{Extensible Records and Generic Operations%
144 \begin{isamarkuptext}%
145 \index{records!extensible|(}%
147 Now, let us define coloured points (type \isa{cpoint}) to be
148 points extended with a field \isa{col} of type \isa{colour}:%
151 \isacommand{datatype}\isamarkupfalse%
152 \ colour\ {\isacharequal}\ Red\ {\isacharbar}\ Green\ {\isacharbar}\ Blue\isanewline
154 \isacommand{record}\isamarkupfalse%
155 \ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline
156 \ \ col\ {\isacharcolon}{\isacharcolon}\ colour%
157 \begin{isamarkuptext}%
159 The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
160 \isa{col}, in that order.%
163 \isacommand{definition}\isamarkupfalse%
164 \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\ \isakeyword{where}\isanewline
165 {\isachardoublequoteopen}cpt{\isadigit{1}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}{\isacharcomma}\ col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequoteclose}%
166 \begin{isamarkuptext}%
167 We can define generic operations that work on arbitrary
168 instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions. Every record structure has an
169 implicit pseudo-field, \cdx{more}, that keeps the extension as an
170 explicit value. Its type is declared as completely
171 polymorphic:~\isa{{\isacharprime}a}. When a fixed record value is expressed
172 using just its standard fields, the value of \isa{more} is
173 implicitly set to \isa{{\isacharparenleft}{\isacharparenright}}, the empty tuple, which has type
174 \isa{unit}. Within the record brackets, you can refer to the
175 \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
178 \isacommand{lemma}\isamarkupfalse%
179 \ {\isachardoublequoteopen}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
186 \isacommand{by}\isamarkupfalse%
195 \begin{isamarkuptext}%
196 This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Note that \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}} is exactly the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}. Selectors and updates are always polymorphic wrt.\ the
197 \isa{more} part of a record scheme, its value is just ignored (for
198 select) or copied (for update).
200 The \isa{more} pseudo-field may be manipulated directly as well,
201 but the identifier needs to be qualified:%
204 \isacommand{lemma}\isamarkupfalse%
205 \ {\isachardoublequoteopen}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequoteclose}\isanewline
212 \isacommand{by}\isamarkupfalse%
213 \ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
221 \begin{isamarkuptext}%
223 We see that the colour part attached to this \isa{point} is a
224 rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col}, this fragment
225 needs to be put back into the context of the parent type scheme, say
226 as \isa{more} part of another \isa{point}.
228 To define generic operations, we need to know a bit more about
229 records. Our definition of \isa{point} above has generated two
234 \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\
235 \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\
240 Type \isa{point} is for fixed records having exactly the two fields
241 \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
242 fields. Note that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}, and \isa{{\isasymlparr}col\ {\isacharcolon}{\isacharcolon}\ colour{\isasymrparr}\ point{\isacharunderscore}scheme} with \isa{cpoint}.
244 In the following example we define two operations --- methods, if we
245 regard records as objects --- to get and set any point's \isa{Xcoord} field.%
248 \isacommand{definition}\isamarkupfalse%
249 \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
250 {\isachardoublequoteopen}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequoteclose}\isanewline
251 \isacommand{definition}\isamarkupfalse%
252 \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
253 {\isachardoublequoteopen}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequoteclose}%
254 \begin{isamarkuptext}%
255 Here is a generic method that modifies a point, incrementing its
256 \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
257 are copied across. It works for any record type scheme derived from
258 \isa{point} (including \isa{cpoint} etc.):%
261 \isacommand{definition}\isamarkupfalse%
262 \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
263 {\isachardoublequoteopen}incX\ r\ {\isasymequiv}\isanewline
264 \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}%
265 \begin{isamarkuptext}%
266 Generic theorems can be proved about generic methods. This trivial
267 lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
270 \isacommand{lemma}\isamarkupfalse%
271 \ {\isachardoublequoteopen}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
278 \isacommand{by}\isamarkupfalse%
279 \ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}%
287 \begin{isamarkuptext}%
289 If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
290 then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
291 than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''. Mixing the ASCII
292 and symbolic versions causes a syntax error. (The two versions are
293 more distinct on screen than they are on paper.)
295 \index{records!extensible|)}%
299 \isamarkupsubsection{Record Equality%
303 \begin{isamarkuptext}%
304 Two records are equal\index{equality!of records} if all pairs of
305 corresponding fields are equal. Concrete record equalities are
306 simplified automatically:%
309 \isacommand{lemma}\isamarkupfalse%
310 \ {\isachardoublequoteopen}{\isacharparenleft}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharprime}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isacharequal}\isanewline
311 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
318 \isacommand{by}\isamarkupfalse%
327 \begin{isamarkuptext}%
328 The following equality is similar, but generic, in that \isa{r}
329 can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
332 \isacommand{lemma}\isamarkupfalse%
333 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequoteclose}\isanewline
340 \isacommand{by}\isamarkupfalse%
349 \begin{isamarkuptext}%
351 We see above the syntax for iterated updates. We could equivalently
352 have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
354 Record equality is \emph{extensional}:
355 \index{extensionality!for records} a record is determined entirely
356 by the values of its fields.%
359 \isacommand{lemma}\isamarkupfalse%
360 \ {\isachardoublequoteopen}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequoteclose}\isanewline
367 \isacommand{by}\isamarkupfalse%
376 \begin{isamarkuptext}%
378 The generic version of this equality includes the pseudo-field
382 \isacommand{lemma}\isamarkupfalse%
383 \ {\isachardoublequoteopen}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}\isanewline
390 \isacommand{by}\isamarkupfalse%
399 \begin{isamarkuptext}%
400 The simplifier can prove many record equalities
401 automatically, but general equality reasoning can be tricky.
402 Consider proving this obvious fact:%
405 \isacommand{lemma}\isamarkupfalse%
406 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}\isanewline
413 \isacommand{apply}\isamarkupfalse%
414 \ simp{\isacharquery}\isanewline
415 \ \ \isacommand{oops}\isamarkupfalse%
424 \begin{isamarkuptext}%
426 Here the simplifier can do nothing, since general record equality is
427 not eliminated automatically. One way to proceed is by an explicit
428 forward step that applies the selector \isa{Xcoord} to both sides
429 of the assumed record equality:%
432 \isacommand{lemma}\isamarkupfalse%
433 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}\isanewline
440 \isacommand{apply}\isamarkupfalse%
441 \ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}%
442 \begin{isamarkuptxt}%
444 \ {\isadigit{1}}{\isachardot}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isacharparenright}\ {\isacharequal}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
446 Now, \isa{simp} will reduce the assumption to the desired
450 \ \ \isacommand{apply}\isamarkupfalse%
452 \ \ \isacommand{done}\isamarkupfalse%
461 \begin{isamarkuptext}%
462 The \isa{cases} method is preferable to such a forward proof. We
463 state the desired lemma again:%
466 \isacommand{lemma}\isamarkupfalse%
467 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}%
474 \begin{isamarkuptxt}%
475 The \methdx{cases} method adds an equality to replace the
476 named record term by an explicit record expression, listing all
477 fields. It even includes the pseudo-field \isa{more}, since the
478 record equality stated here is generic for all extensions.%
481 \ \ \isacommand{apply}\isamarkupfalse%
482 \ {\isacharparenleft}cases\ r{\isacharparenright}%
483 \begin{isamarkuptxt}%
485 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
486 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
487 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
488 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
489 \end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{r} is now represented as
490 an explicit record construction, the updates can be applied and the
491 record equality can be replaced by equality of the corresponding
492 fields (due to injectivity).%
495 \ \ \isacommand{apply}\isamarkupfalse%
497 \ \ \isacommand{done}\isamarkupfalse%
506 \begin{isamarkuptext}%
507 The generic cases method does not admit references to locally bound
508 parameters of a goal. In longer proof scripts one might have to
509 fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
510 internal field representation rules of records. The above use of
511 \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
515 \isamarkupsubsection{Extending and Truncating Records%
519 \begin{isamarkuptext}%
520 Each record declaration introduces a number of derived operations to
521 refer collectively to a record's fields and to convert between fixed
522 record types. They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or convert
523 a \isa{cpoint} to a \isa{point} by forgetting its colour.
527 \item Function \cdx{make} takes as arguments all of the record's
528 fields (including those inherited from ancestors). It returns the
529 corresponding record.
531 \item Function \cdx{fields} takes the record's very own fields and
532 returns a record fragment consisting of just those fields. This may
533 be filled into the \isa{more} part of the parent record scheme.
535 \item Function \cdx{extend} takes two arguments: a record to be
536 extended and a record containing the new fields.
538 \item Function \cdx{truncate} takes a record (possibly an extension
539 of the original record type) and returns a fixed record, removing
540 any additional fields.
543 These functions provide useful abbreviations for standard
544 record expressions involving constructors and selectors. The
545 definitions, which are \emph{not} unfolded by default, are made
546 available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).
547 For example, here are the versions of those functions generated for
548 record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to
549 be the same as \isa{point{\isachardot}make}.
552 point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
553 point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
554 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
555 point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
557 Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
559 cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
560 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
561 cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
562 cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
563 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
564 cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
565 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
568 To demonstrate these functions, we declare a new coloured point by
569 extending an ordinary point. Function \isa{point{\isachardot}extend} augments
570 \isa{pt{\isadigit{1}}} with a colour value, which is converted into an
571 appropriate record fragment by \isa{cpoint{\isachardot}fields}.%
574 \isacommand{definition}\isamarkupfalse%
575 \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\ \isakeyword{where}\isanewline
576 {\isachardoublequoteopen}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequoteclose}%
577 \begin{isamarkuptext}%
578 The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The
579 proof is trivial, by unfolding all the definitions. We deliberately
580 omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying
581 comparison on type \isa{point}.%
584 \isacommand{lemma}\isamarkupfalse%
585 \ {\isachardoublequoteopen}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequoteclose}\isanewline
592 \isacommand{apply}\isamarkupfalse%
593 \ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}%
594 \begin{isamarkuptxt}%
596 \ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
600 \ \ \isacommand{apply}\isamarkupfalse%
601 \ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
602 \ \ \isacommand{done}\isamarkupfalse%
611 \begin{isamarkuptext}%
612 In the example below, a coloured point is truncated to leave a
613 point. We use the \isa{truncate} function of the target record.%
616 \isacommand{lemma}\isamarkupfalse%
617 \ {\isachardoublequoteopen}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequoteclose}\isanewline
624 \isacommand{by}\isamarkupfalse%
625 \ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}%
633 \begin{isamarkuptext}%
635 Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with generic operations
636 (using polymorphic selectors and updates) and explicit coercions
637 (using \isa{extend}, \isa{truncate} etc.) among the three record
642 (For Java programmers.)
643 Model a small class hierarchy using records.
664 %%% TeX-master: "root"