1.1 --- a/doc-src/TutorialI/Types/document/Records.tex Fri Dec 21 19:56:42 2001 +0100
1.2 +++ b/doc-src/TutorialI/Types/document/Records.tex Fri Dec 21 20:58:25 2001 +0100
1.3 @@ -14,7 +14,7 @@
1.4 names, which can make expressions easier to read and reduces the
1.5 risk of confusing one field for another.
1.6
1.7 - A basic Isabelle record covers a certain set of fields, with select
1.8 + A record of Isabelle/HOL covers a collection of fields, with select
1.9 and update operations. Each field has a specified type, which may
1.10 be polymorphic. The field names are part of the record type, and
1.11 the order of the fields is significant --- as it is in Pascal but
1.12 @@ -25,10 +25,9 @@
1.13 Record types can also be defined by extending other record types.
1.14 Extensible records make use of the reserved pseudo-field \cdx{more},
1.15 which is present in every record type. Generic record operations
1.16 - work on all possible extensions of a given type scheme; naive
1.17 - polymorphism takes care of structural sub-typing behind the scenes.
1.18 - There are also explicit coercion functions between fixed record
1.19 - types.%
1.20 + work on all possible extensions of a given type scheme; polymorphism
1.21 + takes care of structural sub-typing behind the scenes. There are
1.22 + also explicit coercion functions between fixed record types.%
1.23 \end{isamarkuptext}%
1.24 \isamarkuptrue%
1.25 %
1.26 @@ -37,11 +36,11 @@
1.27 \isamarkuptrue%
1.28 %
1.29 \begin{isamarkuptext}%
1.30 -Record types are not primitive in Isabelle and have a subtle
1.31 +Record types are not primitive in Isabelle and have a delicate
1.32 internal representation based on nested copies of the primitive
1.33 product type. A \commdx{record} declaration introduces a new record
1.34 type scheme by specifying its fields, which are packaged internally
1.35 - to hold up the perception of records as a separate concept.%
1.36 + to hold up the perception of the record as a distinguished entity.%
1.37 \end{isamarkuptext}%
1.38 \isamarkuptrue%
1.39 \isacommand{record}\ point\ {\isacharequal}\isanewline
1.40 @@ -71,9 +70,9 @@
1.41 \ \ {\isachardoublequote}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
1.42 %
1.43 \begin{isamarkuptext}%
1.44 -For each field, there is a \emph{selector} function of the same
1.45 - 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
1.46 - simplified automatically:%
1.47 +For each field, there is a \emph{selector}\index{selector!record}
1.48 + 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
1.49 + of explicit records are simplified automatically:%
1.50 \end{isamarkuptext}%
1.51 \isamarkuptrue%
1.52 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
1.53 @@ -81,9 +80,9 @@
1.54 \isacommand{by}\ simp\isamarkupfalse%
1.55 %
1.56 \begin{isamarkuptext}%
1.57 -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
1.58 - and whose \isa{Ycoord} value is copied from~\isa{p}. Updates
1.59 - are also simplified automatically:%
1.60 +The \emph{update}\index{update!record} operation is functional. For
1.61 + example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
1.62 + value is zero and whose \isa{Ycoord} value is copied from~\isa{p}. Updates are also simplified automatically:%
1.63 \end{isamarkuptext}%
1.64 \isamarkuptrue%
1.65 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
1.66 @@ -95,8 +94,7 @@
1.67 \begin{warn}
1.68 Field names are declared as constants and can no longer be used as
1.69 variables. It would be unwise, for example, to call the fields of
1.70 - type \isa{point} simply \isa{x} and~\isa{y}. Each record
1.71 - declaration introduces a constant \cdx{more}.
1.72 + type \isa{point} simply \isa{x} and~\isa{y}.
1.73 \end{warn}%
1.74 \end{isamarkuptext}%
1.75 \isamarkuptrue%
1.76 @@ -144,10 +142,11 @@
1.77 \isacommand{by}\ simp\isamarkupfalse%
1.78 %
1.79 \begin{isamarkuptext}%
1.80 -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}}.
1.81 +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 really the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}. Selectors and updates are always polymorphic wrt.\ the \isa{more} part of a record scheme, its value is just ignored (for
1.82 + select) or copied (for update).
1.83
1.84 - The pseudo-field \isa{more} can be selected in the usual way, but
1.85 - the identifier must be qualified:%
1.86 + The \isa{more} pseudo-field may be manipulated directly as well,
1.87 + but the identifier needs to be qualified:%
1.88 \end{isamarkuptext}%
1.89 \isamarkuptrue%
1.90 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline
1.91 @@ -156,26 +155,27 @@
1.92 %
1.93 \begin{isamarkuptext}%
1.94 We see that the colour attached to this \isa{point} is a
1.95 - (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col} in the above
1.96 - fragment, \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}} needs to be put back into the
1.97 - context of its parent type scheme, say as \isa{more} part of a
1.98 - \isa{point}.
1.99 + (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col}, this fragment
1.100 + needs to be put back into the context of the parent type scheme, say
1.101 + as \isa{more} part of another \isa{point}.
1.102
1.103 To define generic operations, we need to know a bit more about
1.104 - records. Our declaration of \isa{point} above generated two type
1.105 + records. Our definition of \isa{point} above generated two type
1.106 abbreviations:
1.107
1.108 - \smallskip
1.109 + \medskip
1.110 \begin{tabular}{l}
1.111 \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\
1.112 \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}} \\
1.113 \end{tabular}
1.114 - \smallskip
1.115 + \medskip
1.116
1.117 - Type \isa{point} is for rigid records having exactly the two fields
1.118 + Type \isa{point} is for fixed records having exactly the two fields
1.119 \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
1.120 - fields, recall that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}. For example, let us define two operations --- methods, if
1.121 - we regard records as objects --- to get and set any point's \isa{Xcoord} field.%
1.122 + 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}.
1.123 +
1.124 + In the following example we define two operations --- methods, if we
1.125 + regard records as objects --- to get and set any point's \isa{Xcoord} field.%
1.126 \end{isamarkuptext}%
1.127 \isamarkuptrue%
1.128 \isacommand{constdefs}\isanewline
1.129 @@ -188,7 +188,7 @@
1.130 Here is a generic method that modifies a point, incrementing its
1.131 \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
1.132 are copied across. It works for any record type scheme derived from
1.133 - \isa{point}, such as \isa{cpoint}:%
1.134 + \isa{point} (including \isa{cpoint} etc.):%
1.135 \end{isamarkuptext}%
1.136 \isamarkuptrue%
1.137 \isacommand{constdefs}\isanewline
1.138 @@ -233,7 +233,7 @@
1.139 %
1.140 \begin{isamarkuptext}%
1.141 The following equality is similar, but generic, in that \isa{r}
1.142 - can be any instance of \isa{point{\isacharunderscore}scheme}:%
1.143 + can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
1.144 \end{isamarkuptext}%
1.145 \isamarkuptrue%
1.146 \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
1.147 @@ -242,11 +242,11 @@
1.148 %
1.149 \begin{isamarkuptext}%
1.150 We see above the syntax for iterated updates. We could equivalently
1.151 - have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
1.152 + have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
1.153
1.154 - Record equality is \emph{extensional}: \index{extensionality!for
1.155 - records} a record is determined entirely by the values of its
1.156 - fields.%
1.157 + \medskip Record equality is \emph{extensional}:
1.158 + \index{extensionality!for records} a record is determined entirely
1.159 + by the values of its fields.%
1.160 \end{isamarkuptext}%
1.161 \isamarkuptrue%
1.162 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
1.163 @@ -254,7 +254,8 @@
1.164 \isacommand{by}\ simp\isamarkupfalse%
1.165 %
1.166 \begin{isamarkuptext}%
1.167 -The generic version of this equality includes the field \isa{more}:%
1.168 +The generic version of this equality includes the pseudo-field
1.169 + \isa{more}:%
1.170 \end{isamarkuptext}%
1.171 \isamarkuptrue%
1.172 \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
1.173 @@ -262,10 +263,7 @@
1.174 \isacommand{by}\ simp\isamarkupfalse%
1.175 %
1.176 \begin{isamarkuptext}%
1.177 -Note that the \isa{r} is of a different (more general) type than
1.178 - the previous one.
1.179 -
1.180 - \medskip The simplifier can prove many record equalities
1.181 +\medskip The simplifier can prove many record equalities
1.182 automatically, but general equality reasoning can be tricky.
1.183 Consider proving this obvious fact:%
1.184 \end{isamarkuptext}%
1.185 @@ -277,8 +275,8 @@
1.186 \isacommand{oops}\isamarkupfalse%
1.187 %
1.188 \begin{isamarkuptext}%
1.189 -The simplifier can do nothing, since general record equality is not
1.190 - eliminated automatically. One way to proceed is by an explicit
1.191 +Here the simplifier can do nothing, since general record equality is
1.192 + not eliminated automatically. One way to proceed is by an explicit
1.193 forward step that applies the selector \isa{Xcoord} to both sides
1.194 of the assumed record equality:%
1.195 \end{isamarkuptext}%
1.196 @@ -300,17 +298,17 @@
1.197 \isacommand{done}\isamarkupfalse%
1.198 %
1.199 \begin{isamarkuptext}%
1.200 -The \isa{cases} method is preferable to such a forward proof.
1.201 - State the desired lemma again:%
1.202 +The \isa{cases} method is preferable to such a forward proof. We
1.203 + state the desired lemma again:%
1.204 \end{isamarkuptext}%
1.205 \isamarkuptrue%
1.206 \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%
1.207 %
1.208 \begin{isamarkuptxt}%
1.209 -The \methdx{cases} method adds an equality to replace the named
1.210 - record variable by an explicit record, listing all fields. It
1.211 - even includes the pseudo-field \isa{more}, since the record
1.212 - equality stated above is generic.%
1.213 +The \methdx{cases} method adds an equality to replace the
1.214 + named record term by an explicit record expression, listing all
1.215 + fields. It even includes the pseudo-field \isa{more}, since the
1.216 + record equality stated here is generic for all extensions.%
1.217 \end{isamarkuptxt}%
1.218 \ \ \isamarkuptrue%
1.219 \isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse%
1.220 @@ -321,32 +319,42 @@
1.221 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
1.222 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
1.223 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
1.224 -\end{isabelle}
1.225 - Again, \isa{simp} finishes the proof. Because \isa{r} has
1.226 - become an explicit record expression, the updates can be applied
1.227 - and the record equality can be replaced by equality of the
1.228 - corresponding fields (due to injectivity).%
1.229 +\end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{r} is now represented as
1.230 + an explicit record construction, the updates can be applied and the
1.231 + record equality can be replaced by equality of the corresponding
1.232 + fields (due to injectivity).%
1.233 \end{isamarkuptxt}%
1.234 \ \ \isamarkuptrue%
1.235 \isacommand{apply}\ simp\isanewline
1.236 \ \ \isamarkupfalse%
1.237 \isacommand{done}\isamarkupfalse%
1.238 %
1.239 +\begin{isamarkuptext}%
1.240 +The generic cases method does not admit references to locally bound
1.241 + parameters of a goal. In longer proof scripts one might have to
1.242 + fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
1.243 + internal representation rules of records. E.g.\ the above use of
1.244 + \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
1.245 +\end{isamarkuptext}%
1.246 +\isamarkuptrue%
1.247 +%
1.248 \isamarkupsubsection{Extending and Truncating Records%
1.249 }
1.250 \isamarkuptrue%
1.251 %
1.252 \begin{isamarkuptext}%
1.253 -Each record declaration introduces functions to refer collectively
1.254 - to a record's fields and to convert between related record types.
1.255 - 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.
1.256 +Each record declaration introduces a number of derived operations to
1.257 + refer collectively to a record's fields and to convert between fixed
1.258 + record types. They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or convert
1.259 + a \isa{cpoint} to a \isa{point} by forgetting its colour.
1.260
1.261 \begin{itemize}
1.262
1.263 \item Function \cdx{make} takes as arguments all of the record's
1.264 - fields. It returns the corresponding record.
1.265 + fields (including those inherited from ancestors). It returns the
1.266 + corresponding record.
1.267
1.268 - \item Function \cdx{fields} takes the record's new fields and
1.269 + \item Function \cdx{fields} takes the record's very own fields and
1.270 returns a record fragment consisting of just those fields. This may
1.271 be filled into the \isa{more} part of the parent record scheme.
1.272
1.273 @@ -362,34 +370,35 @@
1.274 These functions merely provide handsome abbreviations for standard
1.275 record expressions involving constructors and selectors. The
1.276 definitions, which are \emph{not} unfolded by default, are made
1.277 - available by the collective name of \isa{defs} (e.g.\ \isa{point{\isachardot}defs} or \isa{cpoint{\isachardot}defs}).
1.278 + available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).
1.279
1.280 For example, here are the versions of those functions generated for
1.281 record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to
1.282 be the same as \isa{point{\isachardot}make}.
1.283
1.284 \begin{isabelle}%
1.285 -point{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isasymrparr}\isanewline
1.286 -point{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline
1.287 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline
1.288 -point{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isasymrparr}%
1.289 +point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isanewline
1.290 +point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
1.291 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
1.292 +point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}%
1.293 \end{isabelle}
1.294
1.295 Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular.
1.296
1.297 \begin{isabelle}%
1.298 -cpoint{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isacharquery}col\ {\isasymequiv}\isanewline
1.299 -{\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isacharcomma}\ col\ {\isacharequal}\ {\isacharquery}col{\isasymrparr}\isanewline
1.300 -cpoint{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline
1.301 -{\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
1.302 -cpoint{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\isanewline
1.303 -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isasymrparr}%
1.304 +cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
1.305 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isanewline
1.306 +cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isanewline
1.307 +cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
1.308 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline
1.309 +cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
1.310 +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}%
1.311 \end{isabelle}
1.312
1.313 To demonstrate these functions, we declare a new coloured point by
1.314 extending an ordinary point. Function \isa{point{\isachardot}extend} augments
1.315 - \isa{pt{\isadigit{1}}} with a colour, which is converted into an appropriate
1.316 - record fragment by \isa{cpoint{\isachardot}fields}.%
1.317 + \isa{pt{\isadigit{1}}} with a colour value, which is converted into an
1.318 + appropriate record fragment by \isa{cpoint{\isachardot}fields}.%
1.319 \end{isamarkuptext}%
1.320 \isamarkuptrue%
1.321 \isacommand{constdefs}\isanewline
1.322 @@ -419,8 +428,7 @@
1.323 %
1.324 \begin{isamarkuptext}%
1.325 In the example below, a coloured point is truncated to leave a
1.326 - point. We must use the \isa{truncate} function of the shorter
1.327 - record.%
1.328 + point. We use the \isa{truncate} function of the target record.%
1.329 \end{isamarkuptext}%
1.330 \isamarkuptrue%
1.331 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
1.332 @@ -429,8 +437,10 @@
1.333 %
1.334 \begin{isamarkuptext}%
1.335 \begin{exercise}
1.336 - Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with coercions among the
1.337 - three record types.
1.338 + Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with generic operations
1.339 + (using polymorphic selectors and updates) and explicit coercions
1.340 + (using \isa{extend}, \isa{truncate} etc.) among the three record
1.341 + types.
1.342 \end{exercise}
1.343
1.344 \begin{exercise}