1.1 --- a/doc-src/TutorialI/Types/Records.thy Thu Dec 20 18:22:44 2001 +0100
1.2 +++ b/doc-src/TutorialI/Types/Records.thy Thu Dec 20 21:11:04 2001 +0100
1.3 @@ -1,265 +1,403 @@
1.4 -(* Title: HOL/ex/Records.thy
1.5 - ID: $Id$
1.6 - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
1.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
1.8 -*)
1.9
1.10 -header {* Extensible Records *}
1.11 +header {* Records \label{sec:records} *}
1.12
1.13 +(*<*)
1.14 theory Records = Main:
1.15 +(*>*)
1.16
1.17 -subsection {* Points *}
1.18 +text {*
1.19 + \index{records|(}%
1.20 + Records are familiar from programming languages. A record of $n$
1.21 + fields is essentially an $n$-tuple, but the record's components have
1.22 + names, which can make expressions easier to read and reduces the
1.23 + risk of confusing one field for another.
1.24 +
1.25 + A basic Isabelle record covers a certain set of fields, with select
1.26 + and update operations. Each field has a specified type, which may
1.27 + be polymorphic. The field names are part of the record type, and
1.28 + the order of the fields is significant --- as it is in Pascal but
1.29 + not in Standard ML. If two different record types have field names
1.30 + in common, then the ambiguity is resolved in the usual way, by
1.31 + qualified names.
1.32 +
1.33 + Record types can also be defined by extending other record types.
1.34 + Extensible records make use of the reserved pseudo-field \cdx{more},
1.35 + which is present in every record type. Generic record operations
1.36 + work on all possible extensions of a given type scheme; naive
1.37 + polymorphism takes care of structural sub-typing behind the scenes.
1.38 + There are also explicit coercion functions between fixed record
1.39 + types.
1.40 +*}
1.41 +
1.42 +
1.43 +subsection {* Record Basics *}
1.44 +
1.45 +text {*
1.46 + Record types are not primitive in Isabelle and have a subtle
1.47 + internal representation based on nested copies of the primitive
1.48 + product type. A \commdx{record} declaration introduces a new record
1.49 + type scheme by specifying its fields, which are packaged internally
1.50 + to hold up the perception of records as a separate concept.
1.51 +*}
1.52
1.53 record point =
1.54 Xcoord :: int
1.55 Ycoord :: int
1.56
1.57 text {*
1.58 - Apart many other things, above record declaration produces the
1.59 - following theorems:
1.60 + Records of type @{typ point} have two fields named @{text Xcoord}
1.61 + and @{text Ycoord}, both of type~@{typ int}. We now define a
1.62 + constant of type @{typ point}:
1.63 *}
1.64
1.65 +constdefs
1.66 + pt1 :: point
1.67 + "pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
1.68
1.69 -thm "point.simps"
1.70 text {*
1.71 -Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
1.72 -Updates, make, make_scheme and equality introduction (extensionality)
1.73 + We see above the ASCII notation for record brackets. You can also
1.74 + use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}. Record type
1.75 + expressions can be written directly as well, without referring to
1.76 + previously declared names (which happen to be mere type
1.77 + abbreviations):
1.78 *}
1.79
1.80 -thm "point.iffs"
1.81 +constdefs
1.82 + pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"
1.83 + "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
1.84 +
1.85 text {*
1.86 -@{thm[display] point.iffs}
1.87 -%%\rulename{point.iffs}
1.88 -Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord)
1.89 + For each field, there is a \emph{selector} function of the same
1.90 + name. For example, if @{text p} has type @{typ point} then @{text
1.91 + "Xcoord p"} denotes the value of the @{text Xcoord} field of~@{text
1.92 + p}. Expressions involving field selection of explicit records are
1.93 + simplified automatically:
1.94 *}
1.95
1.96 -thm "point.update_defs"
1.97 +lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a"
1.98 + by simp
1.99 +
1.100 text {*
1.101 -@{thm[display] point.update_defs}
1.102 -%%\rulename{point.update_defs}
1.103 -Definitions of updates to Xcoord and Ycoord, also "more"
1.104 + The \emph{update} operation is functional. For example, @{term
1.105 + "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord} value is zero
1.106 + and whose @{text Ycoord} value is copied from~@{text p}. Updates
1.107 + are also simplified automatically:
1.108 *}
1.109
1.110 +lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
1.111 + \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
1.112 + by simp
1.113 +
1.114 text {*
1.115 - The set of theorems @{thm [source] point.simps} is added
1.116 - automatically to the standard simpset, @{thm [source] point.iffs} is
1.117 - added to the Classical Reasoner and Simplifier context.
1.118 + \begin{warn}
1.119 + Field names are declared as constants and can no longer be used as
1.120 + variables. It would be unwise, for example, to call the fields of
1.121 + type @{typ point} simply @{text x} and~@{text y}. Each record
1.122 + declaration introduces a constant \cdx{more}.
1.123 + \end{warn}
1.124 *}
1.125
1.126 -text {* Exchanging Xcoord and Ycoord yields a different type: we must
1.127 -unfortunately write the fields in a canonical order.*}
1.128
1.129 -
1.130 -constdefs
1.131 - pt1 :: point
1.132 - "pt1 == (| Xcoord = 999, Ycoord = 23 |)"
1.133 -
1.134 - pt2 :: "(| Xcoord :: int, Ycoord :: int |)"
1.135 - "pt2 == (| Xcoord = -45, Ycoord = 97 |)"
1.136 -
1.137 -
1.138 -subsubsection {* Some lemmas about records *}
1.139 -
1.140 -text {* Basic simplifications. *}
1.141 -
1.142 -lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a"
1.143 -by simp -- "selection"
1.144 -
1.145 -lemma "(| Xcoord = a, Ycoord = b |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b |)"
1.146 -by simp -- "update"
1.147 -
1.148 -
1.149 -subsection {* Coloured points: record extension *}
1.150 -
1.151 +subsection {* Extensible Records and Generic Operations *}
1.152
1.153 text {*
1.154 - Records are extensible.
1.155 -
1.156 - The name@{text "more"} is reserved, since it is used for extensibility.
1.157 + \index{records!extensible|(}%
1.158 +
1.159 + Now, let us define coloured points (type @{text cpoint}) to be
1.160 + points extended with a field @{text col} of type @{text colour}:
1.161 *}
1.162
1.163 -
1.164 datatype colour = Red | Green | Blue
1.165
1.166 record cpoint = point +
1.167 col :: colour
1.168
1.169 +text {*
1.170 + The fields of this new type are @{text Xcoord}, @{text Ycoord} and
1.171 + @{text col}, in that order:
1.172 +*}
1.173
1.174 -constdefs
1.175 +constdefs
1.176 cpt1 :: cpoint
1.177 - "cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
1.178 + "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
1.179
1.180 +text {*
1.181 + We can define generic operations that work on arbitrary instances of
1.182 + a record scheme, e.g.\ covering @{typ point}, @{typ cpoint} and any
1.183 + further extensions. Every record structure has an implicit
1.184 + pseudo-field, \cdx{more}, that keeps the extension as an explicit
1.185 + value. Its type is declared as completely polymorphic:~@{typ 'a}.
1.186 + When a fixed record value is expressed using just its standard
1.187 + fields, the value of @{text more} is implicitly set to @{text "()"},
1.188 + the empty tuple, which has type @{typ unit}. Within the record
1.189 + brackets, you can refer to the @{text more} field by writing @{text
1.190 + "\<dots>"} (three dots):
1.191 +*}
1.192
1.193 -subsection {* Generic operations *}
1.194 +lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a"
1.195 + by simp
1.196
1.197 +text {*
1.198 + This lemma applies to any record whose first two fields are @{text
1.199 + Xcoord} and~@{text Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord
1.200 + = b, \<dots> = ()\<rparr>"} is actually the same as @{text "\<lparr>Xcoord = a,
1.201 + Ycoord = b\<rparr>"}.
1.202
1.203 -text {* Record selection and record update; these are generic! *}
1.204 -
1.205 -lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a"
1.206 -by simp -- "selection"
1.207 + The pseudo-field @{text more} can be selected in the usual way, but
1.208 + the identifier must be qualified:
1.209 +*}
1.210
1.211 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
1.212 -by (simp add: cpt1_def) -- "tail of this record"
1.213 -
1.214 -
1.215 -lemma "(| Xcoord = a, Ycoord = b, ... = p |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b, ... = p |)"
1.216 -by simp -- "update"
1.217 + by (simp add: cpt1_def)
1.218
1.219 text {*
1.220 - Record declarations define new type abbreviations:
1.221 - @{text [display]
1.222 -" point = (| Xcoord :: int, Ycoord :: int |)
1.223 - 'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
1.224 + We see that the colour attached to this @{typ point} is a
1.225 + (rudimentary) record in its own right, namely @{text "\<lparr>col =
1.226 + Green\<rparr>"}. In order to select or update @{text col} in the above
1.227 + fragment, @{text "\<lparr>col = Green\<rparr>"} needs to be put back into the
1.228 + context of its parent type scheme, say as @{text more} part of a
1.229 + @{typ point}.
1.230 +
1.231 + To define generic operations, we need to know a bit more about
1.232 + records. Our declaration of @{typ point} above generated two type
1.233 + abbreviations:
1.234 +
1.235 + \smallskip
1.236 + \begin{tabular}{l}
1.237 + @{typ point}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
1.238 + @{typ "'a point_scheme"}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
1.239 + \end{tabular}
1.240 + \smallskip
1.241 +
1.242 + Type @{typ point} is for rigid records having exactly the two fields
1.243 + @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
1.244 + "'a point_scheme"} comprises all possible extensions to those two
1.245 + fields, recall that @{typ "unit point_scheme"} coincides with @{typ
1.246 + point}. For example, let us define two operations --- methods, if
1.247 + we regard records as objects --- to get and set any point's @{text
1.248 + Xcoord} field.
1.249 *}
1.250
1.251 constdefs
1.252 getX :: "'a point_scheme \<Rightarrow> int"
1.253 - "getX r == Xcoord r"
1.254 - setX :: "['a point_scheme, int] \<Rightarrow> 'a point_scheme"
1.255 - "setX r a == r (| Xcoord := a |)"
1.256 -
1.257 -
1.258 + "getX r \<equiv> Xcoord r"
1.259 + setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme"
1.260 + "setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
1.261
1.262 text {*
1.263 - \medskip Concrete records are type instances of record schemes.
1.264 + Here is a generic method that modifies a point, incrementing its
1.265 + @{text Xcoord} field. The @{text Ycoord} and @{text more} fields
1.266 + are copied across. It works for any record type scheme derived from
1.267 + @{typ point}, such as @{typ cpoint}:
1.268 *}
1.269
1.270 -lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64"
1.271 -by (simp add: getX_def)
1.272 -
1.273 -
1.274 -text {* \medskip Manipulating the `...' (more) part. beware: EACH record
1.275 - has its OWN more field, so a compound name is required! *}
1.276 -
1.277 constdefs
1.278 incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
1.279 - "incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
1.280 -
1.281 -constdefs
1.282 - setGreen :: "[colour, 'a point_scheme] \<Rightarrow> cpoint"
1.283 - "setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)"
1.284 -
1.285 -
1.286 -text {* works (I think) for ALL extensions of type point? *}
1.287 -
1.288 -lemma "incX r = setX r ((getX r) + 1)"
1.289 -by (simp add: getX_def setX_def incX_def)
1.290 -
1.291 -text {* An equivalent definition. *}
1.292 -lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>"
1.293 -by (simp add: incX_def)
1.294 -
1.295 -
1.296 + "incX r \<equiv> \<lparr>Xcoord = Xcoord r + 1,
1.297 + Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
1.298
1.299 text {*
1.300 - Functions on @{text point} schemes work for type @{text cpoint} as
1.301 - well. *}
1.302 + Generic theorems can be proved about generic methods. This trivial
1.303 + lemma relates @{text incX} to @{text getX} and @{text setX}:
1.304 +*}
1.305
1.306 -lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23"
1.307 -by (simp add: getX_def)
1.308 -
1.309 -
1.310 -subsubsection {* Non-coercive structural subtyping *}
1.311 +lemma "incX r = setX r (getX r + 1)"
1.312 + by (simp add: getX_def setX_def incX_def)
1.313
1.314 text {*
1.315 - Function @{term setX} can be applied to type @{typ cpoint}, not just type
1.316 - @{typ point}, and returns a result of the same type! *}
1.317 + \begin{warn}
1.318 + If you use the symbolic record brackets @{text \<lparr>} and @{text \<rparr>},
1.319 + then you must also use the symbolic ellipsis, ``@{text \<dots>}'', rather
1.320 + than three consecutive periods, ``@{text "..."}''. Mixing the ASCII
1.321 + and symbolic versions causes a syntax error. (The two versions are
1.322 + more distinct on screen than they are on paper.)
1.323 + \end{warn}%\index{records!extensible|)}
1.324 +*}
1.325
1.326 -lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 =
1.327 - \<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>"
1.328 -by (simp add: setX_def)
1.329
1.330 +subsection {* Record Equality *}
1.331
1.332 -subsection {* Other features *}
1.333 +text {*
1.334 + Two records are equal\index{equality!of records} if all pairs of
1.335 + corresponding fields are equal. Record equalities are simplified
1.336 + automatically:
1.337 +*}
1.338
1.339 -text {* Field names (and order) contribute to record identity. *}
1.340 +lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) =
1.341 + (a = a' \<and> b = b')"
1.342 + by simp
1.343
1.344 +text {*
1.345 + The following equality is similar, but generic, in that @{text r}
1.346 + can be any instance of @{text point_scheme}:
1.347 +*}
1.348
1.349 -text {* \medskip Polymorphic records. *}
1.350 +lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
1.351 + by simp
1.352
1.353 -record 'a polypoint = point +
1.354 - content :: 'a
1.355 +text {*
1.356 + We see above the syntax for iterated updates. We could equivalently
1.357 + have written the left-hand side as @{term "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord
1.358 + := b\<rparr>"}.
1.359
1.360 -types cpolypoint = "colour polypoint"
1.361 -
1.362 -
1.363 -subsection {* Equality of records. *}
1.364 -
1.365 -lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')"
1.366 - -- "simplification of concrete record equality"
1.367 -by simp
1.368 -
1.369 -text {* \medskip Surjective pairing *}
1.370 + Record equality is \emph{extensional}: \index{extensionality!for
1.371 + records} a record is determined entirely by the values of its
1.372 + fields.
1.373 +*}
1.374
1.375 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
1.376 -by simp
1.377 -
1.378 -
1.379 -
1.380 -lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>"
1.381 -by auto
1.382 + by simp
1.383
1.384 text {*
1.385 - A rigid record has ()::unit in its name@{text "more"} part
1.386 + The generic version of this equality includes the field @{text
1.387 + more}:
1.388 *}
1.389
1.390 -text {* a polymorphic record equality (covers all possible extensions) *}
1.391 -lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
1.392 - -- "introduction of abstract record equality
1.393 - (order of updates doesn't affect the value)"
1.394 -by simp
1.395 -
1.396 -lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
1.397 - -- "abstract record equality (the same with iterated updates)"
1.398 -by simp
1.399 -
1.400 -text {* Showing that repeated updates don't matter *}
1.401 -lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
1.402 -by simp
1.403 -
1.404 -
1.405 -text {* surjective *}
1.406 -
1.407 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
1.408 -by simp
1.409 -
1.410 + by simp
1.411
1.412 text {*
1.413 - \medskip Splitting abstract record variables.
1.414 + Note that the @{text r} is of a different (more general) type than
1.415 + the previous one.
1.416 +
1.417 + \medskip The simplifier can prove many record equalities
1.418 + automatically, but general equality reasoning can be tricky.
1.419 + Consider proving this obvious fact:
1.420 *}
1.421
1.422 -lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.423 - -- "elimination of abstract record equality (manual proof, by selector)"
1.424 -apply (drule_tac f=Xcoord in arg_cong)
1.425 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.426 -by simp
1.427 +lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.428 + apply simp?
1.429 + oops
1.430
1.431 -text {*So we replace the ugly manual proof by the "cases" method.*}
1.432 -lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.433 -apply (cases r)
1.434 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.435 -by simp
1.436 +text {*
1.437 + The simplifier can do nothing, since general record equality is not
1.438 + eliminated automatically. One way to proceed is by an explicit
1.439 + forward step that applies the selector @{text Xcoord} to both sides
1.440 + of the assumed record equality:
1.441 +*}
1.442 +
1.443 +lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.444 + apply (drule_tac f = Xcoord in arg_cong)
1.445 + txt {* @{subgoals [display, indent = 0, margin = 65]}
1.446 + Now, @{text simp} will reduce the assumption to the desired
1.447 + conclusion. *}
1.448 + apply simp
1.449 + done
1.450 +
1.451 +text {*
1.452 + The @{text cases} method is preferable to such a forward proof.
1.453 + State the desired lemma again:
1.454 +*}
1.455 +
1.456 +lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.457 + txt {*
1.458 + The \methdx{cases} method adds an equality to replace the named
1.459 + record variable by an explicit record, listing all fields. It
1.460 + even includes the pseudo-field @{text more}, since the record
1.461 + equality stated above is generic. *}
1.462 + apply (cases r)
1.463 +
1.464 + txt {* @{subgoals [display, indent = 0, margin = 65]}
1.465 + Again, @{text simp} finishes the proof. Because @{text r} has
1.466 + become an explicit record expression, the updates can be applied
1.467 + and the record equality can be replaced by equality of the
1.468 + corresponding fields (due to injectivity). *}
1.469 + apply simp
1.470 + done
1.471 +
1.472 +
1.473 +subsection {* Extending and Truncating Records *}
1.474 +
1.475 +text {*
1.476 + Each record declaration introduces functions to refer collectively
1.477 + to a record's fields and to convert between related record types.
1.478 + They can, for instance, convert between types @{typ point} and @{typ
1.479 + cpoint}. We can add a colour to a point or to convert a @{typ
1.480 + cpoint} to a @{typ point} by forgetting its colour.
1.481 +
1.482 + \begin{itemize}
1.483 +
1.484 + \item Function \cdx{make} takes as arguments all of the record's
1.485 + fields. It returns the corresponding record.
1.486 +
1.487 + \item Function \cdx{fields} takes the record's new fields and
1.488 + returns a record fragment consisting of just those fields. This may
1.489 + be filled into the @{text more} part of the parent record scheme.
1.490 +
1.491 + \item Function \cdx{extend} takes two arguments: a record to be
1.492 + extended and a record containing the new fields.
1.493 +
1.494 + \item Function \cdx{truncate} takes a record (possibly an extension
1.495 + of the original record type) and returns a fixed record, removing
1.496 + any additional fields.
1.497 +
1.498 + \end{itemize}
1.499 +
1.500 + These functions merely provide handsome abbreviations for standard
1.501 + record expressions involving constructors and selectors. The
1.502 + definitions, which are \emph{not} unfolded by default, are made
1.503 + available by the collective name of @{text defs} (e.g.\ @{text
1.504 + point.defs} or @{text cpoint.defs}).
1.505 +
1.506 + For example, here are the versions of those functions generated for
1.507 + record @{typ point}. We omit @{text point.fields}, which happens to
1.508 + be the same as @{text point.make}.
1.509 +
1.510 + @{thm [display, indent = 0, margin = 65] point.make_def
1.511 + point.extend_def point.truncate_def}
1.512 +
1.513 + Contrast those with the corresponding functions for record @{typ
1.514 + cpoint}. Observe @{text cpoint.fields} in particular.
1.515 +
1.516 + @{thm [display, indent = 0, margin = 65] cpoint.make_def
1.517 + cpoint.extend_def cpoint.truncate_def}
1.518 +
1.519 + To demonstrate these functions, we declare a new coloured point by
1.520 + extending an ordinary point. Function @{text point.extend} augments
1.521 + @{text pt1} with a colour, which is converted into an appropriate
1.522 + record fragment by @{text cpoint.fields}.
1.523 +*}
1.524
1.525 constdefs
1.526 cpt2 :: cpoint
1.527 - "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
1.528 + "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
1.529
1.530 text {*
1.531 -@{thm[display] point.defs}
1.532 -*};
1.533 + The coloured points @{text cpt1} and @{text cpt2} are equal. The
1.534 + proof is trivial, by unfolding all the definitions. We deliberately
1.535 + omit the definition of~@{text pt1} in order to reveal the underlying
1.536 + comparison on type @{typ point}.
1.537 +*}
1.538 +
1.539 +lemma "cpt1 = cpt2"
1.540 + apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
1.541 + txt {* @{subgoals [display, indent = 0, margin = 65]} *}
1.542 + apply (simp add: pt1_def)
1.543 + done
1.544
1.545 text {*
1.546 -@{thm[display] cpoint.defs}
1.547 -*};
1.548 -
1.549 -text{*cpt2 is the same as cpt1, but defined by extending point pt1*}
1.550 -lemma "cpt1 = cpt2"
1.551 -apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
1.552 - --{* @{subgoals[display,indent=0,margin=65]} *}
1.553 -by (simp add: pt1_def)
1.554 -
1.555 + In the example below, a coloured point is truncated to leave a
1.556 + point. We must use the @{text truncate} function of the shorter
1.557 + record.
1.558 +*}
1.559
1.560 lemma "point.truncate cpt2 = pt1"
1.561 -by (simp add: pt1_def cpt2_def point.defs)
1.562 + by (simp add: pt1_def cpt2_def point.defs)
1.563
1.564 +text {*
1.565 + \begin{exercise}
1.566 + Extend record @{typ cpoint} to have a further field, @{text
1.567 + intensity}, of type~@{typ nat}. Experiment with coercions among the
1.568 + three record types.
1.569 + \end{exercise}
1.570 +
1.571 + \begin{exercise}
1.572 + (For Java programmers.)
1.573 + Model a small class hierarchy using records.
1.574 + \end{exercise}
1.575 + \index{records|)}
1.576 +*}
1.577 +
1.578 +(*<*)
1.579 end
1.580 +(*>*)