1.1 --- a/doc-src/TutorialI/Types/Records.thy Fri Dec 21 20:58:25 2001 +0100
1.2 +++ b/doc-src/TutorialI/Types/Records.thy Fri Dec 21 20:58:42 2001 +0100
1.3 @@ -12,7 +12,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 @@ -23,21 +23,20 @@
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 *}
1.24
1.25
1.26 subsection {* Record Basics *}
1.27
1.28 text {*
1.29 - Record types are not primitive in Isabelle and have a subtle
1.30 + Record types are not primitive in Isabelle and have a delicate
1.31 internal representation based on nested copies of the primitive
1.32 product type. A \commdx{record} declaration introduces a new record
1.33 type scheme by specifying its fields, which are packaged internally
1.34 - to hold up the perception of records as a separate concept.
1.35 + to hold up the perception of the record as a distinguished entity.
1.36 *}
1.37
1.38 record point =
1.39 @@ -67,21 +66,21 @@
1.40 "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
1.41
1.42 text {*
1.43 - For each field, there is a \emph{selector} function of the same
1.44 - name. For example, if @{text p} has type @{typ point} then @{text
1.45 - "Xcoord p"} denotes the value of the @{text Xcoord} field of~@{text
1.46 - p}. Expressions involving field selection of explicit records are
1.47 - simplified automatically:
1.48 + For each field, there is a \emph{selector}\index{selector!record}
1.49 + function of the same name. For example, if @{text p} has type @{typ
1.50 + point} then @{text "Xcoord p"} denotes the value of the @{text
1.51 + Xcoord} field of~@{text p}. Expressions involving field selection
1.52 + of explicit records are simplified automatically:
1.53 *}
1.54
1.55 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a"
1.56 by simp
1.57
1.58 text {*
1.59 - The \emph{update} operation is functional. For example, @{term
1.60 - "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord} value is zero
1.61 - and whose @{text Ycoord} value is copied from~@{text p}. Updates
1.62 - are also simplified automatically:
1.63 + The \emph{update}\index{update!record} operation is functional. For
1.64 + example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord}
1.65 + value is zero and whose @{text Ycoord} value is copied from~@{text
1.66 + p}. Updates are also simplified automatically:
1.67 *}
1.68
1.69 lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
1.70 @@ -92,8 +91,7 @@
1.71 \begin{warn}
1.72 Field names are declared as constants and can no longer be used as
1.73 variables. It would be unwise, for example, to call the fields of
1.74 - type @{typ point} simply @{text x} and~@{text y}. Each record
1.75 - declaration introduces a constant \cdx{more}.
1.76 + type @{typ point} simply @{text x} and~@{text y}.
1.77 \end{warn}
1.78 *}
1.79
1.80 @@ -139,12 +137,14 @@
1.81
1.82 text {*
1.83 This lemma applies to any record whose first two fields are @{text
1.84 - Xcoord} and~@{text Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord
1.85 - = b, \<dots> = ()\<rparr>"} is actually the same as @{text "\<lparr>Xcoord = a,
1.86 - Ycoord = b\<rparr>"}.
1.87 + Xcoord} and~@{text Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord =
1.88 + b, \<dots> = ()\<rparr>"} is really the same as @{text "\<lparr>Xcoord = a, Ycoord =
1.89 + b\<rparr>"}. Selectors and updates are always polymorphic wrt.\ the @{text
1.90 + more} part of a record scheme, its value is just ignored (for
1.91 + select) or copied (for update).
1.92
1.93 - The pseudo-field @{text more} can be selected in the usual way, but
1.94 - the identifier must be qualified:
1.95 + The @{text more} pseudo-field may be manipulated directly as well,
1.96 + but the identifier needs to be qualified:
1.97 *}
1.98
1.99 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
1.100 @@ -153,28 +153,30 @@
1.101 text {*
1.102 We see that the colour attached to this @{typ point} is a
1.103 (rudimentary) record in its own right, namely @{text "\<lparr>col =
1.104 - Green\<rparr>"}. In order to select or update @{text col} in the above
1.105 - fragment, @{text "\<lparr>col = Green\<rparr>"} needs to be put back into the
1.106 - context of its parent type scheme, say as @{text more} part of a
1.107 - @{typ point}.
1.108 + Green\<rparr>"}. In order to select or update @{text col}, this fragment
1.109 + needs to be put back into the context of the parent type scheme, say
1.110 + as @{text more} part of another @{typ point}.
1.111
1.112 To define generic operations, we need to know a bit more about
1.113 - records. Our declaration of @{typ point} above generated two type
1.114 + records. Our definition of @{typ point} above generated two type
1.115 abbreviations:
1.116
1.117 - \smallskip
1.118 + \medskip
1.119 \begin{tabular}{l}
1.120 @{typ point}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
1.121 @{typ "'a point_scheme"}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
1.122 \end{tabular}
1.123 - \smallskip
1.124 + \medskip
1.125
1.126 - Type @{typ point} is for rigid records having exactly the two fields
1.127 + Type @{typ point} is for fixed records having exactly the two fields
1.128 @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
1.129 "'a point_scheme"} comprises all possible extensions to those two
1.130 - fields, recall that @{typ "unit point_scheme"} coincides with @{typ
1.131 - point}. For example, let us define two operations --- methods, if
1.132 - we regard records as objects --- to get and set any point's @{text
1.133 + fields. Note that @{typ "unit point_scheme"} coincides with @{typ
1.134 + point}, and @{typ "\<lparr>col :: colour\<rparr> point_scheme"} with @{typ
1.135 + cpoint}.
1.136 +
1.137 + In the following example we define two operations --- methods, if we
1.138 + regard records as objects --- to get and set any point's @{text
1.139 Xcoord} field.
1.140 *}
1.141
1.142 @@ -188,7 +190,7 @@
1.143 Here is a generic method that modifies a point, incrementing its
1.144 @{text Xcoord} field. The @{text Ycoord} and @{text more} fields
1.145 are copied across. It works for any record type scheme derived from
1.146 - @{typ point}, such as @{typ cpoint}:
1.147 + @{typ point} (including @{typ cpoint} etc.):
1.148 *}
1.149
1.150 constdefs
1.151 @@ -229,7 +231,7 @@
1.152
1.153 text {*
1.154 The following equality is similar, but generic, in that @{text r}
1.155 - can be any instance of @{text point_scheme}:
1.156 + can be any instance of @{typ "'a point_scheme"}:
1.157 *}
1.158
1.159 lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
1.160 @@ -237,29 +239,26 @@
1.161
1.162 text {*
1.163 We see above the syntax for iterated updates. We could equivalently
1.164 - have written the left-hand side as @{term "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord
1.165 - := b\<rparr>"}.
1.166 + have written the left-hand side as @{text "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord :=
1.167 + b\<rparr>"}.
1.168
1.169 - Record equality is \emph{extensional}: \index{extensionality!for
1.170 - records} a record is determined entirely by the values of its
1.171 - fields.
1.172 + \medskip Record equality is \emph{extensional}:
1.173 + \index{extensionality!for records} a record is determined entirely
1.174 + by the values of its fields.
1.175 *}
1.176
1.177 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
1.178 by simp
1.179
1.180 text {*
1.181 - The generic version of this equality includes the field @{text
1.182 - more}:
1.183 + The generic version of this equality includes the pseudo-field
1.184 + @{text more}:
1.185 *}
1.186
1.187 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
1.188 by simp
1.189
1.190 text {*
1.191 - Note that the @{text r} is of a different (more general) type than
1.192 - the previous one.
1.193 -
1.194 \medskip The simplifier can prove many record equalities
1.195 automatically, but general equality reasoning can be tricky.
1.196 Consider proving this obvious fact:
1.197 @@ -270,8 +269,8 @@
1.198 oops
1.199
1.200 text {*
1.201 - The simplifier can do nothing, since general record equality is not
1.202 - eliminated automatically. One way to proceed is by an explicit
1.203 + Here the simplifier can do nothing, since general record equality is
1.204 + not eliminated automatically. One way to proceed is by an explicit
1.205 forward step that applies the selector @{text Xcoord} to both sides
1.206 of the assumed record equality:
1.207 *}
1.208 @@ -285,42 +284,54 @@
1.209 done
1.210
1.211 text {*
1.212 - The @{text cases} method is preferable to such a forward proof.
1.213 - State the desired lemma again:
1.214 + The @{text cases} method is preferable to such a forward proof. We
1.215 + state the desired lemma again:
1.216 *}
1.217
1.218 lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
1.219 - txt {*
1.220 - The \methdx{cases} method adds an equality to replace the named
1.221 - record variable by an explicit record, listing all fields. It
1.222 - even includes the pseudo-field @{text more}, since the record
1.223 - equality stated above is generic. *}
1.224 +
1.225 + txt {* The \methdx{cases} method adds an equality to replace the
1.226 + named record term by an explicit record expression, listing all
1.227 + fields. It even includes the pseudo-field @{text more}, since the
1.228 + record equality stated here is generic for all extensions. *}
1.229 +
1.230 apply (cases r)
1.231
1.232 - txt {* @{subgoals [display, indent = 0, margin = 65]}
1.233 - Again, @{text simp} finishes the proof. Because @{text r} has
1.234 - become an explicit record expression, the updates can be applied
1.235 - and the record equality can be replaced by equality of the
1.236 - corresponding fields (due to injectivity). *}
1.237 + txt {* @{subgoals [display, indent = 0, margin = 65]} Again, @{text
1.238 + simp} finishes the proof. Because @{text r} is now represented as
1.239 + an explicit record construction, the updates can be applied and the
1.240 + record equality can be replaced by equality of the corresponding
1.241 + fields (due to injectivity). *}
1.242 +
1.243 apply simp
1.244 done
1.245
1.246 +text {*
1.247 + The generic cases method does not admit references to locally bound
1.248 + parameters of a goal. In longer proof scripts one might have to
1.249 + fall back on the primitive @{text rule_tac} used together with the
1.250 + internal representation rules of records. E.g.\ the above use of
1.251 + @{text "(cases r)"} would become @{text "(rule_tac r = r in
1.252 + point.cases_scheme)"}.
1.253 +*}
1.254 +
1.255
1.256 subsection {* Extending and Truncating Records *}
1.257
1.258 text {*
1.259 - Each record declaration introduces functions to refer collectively
1.260 - to a record's fields and to convert between related record types.
1.261 - They can, for instance, convert between types @{typ point} and @{typ
1.262 - cpoint}. We can add a colour to a point or to convert a @{typ
1.263 - cpoint} to a @{typ point} by forgetting its colour.
1.264 + Each record declaration introduces a number of derived operations to
1.265 + refer collectively to a record's fields and to convert between fixed
1.266 + record types. They can, for instance, convert between types @{typ
1.267 + point} and @{typ cpoint}. We can add a colour to a point or convert
1.268 + a @{typ cpoint} to a @{typ point} by forgetting its colour.
1.269
1.270 \begin{itemize}
1.271
1.272 \item Function \cdx{make} takes as arguments all of the record's
1.273 - fields. It returns the corresponding record.
1.274 + fields (including those inherited from ancestors). It returns the
1.275 + corresponding record.
1.276
1.277 - \item Function \cdx{fields} takes the record's new fields and
1.278 + \item Function \cdx{fields} takes the record's very own fields and
1.279 returns a record fragment consisting of just those fields. This may
1.280 be filled into the @{text more} part of the parent record scheme.
1.281
1.282 @@ -336,26 +347,27 @@
1.283 These functions merely provide handsome abbreviations for standard
1.284 record expressions involving constructors and selectors. The
1.285 definitions, which are \emph{not} unfolded by default, are made
1.286 - available by the collective name of @{text defs} (e.g.\ @{text
1.287 - point.defs} or @{text cpoint.defs}).
1.288 + available by the collective name of @{text defs} (@{text
1.289 + point.defs}, @{text cpoint.defs}, etc.).
1.290
1.291 For example, here are the versions of those functions generated for
1.292 record @{typ point}. We omit @{text point.fields}, which happens to
1.293 be the same as @{text point.make}.
1.294
1.295 - @{thm [display, indent = 0, margin = 65] point.make_def
1.296 - point.extend_def point.truncate_def}
1.297 + @{thm [display, indent = 0, margin = 65] point.make_def [no_vars]
1.298 + point.extend_def [no_vars] point.truncate_def [no_vars]}
1.299
1.300 Contrast those with the corresponding functions for record @{typ
1.301 cpoint}. Observe @{text cpoint.fields} in particular.
1.302
1.303 - @{thm [display, indent = 0, margin = 65] cpoint.make_def
1.304 - cpoint.extend_def cpoint.truncate_def}
1.305 + @{thm [display, indent = 0, margin = 65] cpoint.make_def [no_vars]
1.306 + cpoint.fields_def [no_vars] cpoint.extend_def [no_vars]
1.307 + cpoint.truncate_def [no_vars]}
1.308
1.309 To demonstrate these functions, we declare a new coloured point by
1.310 extending an ordinary point. Function @{text point.extend} augments
1.311 - @{text pt1} with a colour, which is converted into an appropriate
1.312 - record fragment by @{text cpoint.fields}.
1.313 + @{text pt1} with a colour value, which is converted into an
1.314 + appropriate record fragment by @{text cpoint.fields}.
1.315 *}
1.316
1.317 constdefs
1.318 @@ -377,8 +389,7 @@
1.319
1.320 text {*
1.321 In the example below, a coloured point is truncated to leave a
1.322 - point. We must use the @{text truncate} function of the shorter
1.323 - record.
1.324 + point. We use the @{text truncate} function of the target record.
1.325 *}
1.326
1.327 lemma "point.truncate cpt2 = pt1"
1.328 @@ -387,8 +398,10 @@
1.329 text {*
1.330 \begin{exercise}
1.331 Extend record @{typ cpoint} to have a further field, @{text
1.332 - intensity}, of type~@{typ nat}. Experiment with coercions among the
1.333 - three record types.
1.334 + intensity}, of type~@{typ nat}. Experiment with generic operations
1.335 + (using polymorphic selectors and updates) and explicit coercions
1.336 + (using @{text extend}, @{text truncate} etc.) among the three record
1.337 + types.
1.338 \end{exercise}
1.339
1.340 \begin{exercise}