12567

1 


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


3 


4 
(*<*)

16417

5 
theory Records imports Main begin

12567

6 
(*>*)


7 


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.

11387

14 

12586

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

12567

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.

11387

22 

12567

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


24 
Extensible records make use of the reserved pseudofield \cdx{more},


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

12586

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


27 
takes care of structural subtyping behind the scenes. There are


28 
also explicit coercion functions between fixed record types.

12567

29 
*}


30 

11387

31 

12567

32 
subsection {* Record Basics *}


33 


34 
text {*

12586

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

12655

36 
internal representation \cite{NaraschewskiWTPHOLs98}, 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

12700

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

12567

41 
*}

11387

42 


43 
record point =


44 
Xcoord :: int


45 
Ycoord :: int


46 

27015

47 
text {*\noindent

15905

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

12567

50 
constant of type @{typ point}:


51 
*}


52 

27015

53 
definition pt1 :: point where


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

12567

55 

27015

56 
text {*\noindent

12567

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

12655

59 
expressions can be also written directly with individual fields.

12700

60 
The type name above is merely an abbreviation.

12567

61 
*}


62 

27015

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


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

12567

65 


66 
text {*

12586

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:

12567

72 
*}


73 


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


75 
by simp


76 


77 
text {*

12586

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

15905

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

12655

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

12567

82 
*}


83 


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

27015

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

12567

86 
by simp


87 


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

12586

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

12567

93 
\end{warn}

11387

94 
*}


95 

11428

96 

12567

97 
subsection {* Extensible Records and Generic Operations *}

11387

98 


99 
text {*

12567

100 
\index{records!extensible(}%

11387

101 

12567

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


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

11387

104 
*}


105 


106 
datatype colour = Red  Green  Blue


107 


108 
record cpoint = point +


109 
col :: colour


110 

27015

111 
text {*\noindent

15905

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

12655

113 
@{text col}, in that order.

12567

114 
*}

11387

115 

27015

116 
definition cpt1 :: cpoint where


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

11387

118 

12567

119 
text {*

27015

120 
We can define generic operations that work on arbitrary

12657

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 pseudofield, \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):

12567

130 
*}

11387

131 

12567

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


133 
by simp

11387

134 

12567

135 
text {*


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

15905

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

12655

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

12586

141 
select) or copied (for update).

12567

142 

12586

143 
The @{text more} pseudofield may be manipulated directly as well,


144 
but the identifier needs to be qualified:

12567

145 
*}

11387

146 


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

12567

148 
by (simp add: cpt1_def)

11387

149 

27015

150 
text {*\noindent

12655

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

12700

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

12586

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}.

12567

156 


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

12655

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


159 
type abbreviations:

12567

160 

12586

161 
\medskip

12567

162 
\begin{tabular}{l}

27015

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>"} \\

12567

165 
\end{tabular}

12586

166 
\medskip

27015

167 


168 
\noindent

12586

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

15905

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

12567

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

12586

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}.


175 


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

12567

178 
Xcoord} field.

11387

179 
*}


180 

27015

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>"

11387

185 


186 
text {*

12567

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

15905

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

12567

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

12586

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

11387

191 
*}


192 

27015

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>"

11387

196 


197 
text {*

12567

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

15905

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

12567

200 
*}

11387

201 

12567

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


203 
by (simp add: getX_def setX_def incX_def)

11387

204 


205 
text {*

12567

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.)

12634

212 
\end{warn}%


213 
\index{records!extensible)}

12567

214 
*}

11387

215 


216 

12567

217 
subsection {* Record Equality *}


218 


219 
text {*


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

12655

221 
corresponding fields are equal. Concrete record equalities are


222 
simplified automatically:

12567

223 
*}


224 


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


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


227 
by simp

11387

228 

12567

229 
text {*


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

12586

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

12567

232 
*}


233 


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


235 
by simp

11387

236 

27015

237 
text {*\noindent

12567

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

12586

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


240 
b\<rparr>"}.

12567

241 

27015

242 
Record equality is \emph{extensional}:

12586

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


244 
by the values of its fields.

12567

245 
*}

11387

246 


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

12567

248 
by simp

11387

249 

27015

250 
text {*\noindent

12586

251 
The generic version of this equality includes the pseudofield


252 
@{text more}:

12567

253 
*}

11387

254 

12567

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


256 
by simp

11387

257 


258 
text {*

27015

259 
The simplifier can prove many record equalities

12567

260 
automatically, but general equality reasoning can be tricky.


261 
Consider proving this obvious fact:


262 
*}


263 


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


265 
apply simp?


266 
oops


267 

27015

268 
text {*\noindent

12586

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


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

15905

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

12567

272 
of the assumed record equality:

11387

273 
*}


274 

12567

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


282 


283 
text {*

12586

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


285 
state the desired lemma again:

12567

286 
*}

11387

287 

12567

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

12586

289 


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 pseudofield @{text more}, since the


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


294 

12567

295 
apply (cases r)

11387

296 

12586

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). *}


302 

12567

303 
apply simp


304 
done

11387

305 

12586

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

12657

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


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

12586

312 
point.cases_scheme)"}.


313 
*}


314 

11387

315 

12567

316 
subsection {* Extending and Truncating Records *}

11387

317 


318 
text {*

12586

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.

12567

324 


325 
\begin{itemize}


326 


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

12586

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


329 
corresponding record.

12567

330 

12586

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

12567

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.


334 


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


336 
extended and a record containing the new fields.


337 


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.


341 


342 
\end{itemize}

12700

343 
These functions provide useful abbreviations for standard

12567

344 
record expressions involving constructors and selectors. The


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

12586

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


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

12567

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}.

11387

351 

12586

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


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

12567

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


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

12586

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]}

12567

359 


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


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

12586

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


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

12567

364 
*}

11387

365 

27015

366 
definition cpt2 :: cpoint where


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

12407

368 


369 
text {*

15905

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

12567

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 
*}


375 


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

12407

381 


382 
text {*

12567

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

12586

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

12567

385 
*}

12407

386 


387 
lemma "point.truncate cpt2 = pt1"

12567

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


389 


390 
text {*


391 
\begin{exercise}


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

12586

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.

12567

397 
\end{exercise}

12407

398 

12567

399 
\begin{exercise}


400 
(For Java programmers.)


401 
Model a small class hierarchy using records.


402 
\end{exercise}


403 
\index{records)}


404 
*}


405 


406 
(*<*)

11387

407 
end

12567

408 
(*>*)
