summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Tutorial/Types/Records.thy

author | wenzelm |

Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) | |

changeset 58889 | 5b7a9633cfa8 |

parent 58620 | 7435b6a3f72e |

child 67406 | 23307fd33906 |

permissions | -rw-r--r-- |

modernized header uniformly as section;

2 section {* Records \label{sec:records} *}

4 (*<*)

5 theory Records imports Main begin

6 (*>*)

8 text {*

9 \index{records|(}%

10 Records are familiar from programming languages. A record of $n$

11 fields is essentially an $n$-tuple, but the record's components have

12 names, which can make expressions easier to read and reduces the

13 risk of confusing one field for another.

15 A record of Isabelle/HOL covers a collection of fields, with select

16 and update operations. Each field has a specified type, which may

17 be polymorphic. The field names are part of the record type, and

18 the order of the fields is significant --- as it is in Pascal but

19 not in Standard ML. If two different record types have field names

20 in common, then the ambiguity is resolved in the usual way, by

21 qualified names.

23 Record types can also be defined by extending other record types.

24 Extensible records make use of the reserved pseudo-field \cdx{more},

25 which is present in every record type. Generic record operations

26 work on all possible extensions of a given type scheme; polymorphism

27 takes care of structural sub-typing behind the scenes. There are

28 also explicit coercion functions between fixed record types.

29 *}

32 subsection {* Record Basics *}

34 text {*

35 Record types are not primitive in Isabelle and have a delicate

36 internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on

37 nested copies of the primitive product type. A \commdx{record}

38 declaration introduces a new record type scheme by specifying its

39 fields, which are packaged internally to hold up the perception of

40 the record as a distinguished entity. Here is a simple example:

41 *}

43 record point =

44 Xcoord :: int

45 Ycoord :: int

47 text {*\noindent

48 Records of type @{typ point} have two fields named @{const Xcoord}

49 and @{const Ycoord}, both of type~@{typ int}. We now define a

50 constant of type @{typ point}:

51 *}

53 definition pt1 :: point where

54 "pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"

56 text {*\noindent

57 We see above the ASCII notation for record brackets. You can also

58 use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}. Record type

59 expressions can be also written directly with individual fields.

60 The type name above is merely an abbreviation.

61 *}

63 definition pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>" where

64 "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"

66 text {*

67 For each field, there is a \emph{selector}\index{selector!record}

68 function of the same name. For example, if @{text p} has type @{typ

69 point} then @{text "Xcoord p"} denotes the value of the @{text

70 Xcoord} field of~@{text p}. Expressions involving field selection

71 of explicit records are simplified automatically:

72 *}

74 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a"

75 by simp

77 text {*

78 The \emph{update}\index{update!record} operation is functional. For

79 example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{const Xcoord}

80 value is zero and whose @{const Ycoord} value is copied from~@{text

81 p}. Updates of explicit records are also simplified automatically:

82 *}

84 lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =

85 \<lparr>Xcoord = 0, Ycoord = b\<rparr>"

86 by simp

88 text {*

89 \begin{warn}

90 Field names are declared as constants and can no longer be used as

91 variables. It would be unwise, for example, to call the fields of

92 type @{typ point} simply @{text x} and~@{text y}.

93 \end{warn}

94 *}

97 subsection {* Extensible Records and Generic Operations *}

99 text {*

100 \index{records!extensible|(}%

102 Now, let us define coloured points (type @{text cpoint}) to be

103 points extended with a field @{text col} of type @{text colour}:

104 *}

106 datatype colour = Red | Green | Blue

108 record cpoint = point +

109 col :: colour

111 text {*\noindent

112 The fields of this new type are @{const Xcoord}, @{text Ycoord} and

113 @{text col}, in that order.

114 *}

116 definition cpt1 :: cpoint where

117 "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"

119 text {*

120 We can define generic operations that work on arbitrary

121 instances of a record scheme, e.g.\ covering @{typ point}, @{typ

122 cpoint}, and any further extensions. Every record structure has an

123 implicit pseudo-field, \cdx{more}, that keeps the extension as an

124 explicit value. Its type is declared as completely

125 polymorphic:~@{typ 'a}. When a fixed record value is expressed

126 using just its standard fields, the value of @{text more} is

127 implicitly set to @{text "()"}, the empty tuple, which has type

128 @{typ unit}. Within the record brackets, you can refer to the

129 @{text more} field by writing ``@{text "\<dots>"}'' (three dots):

130 *}

132 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a"

133 by simp

135 text {*

136 This lemma applies to any record whose first two fields are @{text

137 Xcoord} and~@{const Ycoord}. Note that @{text "\<lparr>Xcoord = a, Ycoord

138 = b, \<dots> = ()\<rparr>"} is exactly the same as @{text "\<lparr>Xcoord = a, Ycoord

139 = b\<rparr>"}. Selectors and updates are always polymorphic wrt.\ the

140 @{text more} part of a record scheme, its value is just ignored (for

141 select) or copied (for update).

143 The @{text more} pseudo-field may be manipulated directly as well,

144 but the identifier needs to be qualified:

145 *}

147 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"

148 by (simp add: cpt1_def)

150 text {*\noindent

151 We see that the colour part attached to this @{typ point} is a

152 rudimentary record in its own right, namely @{text "\<lparr>col =

153 Green\<rparr>"}. In order to select or update @{text col}, this fragment

154 needs to be put back into the context of the parent type scheme, say

155 as @{text more} part of another @{typ point}.

157 To define generic operations, we need to know a bit more about

158 records. Our definition of @{typ point} above has generated two

159 type abbreviations:

161 \medskip

162 \begin{tabular}{l}

163 @{typ point}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\

164 @{typ "'a point_scheme"}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\

165 \end{tabular}

166 \medskip

168 \noindent

169 Type @{typ point} is for fixed records having exactly the two fields

170 @{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ

171 "'a point_scheme"} comprises all possible extensions to those two

172 fields. Note that @{typ "unit point_scheme"} coincides with @{typ

173 point}, and @{typ "\<lparr>col :: colour\<rparr> point_scheme"} with @{typ

174 cpoint}.

176 In the following example we define two operations --- methods, if we

177 regard records as objects --- to get and set any point's @{text

178 Xcoord} field.

179 *}

181 definition getX :: "'a point_scheme \<Rightarrow> int" where

182 "getX r \<equiv> Xcoord r"

183 definition setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme" where

184 "setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"

186 text {*

187 Here is a generic method that modifies a point, incrementing its

188 @{const Xcoord} field. The @{text Ycoord} and @{text more} fields

189 are copied across. It works for any record type scheme derived from

190 @{typ point} (including @{typ cpoint} etc.):

191 *}

193 definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" where

194 "incX r \<equiv>

195 \<lparr>Xcoord = Xcoord r + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"

197 text {*

198 Generic theorems can be proved about generic methods. This trivial

199 lemma relates @{const incX} to @{text getX} and @{text setX}:

200 *}

202 lemma "incX r = setX r (getX r + 1)"

203 by (simp add: getX_def setX_def incX_def)

205 text {*

206 \begin{warn}

207 If you use the symbolic record brackets @{text \<lparr>} and @{text \<rparr>},

208 then you must also use the symbolic ellipsis, ``@{text \<dots>}'', rather

209 than three consecutive periods, ``@{text "..."}''. Mixing the ASCII

210 and symbolic versions causes a syntax error. (The two versions are

211 more distinct on screen than they are on paper.)

212 \end{warn}%

213 \index{records!extensible|)}

214 *}

217 subsection {* Record Equality *}

219 text {*

220 Two records are equal\index{equality!of records} if all pairs of

221 corresponding fields are equal. Concrete record equalities are

222 simplified automatically:

223 *}

225 lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) =

226 (a = a' \<and> b = b')"

227 by simp

229 text {*

230 The following equality is similar, but generic, in that @{text r}

231 can be any instance of @{typ "'a point_scheme"}:

232 *}

234 lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"

235 by simp

237 text {*\noindent

238 We see above the syntax for iterated updates. We could equivalently

239 have written the left-hand side as @{text "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord :=

240 b\<rparr>"}.

242 Record equality is \emph{extensional}:

243 \index{extensionality!for records} a record is determined entirely

244 by the values of its fields.

245 *}

247 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"

248 by simp

250 text {*\noindent

251 The generic version of this equality includes the pseudo-field

252 @{text more}:

253 *}

255 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"

256 by simp

258 text {*

259 The simplifier can prove many record equalities

260 automatically, but general equality reasoning can be tricky.

261 Consider proving this obvious fact:

262 *}

264 lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"

265 apply simp?

266 oops

268 text {*\noindent

269 Here the simplifier can do nothing, since general record equality is

270 not eliminated automatically. One way to proceed is by an explicit

271 forward step that applies the selector @{const Xcoord} to both sides

272 of the assumed record equality:

273 *}

275 lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"

276 apply (drule_tac f = Xcoord in arg_cong)

277 txt {* @{subgoals [display, indent = 0, margin = 65]}

278 Now, @{text simp} will reduce the assumption to the desired

279 conclusion. *}

280 apply simp

281 done

283 text {*

284 The @{text cases} method is preferable to such a forward proof. We

285 state the desired lemma again:

286 *}

288 lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"

290 txt {* The \methdx{cases} method adds an equality to replace the

291 named record term by an explicit record expression, listing all

292 fields. It even includes the pseudo-field @{text more}, since the

293 record equality stated here is generic for all extensions. *}

295 apply (cases r)

297 txt {* @{subgoals [display, indent = 0, margin = 65]} Again, @{text

298 simp} finishes the proof. Because @{text r} is now represented as

299 an explicit record construction, the updates can be applied and the

300 record equality can be replaced by equality of the corresponding

301 fields (due to injectivity). *}

303 apply simp

304 done

306 text {*

307 The generic cases method does not admit references to locally bound

308 parameters of a goal. In longer proof scripts one might have to

309 fall back on the primitive @{text rule_tac} used together with the

310 internal field representation rules of records. The above use of

311 @{text "(cases r)"} would become @{text "(rule_tac r = r in

312 point.cases_scheme)"}.

313 *}

316 subsection {* Extending and Truncating Records *}

318 text {*

319 Each record declaration introduces a number of derived operations to

320 refer collectively to a record's fields and to convert between fixed

321 record types. They can, for instance, convert between types @{typ

322 point} and @{typ cpoint}. We can add a colour to a point or convert

323 a @{typ cpoint} to a @{typ point} by forgetting its colour.

325 \begin{itemize}

327 \item Function \cdx{make} takes as arguments all of the record's

328 fields (including those inherited from ancestors). It returns the

329 corresponding record.

331 \item Function \cdx{fields} takes the record's very own fields and

332 returns a record fragment consisting of just those fields. This may

333 be filled into the @{text more} part of the parent record scheme.

335 \item Function \cdx{extend} takes two arguments: a record to be

336 extended and a record containing the new fields.

338 \item Function \cdx{truncate} takes a record (possibly an extension

339 of the original record type) and returns a fixed record, removing

340 any additional fields.

342 \end{itemize}

343 These functions provide useful abbreviations for standard

344 record expressions involving constructors and selectors. The

345 definitions, which are \emph{not} unfolded by default, are made

346 available by the collective name of @{text defs} (@{text

347 point.defs}, @{text cpoint.defs}, etc.).

348 For example, here are the versions of those functions generated for

349 record @{typ point}. We omit @{text point.fields}, which happens to

350 be the same as @{text point.make}.

352 @{thm [display, indent = 0, margin = 65] point.make_def [no_vars]

353 point.extend_def [no_vars] point.truncate_def [no_vars]}

354 Contrast those with the corresponding functions for record @{typ

355 cpoint}. Observe @{text cpoint.fields} in particular.

356 @{thm [display, indent = 0, margin = 65] cpoint.make_def [no_vars]

357 cpoint.fields_def [no_vars] cpoint.extend_def [no_vars]

358 cpoint.truncate_def [no_vars]}

360 To demonstrate these functions, we declare a new coloured point by

361 extending an ordinary point. Function @{text point.extend} augments

362 @{text pt1} with a colour value, which is converted into an

363 appropriate record fragment by @{text cpoint.fields}.

364 *}

366 definition cpt2 :: cpoint where

367 "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"

369 text {*

370 The coloured points @{const cpt1} and @{text cpt2} are equal. The

371 proof is trivial, by unfolding all the definitions. We deliberately

372 omit the definition of~@{text pt1} in order to reveal the underlying

373 comparison on type @{typ point}.

374 *}

376 lemma "cpt1 = cpt2"

377 apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)

378 txt {* @{subgoals [display, indent = 0, margin = 65]} *}

379 apply (simp add: pt1_def)

380 done

382 text {*

383 In the example below, a coloured point is truncated to leave a

384 point. We use the @{text truncate} function of the target record.

385 *}

387 lemma "point.truncate cpt2 = pt1"

388 by (simp add: pt1_def cpt2_def point.defs)

390 text {*

391 \begin{exercise}

392 Extend record @{typ cpoint} to have a further field, @{text

393 intensity}, of type~@{typ nat}. Experiment with generic operations

394 (using polymorphic selectors and updates) and explicit coercions

395 (using @{text extend}, @{text truncate} etc.) among the three record

396 types.

397 \end{exercise}

399 \begin{exercise}

400 (For Java programmers.)

401 Model a small class hierarchy using records.

402 \end{exercise}

403 \index{records|)}

404 *}

406 (*<*)

407 end

408 (*>*)