3 \def\isabellecontext{Records}%
5 \isamarkupheader{Records \label{sec:records}%
10 \begin{isamarkuptext}%
12 Records are familiar from programming languages. A record of $n$
13 fields is essentially an $n$-tuple, but the record's components have
14 names, which can make expressions easier to read and reduces the
15 risk of confusing one field for another.
17 A record of Isabelle/HOL covers a collection of fields, with select
18 and update operations. Each field has a specified type, which may
19 be polymorphic. The field names are part of the record type, and
20 the order of the fields is significant --- as it is in Pascal but
21 not in Standard ML. If two different record types have field names
22 in common, then the ambiguity is resolved in the usual way, by
25 Record types can also be defined by extending other record types.
26 Extensible records make use of the reserved pseudo-field \cdx{more},
27 which is present in every record type. Generic record operations
28 work on all possible extensions of a given type scheme; polymorphism
29 takes care of structural sub-typing behind the scenes. There are
30 also explicit coercion functions between fixed record types.%
34 \isamarkupsubsection{Record Basics%
38 \begin{isamarkuptext}%
39 Record types are not primitive in Isabelle and have a delicate
40 internal representation \cite{NaraschewskiW-TPHOLs98}, based on
41 nested copies of the primitive product type. A \commdx{record}
42 declaration introduces a new record type scheme by specifying its
43 fields, which are packaged internally to hold up the perception of
44 the record as a distinguished entity. Here is a simple example:%
47 \isacommand{record}\ point\ {\isacharequal}\isanewline
48 \ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline
49 \ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int\isamarkupfalse%
51 \begin{isamarkuptext}%
52 Records of type \isa{point} have two fields named \isa{Xcoord}
53 and \isa{Ycoord}, both of type~\isa{int}. We now define a
54 constant of type \isa{point}:%
57 \isacommand{constdefs}\isanewline
58 \ \ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\isanewline
59 \ \ {\isachardoublequote}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
61 \begin{isamarkuptext}%
62 We see above the ASCII notation for record brackets. You can also
63 use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}. Record type
64 expressions can be also written directly with individual fields.
65 The type name above is merely an abbreviation.%
68 \isacommand{constdefs}\isanewline
69 \ \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequote}\isanewline
70 \ \ {\isachardoublequote}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
72 \begin{isamarkuptext}%
73 For each field, there is a \emph{selector}\index{selector!record}
74 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
75 of explicit records are simplified automatically:%
78 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
80 \isacommand{by}\ simp\isamarkupfalse%
82 \begin{isamarkuptext}%
83 The \emph{update}\index{update!record} operation is functional. For
84 example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
85 value is zero and whose \isa{Ycoord} value is copied from~\isa{p}. Updates of explicit records are also simplified automatically:%
88 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
89 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline
91 \isacommand{by}\ simp\isamarkupfalse%
93 \begin{isamarkuptext}%
95 Field names are declared as constants and can no longer be used as
96 variables. It would be unwise, for example, to call the fields of
97 type \isa{point} simply \isa{x} and~\isa{y}.
102 \isamarkupsubsection{Extensible Records and Generic Operations%
106 \begin{isamarkuptext}%
107 \index{records!extensible|(}%
109 Now, let us define coloured points (type \isa{cpoint}) to be
110 points extended with a field \isa{col} of type \isa{colour}:%
113 \isacommand{datatype}\ colour\ {\isacharequal}\ Red\ {\isacharbar}\ Green\ {\isacharbar}\ Blue\isanewline
116 \isacommand{record}\ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline
117 \ \ col\ {\isacharcolon}{\isacharcolon}\ colour\isamarkupfalse%
119 \begin{isamarkuptext}%
120 The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
121 \isa{col}, in that order.%
124 \isacommand{constdefs}\isanewline
125 \ \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
126 \ \ {\isachardoublequote}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}{\isachardoublequote}\isamarkupfalse%
128 \begin{isamarkuptext}%
129 \medskip We can define generic operations that work on arbitrary
130 instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions. Every record structure has an
131 implicit pseudo-field, \cdx{more}, that keeps the extension as an
132 explicit value. Its type is declared as completely
133 polymorphic:~\isa{{\isacharprime}a}. When a fixed record value is expressed
134 using just its standard fields, the value of \isa{more} is
135 implicitly set to \isa{{\isacharparenleft}{\isacharparenright}}, the empty tuple, which has type
136 \isa{unit}. Within the record brackets, you can refer to the
137 \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
140 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
142 \isacommand{by}\ simp\isamarkupfalse%
144 \begin{isamarkuptext}%
145 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
146 \isa{more} part of a record scheme, its value is just ignored (for
147 select) or copied (for update).
149 The \isa{more} pseudo-field may be manipulated directly as well,
150 but the identifier needs to be qualified:%
153 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline
155 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
157 \begin{isamarkuptext}%
158 We see that the colour part attached to this \isa{point} is a
159 rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col}, this fragment
160 needs to be put back into the context of the parent type scheme, say
161 as \isa{more} part of another \isa{point}.
163 To define generic operations, we need to know a bit more about
164 records. Our definition of \isa{point} above has generated two
169 \isa{point}~\isa{{\isacharequal}}~\isa{point} \\
170 \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\
174 Type \isa{point} is for fixed records having exactly the two fields
175 \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
176 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}.
178 In the following example we define two operations --- methods, if we
179 regard records as objects --- to get and set any point's \isa{Xcoord} field.%
182 \isacommand{constdefs}\isanewline
183 \ \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequote}\isanewline
184 \ \ {\isachardoublequote}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequote}\isanewline
185 \ \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline
186 \ \ {\isachardoublequote}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
188 \begin{isamarkuptext}%
189 Here is a generic method that modifies a point, incrementing its
190 \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
191 are copied across. It works for any record type scheme derived from
192 \isa{point} (including \isa{cpoint} etc.):%
195 \isacommand{constdefs}\isanewline
196 \ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline
197 \ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\isanewline
198 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
200 \begin{isamarkuptext}%
201 Generic theorems can be proved about generic methods. This trivial
202 lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
205 \isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
207 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
209 \begin{isamarkuptext}%
211 If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
212 then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
213 than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''. 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.)
217 \index{records!extensible|)}%
221 \isamarkupsubsection{Record Equality%
225 \begin{isamarkuptext}%
226 Two records are equal\index{equality!of records} if all pairs of
227 corresponding fields are equal. Concrete record equalities are
228 simplified automatically:%
231 \isacommand{lemma}\ {\isachardoublequote}{\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
232 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline
234 \isacommand{by}\ simp\isamarkupfalse%
236 \begin{isamarkuptext}%
237 The following equality is similar, but generic, in that \isa{r}
238 can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
241 \isacommand{lemma}\ {\isachardoublequote}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}{\isachardoublequote}\isanewline
243 \isacommand{by}\ simp\isamarkupfalse%
245 \begin{isamarkuptext}%
246 We see above the syntax for iterated updates. We could equivalently
247 have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
249 \medskip Record equality is \emph{extensional}:
250 \index{extensionality!for records} a record is determined entirely
251 by the values of its fields.%
254 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
256 \isacommand{by}\ simp\isamarkupfalse%
258 \begin{isamarkuptext}%
259 The generic version of this equality includes the pseudo-field
263 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline
265 \isacommand{by}\ simp\isamarkupfalse%
267 \begin{isamarkuptext}%
268 \medskip The simplifier can prove many record equalities
269 automatically, but general equality reasoning can be tricky.
270 Consider proving this obvious fact:%
273 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
275 \isacommand{apply}\ simp{\isacharquery}\isanewline
277 \isacommand{oops}\isamarkupfalse%
279 \begin{isamarkuptext}%
280 Here the simplifier can do nothing, since general record equality is
281 not eliminated automatically. One way to proceed is by an explicit
282 forward step that applies the selector \isa{Xcoord} to both sides
283 of the assumed record equality:%
286 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
288 \isacommand{apply}\ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
290 \begin{isamarkuptxt}%
292 \ {\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}%
294 Now, \isa{simp} will reduce the assumption to the desired
298 \isacommand{apply}\ simp\isanewline
300 \isacommand{done}\isamarkupfalse%
302 \begin{isamarkuptext}%
303 The \isa{cases} method is preferable to such a forward proof. We
304 state the desired lemma again:%
307 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse%
309 \begin{isamarkuptxt}%
310 The \methdx{cases} method adds an equality to replace the
311 named record term by an explicit record expression, listing all
312 fields. It even includes the pseudo-field \isa{more}, since the
313 record equality stated here is generic for all extensions.%
316 \isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse%
318 \begin{isamarkuptxt}%
320 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
321 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
322 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
323 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
324 \end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{r} is now represented as
325 an explicit record construction, the updates can be applied and the
326 record equality can be replaced by equality of the corresponding
327 fields (due to injectivity).%
330 \isacommand{apply}\ simp\isanewline
332 \isacommand{done}\isamarkupfalse%
334 \begin{isamarkuptext}%
335 The generic cases method does not admit references to locally bound
336 parameters of a goal. In longer proof scripts one might have to
337 fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
338 internal field representation rules of records. The above use of
339 \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
343 \isamarkupsubsection{Extending and Truncating Records%
347 \begin{isamarkuptext}%
348 Each record declaration introduces a number of derived operations to
349 refer collectively to a record's fields and to convert between fixed
350 record types. They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or convert
351 a \isa{cpoint} to a \isa{point} by forgetting its colour.
355 \item Function \cdx{make} takes as arguments all of the record's
356 fields (including those inherited from ancestors). It returns the
357 corresponding record.
359 \item Function \cdx{fields} takes the record's very own fields and
360 returns a record fragment consisting of just those fields. This may
361 be filled into the \isa{more} part of the parent record scheme.
363 \item Function \cdx{extend} takes two arguments: a record to be
364 extended and a record containing the new fields.
366 \item Function \cdx{truncate} takes a record (possibly an extension
367 of the original record type) and returns a fixed record, removing
368 any additional fields.
372 These functions provide useful abbreviations for standard
373 record expressions involving constructors and selectors. The
374 definitions, which are \emph{not} unfolded by default, are made
375 available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).
377 For example, here are the versions of those functions generated for
378 record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to
379 be the same as \isa{point{\isachardot}make}.
382 point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isasep\isanewline%
383 point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
384 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
385 point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
388 Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
391 cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
392 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
393 cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isasep\isanewline%
394 cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
395 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
396 cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
397 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
400 To demonstrate these functions, we declare a new coloured point by
401 extending an ordinary point. Function \isa{point{\isachardot}extend} augments
402 \isa{pt{\isadigit{1}}} with a colour value, which is converted into an
403 appropriate record fragment by \isa{cpoint{\isachardot}fields}.%
406 \isacommand{constdefs}\isanewline
407 \ \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
408 \ \ {\isachardoublequote}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
410 \begin{isamarkuptext}%
411 The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The
412 proof is trivial, by unfolding all the definitions. We deliberately
413 omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying
414 comparison on type \isa{point}.%
417 \isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline
419 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}\isamarkupfalse%
421 \begin{isamarkuptxt}%
423 \ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
427 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
429 \isacommand{done}\isamarkupfalse%
431 \begin{isamarkuptext}%
432 In the example below, a coloured point is truncated to leave a
433 point. We use the \isa{truncate} function of the target record.%
436 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
438 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}\isamarkupfalse%
440 \begin{isamarkuptext}%
442 Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with generic operations
443 (using polymorphic selectors and updates) and explicit coercions
444 (using \isa{extend}, \isa{truncate} etc.) among the three record
449 (For Java programmers.)
450 Model a small class hierarchy using records.
459 %%% TeX-master: "root"