1.1 --- a/doc-src/TutorialI/Types/records.tex Thu Dec 20 21:13:36 2001 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,342 +0,0 @@
1.4 -\section{Records}
1.5 -\label{sec:records}
1.6 -
1.7 -\index{records|(}%
1.8 -Records are familiar from programming languages. A record of $n$
1.9 -fields is essentially an $n$-tuple, but the record's components have
1.10 -names, which can make expressions easier to read and reduces the risk
1.11 -of confusing one field for another.
1.12 -
1.13 -A basic Isabelle record has a fixed set of fields, with access
1.14 -and update operations. Each field has a specified type, which may be
1.15 -polymorphic. The field names are part of the record type, and the
1.16 -order of the fields is significant --- as it is in Pascal but not in
1.17 -Standard ML. If two different record types have fields in common,
1.18 -then the ambiguity is resolved in the usual way, by qualified names.
1.19 -
1.20 -Record types can also be defined by extending other record types.
1.21 -Extensible records make use of the reserved field \cdx{more}, which is
1.22 -present in every record type. Generic methods, or operations that
1.23 -work on all possible extensions of a given record, can be expressed by
1.24 -definitions involving \isa{more}, but the details are complicated.
1.25 -
1.26 -\subsection{Record Basics}
1.27 -
1.28 -Record types are not primitive in Isabelle and have a complex internal
1.29 -representation. A \commdx{record} declaration
1.30 -introduces a new record type:
1.31 -\begin{isabelle}
1.32 -\isacommand{record}\ point\ =\isanewline
1.33 -\ \ Xcoord\ ::\ int\isanewline
1.34 -\ \ Ycoord\ ::\ int
1.35 -\end{isabelle}
1.36 -
1.37 -Records of type \isa{point} have two fields named \isa{Xcoord} and \isa{Ycoord},
1.38 -both of type~\isa{int}. We now declare a constant of type
1.39 -\isa{point}:
1.40 -\begin{isabelle}
1.41 -\isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline
1.42 -\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)"
1.43 -\end{isabelle}
1.44 -We see above the ASCII notation for record brackets. You can also use
1.45 -the symbolic brackets \isa{\isasymlparr} and \isa{\isasymrparr}.
1.46 -Record types can be written directly, without referring to
1.47 -previously declared names:
1.48 -\begin{isabelle}
1.49 -\isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\
1.50 -|)"\ \isanewline
1.51 -\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)"
1.52 -\end{isabelle}
1.53 -
1.54 -For each field, there is a \emph{selector} function of the same name. For
1.55 -example, if \isa{p} has type \isa{point} then \isa{Xcoord p} denotes the
1.56 -value of the \isa{Xcoord} field of~\isa{p}. Expressions involving field
1.57 -selection are simplified automatically:
1.58 -\begin{isabelle}
1.59 -\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ =\ a"\isanewline
1.60 -\isacommand{by}\ simp
1.61 -\end{isabelle}
1.62 -The \emph{update} operation is functional. For example,
1.63 -\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value
1.64 -is zero and whose
1.65 -\isa{Ycoord} value is copied from~\isa{p}. Updates are also simplified
1.66 -automatically:
1.67 -\begin{isabelle}
1.68 -\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\
1.69 -=\isanewline
1.70 -\ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline
1.71 -\isacommand{by}\ simp
1.72 -\end{isabelle}
1.73 -
1.74 -\begin{warn}
1.75 -Field names are declared as constants and can no longer be
1.76 -used as variables. It would be unwise, for example, to call the fields
1.77 -of type \isa{point} simply \isa{x} and~\isa{y}. Each record
1.78 -declaration introduces a constant \cdx{more}.
1.79 -\end{warn}
1.80 -
1.81 -
1.82 -\subsection{Extensible Records and Generic Operations}
1.83 -
1.84 -\index{records!extensible|(}%
1.85 -Now, let us define coloured points
1.86 -(type \isa{cpoint}) to be points extended with a field \isa{col} of type
1.87 -\isa{colour}:
1.88 -\begin{isabelle}
1.89 -\isacommand{datatype}\ colour\ =\ Red\ |\ Green\ |\
1.90 -Blue\isanewline
1.91 -\isanewline
1.92 -\isacommand{record}\ cpoint\ =\ point\ +\isanewline
1.93 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ col\ ::\ colour
1.94 -\end{isabelle}
1.95 -
1.96 -The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and \isa{col}, in that
1.97 -order:
1.98 -\begin{isabelle}
1.99 -\isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline
1.100 -\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\
1.101 -=\ Green\ |)"
1.102 -\end{isabelle}
1.103 -
1.104 -
1.105 -We can define generic operations that work on type \isa{point} and all
1.106 -extensions of it.
1.107 -Every record structure has an implicit field, \cdx{more}, to allow
1.108 -extension. Its type is completely polymorphic:~\isa{'a}. When a
1.109 -record value is expressed using just its standard fields, the value of
1.110 -\isa{more} is implicitly set to \isa{()}, the empty tuple, which has
1.111 -type \isa{unit}. Within the record brackets, you can refer to the
1.112 -\isa{more} field by writing \isa{...} (three periods):
1.113 -\begin{isabelle}
1.114 -\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b,\ ...\ =\ p\ |)\ =\ a"
1.115 -\end{isabelle}
1.116 -This lemma (trivially proved using \isa{simp}) applies to any
1.117 -record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Field
1.118 -\isa{more} can be selected in the usual way, but as all records have
1.119 -this field, the identifier must be qualified:
1.120 -\begin{isabelle}
1.121 -\isacommand{lemma}\ "point.more\ cpt1\ =\ \isasymlparr col\ =\ Green\isasymrparr "\isanewline
1.122 -\isacommand{by}\ (simp\ add:\ cpt1_def)
1.123 -\end{isabelle}
1.124 -%
1.125 -We see that the colour attached to this \isa{point} is a record in its
1.126 -own right, namely
1.127 -\isa{\isasymlparr col\ =\ Green\isasymrparr}.
1.128 -
1.129 -To define generic operations, we need to know a bit more about records.
1.130 -Our declaration of \isa{point} above generated two type
1.131 -abbreviations:
1.132 -\begin{isabelle}
1.133 -\ \ \ \ point\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\ |)\isanewline
1.134 -\ \ \ \ 'a\ point_scheme\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int,\ ...\ ::\ 'a\ |)
1.135 -\end{isabelle}
1.136 -%
1.137 -Type \isa{point} is for rigid records having the two fields
1.138 -\isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{'a\ point_scheme}
1.139 -comprises all possible extensions to those two fields. For example,
1.140 -let us define two operations --- methods, if we regard records as
1.141 -objects --- to get and set any point's
1.142 -\isa{Xcoord} field.
1.143 -\begin{isabelle}
1.144 -\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline
1.145 -\ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
1.146 -\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
1.147 -\ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)"
1.148 -\end{isabelle}
1.149 -
1.150 -Here is a generic method that modifies a point, incrementing its
1.151 -\isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields
1.152 -are copied across. It works for type \isa{point} and any of its
1.153 -extensions, such as \isa{cpoint}:
1.154 -\begin{isabelle}
1.155 -\isacommand{constdefs}\isanewline
1.156 -\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
1.157 -\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline
1.158 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline
1.159 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\
1.160 -r\isasymrparr"
1.161 -\end{isabelle}
1.162 -
1.163 -Generic theorems can be proved about generic methods. This trivial
1.164 -lemma relates \isa{incX} to \isa{getX} and \isa{setX}:
1.165 -\begin{isabelle}
1.166 -\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline
1.167 -\isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def)
1.168 -\end{isabelle}
1.169 -
1.170 -\begin{warn}
1.171 -If you use the symbolic record brackets \isa{\isasymlparr} and
1.172 -\isa{\isasymrparr}, then you must also use the symbolic ellipsis,
1.173 -\isa{\isasymdots}, rather than three consecutive periods,
1.174 -\isa{...}. Mixing the ASCII and symbolic versions
1.175 -causes a syntax error. (The two versions are more
1.176 -distinct on screen than they are on paper.)
1.177 -\end{warn}%
1.178 -\index{records!extensible|)}
1.179 -
1.180 -
1.181 -\subsection{Record Equality}
1.182 -
1.183 -Two records are equal\index{equality!of records}
1.184 -if all pairs of corresponding fields are equal.
1.185 -Record equalities are simplified automatically:
1.186 -\begin{isabelle}
1.187 -\isacommand{lemma}\ "(\isasymlparr Xcoord\ =\ a,\ Ycoord\ =\ b\isasymrparr \ =\ \isasymlparr Xcoord\ =\ a',\ Ycoord\ =\ b'\isasymrparr )\
1.188 -=\isanewline
1.189 -\ \ \ \ \ \ \ \ (a\ =\ a'\ \&\ b\ =\ b')"\isanewline
1.190 -\isacommand{by}\ simp
1.191 -\end{isabelle}
1.192 -
1.193 -The following equality is similar, but generic, in that \isa{r} can
1.194 -be any instance of \isa{point_scheme}:
1.195 -\begin{isabelle}
1.196 -\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a,\ Ycoord\ :=\
1.197 -b\isasymrparr \ =\ r\ \isasymlparr Ycoord\ :=\ b,\ Xcoord\ :=\
1.198 -a\isasymrparr "\isanewline
1.199 -\isacommand{by}\ simp
1.200 -\end{isabelle}
1.201 -We see above the syntax for iterated updates. We could equivalently
1.202 -have written the left-hand side as
1.203 -\isa{r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ \isasymlparr
1.204 -Ycoord\ :=\ b\isasymrparr}.
1.205 -
1.206 -Record equality is \emph{extensional}:
1.207 -\index{extensionality!for records}
1.208 -a record is determined entirely by the values of its fields.
1.209 -\begin{isabelle}
1.210 -\isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\
1.211 -Ycoord\ r\isasymrparr "\isanewline
1.212 -\isacommand{by}\ simp
1.213 -\end{isabelle}
1.214 -The generic version of this equality includes the field \isa{more}:
1.215 -\begin{isabelle}
1.216 -\ \ \ \ r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ Ycoord\ r,\ \isasymdots \ =\ point.more\
1.217 -r\isasymrparr
1.218 -\end{isabelle}
1.219 -
1.220 -\medskip
1.221 -The simplifier can prove many record equalities automatically,
1.222 -but general equality reasoning can be tricky. Consider proving this
1.223 -obvious fact:
1.224 -\begin{isabelle}
1.225 -\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\
1.226 -a'"
1.227 -\end{isabelle}
1.228 -The simplifier can do nothing. One way to proceed is by an explicit
1.229 -forward step that applies the selector \isa{Xcoord} to both sides
1.230 -of the assumed record equality:
1.231 -\begin{isabelle}
1.232 -\isacommand{apply}\ (drule_tac\ f=Xcoord\ \isakeyword{in}\ arg_cong)\isanewline
1.233 -\ 1.\ Xcoord\ (r\isasymlparr Xcoord\ :=\ a\isasymrparr )\ =\ Xcoord\
1.234 -(r\isasymlparr Xcoord\ :=\ a'\isasymrparr )\ \isasymLongrightarrow \
1.235 -a\ =\ a'
1.236 -\end{isabelle}
1.237 -Now, \isa{simp} will reduce the assumption to the desired
1.238 -conclusion.
1.239 -
1.240 -The \isa{cases} method is preferable to such a forward proof.
1.241 -State the desired lemma again:
1.242 -\begin{isabelle}
1.243 -\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\ a'"
1.244 -\end{isabelle}
1.245 -The \methdx{cases} method adds an equality to replace
1.246 -the named record variable by an explicit record, listing all fields.
1.247 -It even includes the field \isa{more}, since the record equality is generic.
1.248 -\begin{isabelle}
1.249 -\isacommand{apply}\ (cases\ r)\isanewline
1.250 -\ 1.\ \isasymAnd Xcoord\ Ycoord\ more.\isanewline
1.251 -\isaindent{\ 1.\ \ \ \ }\isasymlbrakk r\isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\isasymlparr Xcoord\ :=\ a'\isasymrparr ;\isanewline
1.252 -\isaindent{\ 1.\ \ \ \ \ \ \ }r\ =\ \isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isasymrbrakk \isanewline
1.253 -\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ a\ =\ a'
1.254 -\end{isabelle}
1.255 -Again, \isa{simp} finishes the proof. Because \isa{r} has become an explicit
1.256 -record expression, the updates can be applied and the record equality can be
1.257 -replaced by equality of the corresponding fields.
1.258 -
1.259 -
1.260 -\subsection{Extending and Truncating Records}
1.261 -
1.262 -Each record declaration introduces functions to refer collectively to a
1.263 -record's fields and to convert between related record types. They can, for
1.264 -instance, convert between types \isa{point} and \isa{cpoint}. We can add a
1.265 -colour to a point or to convert a \isa{cpoint} to a \isa{point} by forgetting
1.266 -its colour.
1.267 -
1.268 -\begin{itemize}
1.269 -\item Function \isa{make} takes as arguments all of the record's fields.
1.270 - It returns the corresponding record.
1.271 -\item If the record type is an extension of another,
1.272 - function \isa{fields} takes the record's new fields
1.273 - and returns a record consisting of just those fields.
1.274 -\item Function \isa{extend} takes two arguments: a record to be extended and a
1.275 - record containing the new fields.
1.276 -\item Function \isa{truncate} takes a record (possibly an extension of the
1.277 - original record type) and returns a record of the original type, deleting
1.278 - any additional fields.
1.279 -\end{itemize}
1.280 -
1.281 -For example, here are the versions of those functions generated for record
1.282 -\isa{point}. We omit \isa{point.fields}, which is the same as
1.283 -\isa{point.make}.
1.284 -\begin{isabelle}
1.285 -point.make\ ?Xcoord\ ?Ycoord\ \isasymequiv \isanewline\smallskip
1.286 -\ \ \isasymlparr Xcoord\ =\ ?Xcoord,\ Ycoord\ =\ ?Ycoord\isasymrparr \isanewline
1.287 -point.extend\ ?r\ ?more\ \isasymequiv \isanewline\smallskip
1.288 -\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ \isasymdots \ =\ ?more\isasymrparr \isanewline\smallskip
1.289 -point.truncate\ ?r\ \isasymequiv \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r\isasymrparr
1.290 -\end{isabelle}
1.291 -
1.292 -Contrast those with the corresponding functions for record \isa{cpoint}.
1.293 -Observe \isa{cpoint.fields} in particular.
1.294 -\begin{isabelle}
1.295 -cpoint.make\ ?Xcoord\ ?Ycoord\ ?col\ \isasymequiv \isanewline
1.296 -\ \ \isasymlparr Xcoord\ =\ ?Xcoord,\ Ycoord\ =\ ?Ycoord,\ col\ =\ ?col\isasymrparr \par\smallskip
1.297 -cpoint.fields\ ?col\ \isasymequiv \ \isasymlparr col\ =\ ?col\isasymrparr \par\smallskip
1.298 -cpoint.extend\ ?r\ ?more\ \isasymequiv \par
1.299 -\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ col\ =\ col\ ?r,\isanewline
1.300 -\isaindent{\ \ \ }\isasymdots \ =\ ?more\isasymrparr \par\smallskip
1.301 -cpoint.truncate\ ?r\ \isasymequiv \par
1.302 -\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ col\ =\ col\ ?r\isasymrparr
1.303 -\end{isabelle}
1.304 -
1.305 -To demonstrate these functions, we declare a new coloured point by extending
1.306 -an ordinary point. Function \isa{point.extend} augments \isa{pt1} with a
1.307 -colour, which is converted into a record by \isa{cpoint.fields}.
1.308 -\begin{isabelle}
1.309 -\isacommand{constdefs}\isanewline
1.310 -\ \ cpt2\ ::\ cpoint\isanewline
1.311 -\ \ \ "cpt2\ \isasymequiv\ point.extend\ pt1\ (cpoint.fields\ Green)"\isamarkupfalse%
1.312 -\end{isabelle}
1.313 -
1.314 -The coloured points \isa{cpt1} and \isa{cpt2} are equal. The proof is
1.315 -trivial, by unfolding all the definitions. We deliberately omit the
1.316 -definition of~\isa{pt1} in order to reveal the underlying comparison on type
1.317 -\isa{point}.
1.318 -\begin{isabelle}
1.319 -\isacommand{lemma}\ "cpt1\ =\ cpt2"\isanewline
1.320 -\isacommand{apply}\ (simp\ add:\ cpt1_def\ cpt2_def\ point.defs\ cpoint.defs)\isanewline
1.321 -\ 1.\ Xcoord\ pt1\ =\ 999\ \isasymand \ Ycoord\ pt1\ =\ 23
1.322 -\par\smallskip
1.323 -\isacommand{by}\ (simp\ add:\ pt1_def)
1.324 -\end{isabelle}
1.325 -
1.326 -In the example below, a coloured point is truncated to leave a point.
1.327 -We must use the \isa{truncate} function of the shorter record.
1.328 -\begin{isabelle}
1.329 -\isacommand{lemma}\ "point.truncate\ cpt2\ =\ pt1"\isanewline
1.330 -\isacommand{by}\ (simp\ add:\ pt1_def\ cpt2_def\ point.defs)
1.331 -\end{isabelle}
1.332 -
1.333 -\begin{exercise}
1.334 -Extend record \isa{cpoint} to have a further field, \isa{intensity}, of
1.335 -type~\isa{nat}. Experiment with coercions among the three record types.
1.336 -\end{exercise}
1.337 -
1.338 -\begin{exercise}
1.339 -(For Java programmers.)
1.340 -Model a small class hierarchy using records.
1.341 -\end{exercise}
1.342 -\index{records|)}
1.343 -
1.344 -\endinput
1.345 -