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 basic Isabelle record covers a certain set 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; naive
29 polymorphism takes care of structural sub-typing behind the scenes.
30 There are also explicit coercion functions between fixed record
35 \isamarkupsubsection{Record Basics%
39 \begin{isamarkuptext}%
40 Record types are not primitive in Isabelle and have a subtle
41 internal representation based on nested copies of the primitive
42 product type. A \commdx{record} declaration introduces a new record
43 type scheme by specifying its fields, which are packaged internally
44 to hold up the perception of records as a separate concept.%
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 written directly as well, without referring to
65 previously declared names (which happen to be mere type
69 \isacommand{constdefs}\isanewline
70 \ \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequote}\isanewline
71 \ \ {\isachardoublequote}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
73 \begin{isamarkuptext}%
74 For each field, there is a \emph{selector} function of the same
75 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 of explicit records are
76 simplified automatically:%
79 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
81 \isacommand{by}\ simp\isamarkupfalse%
83 \begin{isamarkuptext}%
84 The \emph{update} operation is functional. For example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord} value is zero
85 and whose \isa{Ycoord} value is copied from~\isa{p}. Updates
86 are also simplified automatically:%
89 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
90 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline
92 \isacommand{by}\ simp\isamarkupfalse%
94 \begin{isamarkuptext}%
96 Field names are declared as constants and can no longer be used as
97 variables. It would be unwise, for example, to call the fields of
98 type \isa{point} simply \isa{x} and~\isa{y}. Each record
99 declaration introduces a constant \cdx{more}.
104 \isamarkupsubsection{Extensible Records and Generic Operations%
108 \begin{isamarkuptext}%
109 \index{records!extensible|(}%
111 Now, let us define coloured points (type \isa{cpoint}) to be
112 points extended with a field \isa{col} of type \isa{colour}:%
115 \isacommand{datatype}\ colour\ {\isacharequal}\ Red\ {\isacharbar}\ Green\ {\isacharbar}\ Blue\isanewline
118 \isacommand{record}\ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline
119 \ \ col\ {\isacharcolon}{\isacharcolon}\ colour\isamarkupfalse%
121 \begin{isamarkuptext}%
122 The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
123 \isa{col}, in that order:%
126 \isacommand{constdefs}\isanewline
127 \ \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
128 \ \ {\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%
130 \begin{isamarkuptext}%
131 We can define generic operations that work on arbitrary instances of
132 a record scheme, e.g.\ covering \isa{point}, \isa{cpoint} and any
133 further extensions. Every record structure has an implicit
134 pseudo-field, \cdx{more}, that keeps the extension as an explicit
135 value. Its type is declared as completely polymorphic:~\isa{{\isacharprime}a}.
136 When a fixed record value is expressed using just its standard
137 fields, the value of \isa{more} is implicitly set to \isa{{\isacharparenleft}{\isacharparenright}},
138 the empty tuple, which has type \isa{unit}. Within the record
139 brackets, you can refer to the \isa{more} field by writing \isa{{\isasymdots}} (three dots):%
142 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
144 \isacommand{by}\ simp\isamarkupfalse%
146 \begin{isamarkuptext}%
147 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 actually the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}.
149 The pseudo-field \isa{more} can be selected in the usual way, but
150 the identifier must 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 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} in the above
160 fragment, \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}} needs to be put back into the
161 context of its parent type scheme, say as \isa{more} part of a
164 To define generic operations, we need to know a bit more about
165 records. Our declaration of \isa{point} above generated two type
170 \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\
171 \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}} \\
175 Type \isa{point} is for rigid records having exactly the two fields
176 \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
177 fields, recall that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}. For example, let us define two operations --- methods, if
178 we regard records as objects --- to get and set any point's \isa{Xcoord} field.%
181 \isacommand{constdefs}\isanewline
182 \ \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequote}\isanewline
183 \ \ {\isachardoublequote}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequote}\isanewline
184 \ \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline
185 \ \ {\isachardoublequote}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
187 \begin{isamarkuptext}%
188 Here is a generic method that modifies a point, incrementing its
189 \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
190 are copied across. It works for any record type scheme derived from
191 \isa{point}, such as \isa{cpoint}:%
194 \isacommand{constdefs}\isanewline
195 \ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline
196 \ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\isanewline
197 \ \ \ \ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
199 \begin{isamarkuptext}%
200 Generic theorems can be proved about generic methods. This trivial
201 lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
204 \isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
206 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
208 \begin{isamarkuptext}%
210 If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
211 then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
212 than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''. Mixing the ASCII
213 and symbolic versions causes a syntax error. (The two versions are
214 more distinct on screen than they are on paper.)
215 \end{warn}%\index{records!extensible|)}%
219 \isamarkupsubsection{Record Equality%
223 \begin{isamarkuptext}%
224 Two records are equal\index{equality!of records} if all pairs of
225 corresponding fields are equal. Record equalities are simplified
229 \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
230 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline
232 \isacommand{by}\ simp\isamarkupfalse%
234 \begin{isamarkuptext}%
235 The following equality is similar, but generic, in that \isa{r}
236 can be any instance of \isa{point{\isacharunderscore}scheme}:%
239 \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
241 \isacommand{by}\ simp\isamarkupfalse%
243 \begin{isamarkuptext}%
244 We see above the syntax for iterated updates. We could equivalently
245 have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
247 Record equality is \emph{extensional}: \index{extensionality!for
248 records} a record is determined entirely by the values of its
252 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
254 \isacommand{by}\ simp\isamarkupfalse%
256 \begin{isamarkuptext}%
257 The generic version of this equality includes the field \isa{more}:%
260 \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
262 \isacommand{by}\ simp\isamarkupfalse%
264 \begin{isamarkuptext}%
265 Note that the \isa{r} is of a different (more general) type than
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 The simplifier can do nothing, since general record equality is not
281 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.
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 named
311 record variable by an explicit record, listing all fields. It
312 even includes the pseudo-field \isa{more}, since the record
313 equality stated above is generic.%
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}%
325 Again, \isa{simp} finishes the proof. Because \isa{r} has
326 become an explicit record expression, the updates can be applied
327 and the record equality can be replaced by equality of the
328 corresponding fields (due to injectivity).%
331 \isacommand{apply}\ simp\isanewline
333 \isacommand{done}\isamarkupfalse%
335 \isamarkupsubsection{Extending and Truncating Records%
339 \begin{isamarkuptext}%
340 Each record declaration introduces functions to refer collectively
341 to a record's fields and to convert between related record types.
342 They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or to convert a \isa{cpoint} to a \isa{point} by forgetting its colour.
346 \item Function \cdx{make} takes as arguments all of the record's
347 fields. It returns the corresponding record.
349 \item Function \cdx{fields} takes the record's new fields and
350 returns a record fragment consisting of just those fields. This may
351 be filled into the \isa{more} part of the parent record scheme.
353 \item Function \cdx{extend} takes two arguments: a record to be
354 extended and a record containing the new fields.
356 \item Function \cdx{truncate} takes a record (possibly an extension
357 of the original record type) and returns a fixed record, removing
358 any additional fields.
362 These functions merely provide handsome abbreviations for standard
363 record expressions involving constructors and selectors. The
364 definitions, which are \emph{not} unfolded by default, are made
365 available by the collective name of \isa{defs} (e.g.\ \isa{point{\isachardot}defs} or \isa{cpoint{\isachardot}defs}).
367 For example, here are the versions of those functions generated for
368 record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to
369 be the same as \isa{point{\isachardot}make}.
372 point{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isasymrparr}\isanewline
373 point{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline
374 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline
375 point{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isasymrparr}%
378 Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
381 cpoint{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isacharquery}col\ {\isasymequiv}\isanewline
382 {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isacharcomma}\ col\ {\isacharequal}\ {\isacharquery}col{\isasymrparr}\isanewline
383 cpoint{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline
384 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline
385 cpoint{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\isanewline
386 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isasymrparr}%
389 To demonstrate these functions, we declare a new coloured point by
390 extending an ordinary point. Function \isa{point{\isachardot}extend} augments
391 \isa{pt{\isadigit{1}}} with a colour, which is converted into an appropriate
392 record fragment by \isa{cpoint{\isachardot}fields}.%
395 \isacommand{constdefs}\isanewline
396 \ \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
397 \ \ {\isachardoublequote}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
399 \begin{isamarkuptext}%
400 The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The
401 proof is trivial, by unfolding all the definitions. We deliberately
402 omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying
403 comparison on type \isa{point}.%
406 \isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline
408 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}\isamarkupfalse%
410 \begin{isamarkuptxt}%
412 \ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
416 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
418 \isacommand{done}\isamarkupfalse%
420 \begin{isamarkuptext}%
421 In the example below, a coloured point is truncated to leave a
422 point. We must use the \isa{truncate} function of the shorter
426 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
428 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}\isamarkupfalse%
430 \begin{isamarkuptext}%
432 Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with coercions among the
437 (For Java programmers.)
438 Model a small class hierarchy using records.
447 %%% TeX-master: "root"