# HG changeset patch # User wenzelm # Date 1008879299 -3600 # Node ID f8ad8cfb83092dd4603bc790b76419ca49d144cc # Parent 0000276024e5d4f48c639e0ccab85417e8e790fd generated text; diff -r 0000276024e5 -r f8ad8cfb8309 doc-src/TutorialI/Types/document/Records.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Types/document/Records.tex Thu Dec 20 21:14:59 2001 +0100 @@ -0,0 +1,448 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Records}% +% +\isamarkupheader{Records \label{sec:records}% +} +\isamarkuptrue% +\isamarkupfalse% +% +\begin{isamarkuptext}% +\index{records|(}% + Records are familiar from programming languages. A record of $n$ + fields is essentially an $n$-tuple, but the record's components have + names, which can make expressions easier to read and reduces the + risk of confusing one field for another. + + A basic Isabelle record covers a certain set of fields, with select + and update operations. Each field has a specified type, which may + be polymorphic. The field names are part of the record type, and + the order of the fields is significant --- as it is in Pascal but + not in Standard ML. If two different record types have field names + in common, then the ambiguity is resolved in the usual way, by + qualified names. + + Record types can also be defined by extending other record types. + Extensible records make use of the reserved pseudo-field \cdx{more}, + which is present in every record type. Generic record operations + work on all possible extensions of a given type scheme; naive + polymorphism takes care of structural sub-typing behind the scenes. + There are also explicit coercion functions between fixed record + types.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record Basics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Record types are not primitive in Isabelle and have a subtle + internal representation based on nested copies of the primitive + product type. A \commdx{record} declaration introduces a new record + type scheme by specifying its fields, which are packaged internally + to hold up the perception of records as a separate concept.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{record}\ point\ {\isacharequal}\isanewline +\ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline +\ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int\isamarkupfalse% +% +\begin{isamarkuptext}% +Records of type \isa{point} have two fields named \isa{Xcoord} + and \isa{Ycoord}, both of type~\isa{int}. We now define a + constant of type \isa{point}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\isanewline +\ \ {\isachardoublequote}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +We see above the ASCII notation for record brackets. You can also + use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}. Record type + expressions can be written directly as well, without referring to + previously declared names (which happen to be mere type + abbreviations):% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +For each field, there is a \emph{selector} function of the same + name. For example, if \isa{p} has type \isa{point} then \isa{Xcoord\ p} denotes the value of the \isa{Xcoord} field of~\isa{p}. Expressions involving field selection of explicit records are + simplified automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +The \emph{update} operation is functional. For example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord} value is zero + and whose \isa{Ycoord} value is copied from~\isa{p}. Updates + are also simplified automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline +\ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +\begin{warn} + Field names are declared as constants and can no longer be used as + variables. It would be unwise, for example, to call the fields of + type \isa{point} simply \isa{x} and~\isa{y}. Each record + declaration introduces a constant \cdx{more}. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Extensible Records and Generic Operations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{records!extensible|(}% + + Now, let us define coloured points (type \isa{cpoint}) to be + points extended with a field \isa{col} of type \isa{colour}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\ colour\ {\isacharequal}\ Red\ {\isacharbar}\ Green\ {\isacharbar}\ Blue\isanewline +\isanewline +\isamarkupfalse% +\isacommand{record}\ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline +\ \ col\ {\isacharcolon}{\isacharcolon}\ colour\isamarkupfalse% +% +\begin{isamarkuptext}% +The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and + \isa{col}, in that order:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline +\ \ {\isachardoublequote}cpt{\isadigit{1}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}{\isacharcomma}\ col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +We can define generic operations that work on arbitrary instances of + a record scheme, e.g.\ covering \isa{point}, \isa{cpoint} and any + further extensions. Every record structure has an implicit + pseudo-field, \cdx{more}, that keeps the extension as an explicit + value. Its type is declared as completely polymorphic:~\isa{{\isacharprime}a}. + When a fixed record value is expressed using just its standard + fields, the value of \isa{more} is implicitly set to \isa{{\isacharparenleft}{\isacharparenright}}, + the empty tuple, which has type \isa{unit}. Within the record + brackets, you can refer to the \isa{more} field by writing \isa{{\isasymdots}} (three dots):% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Note that \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}} is actually the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}. + + The pseudo-field \isa{more} can be selected in the usual way, but + the identifier must be qualified:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptext}% +We see that the colour attached to this \isa{point} is a + (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col} in the above + fragment, \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}} needs to be put back into the + context of its parent type scheme, say as \isa{more} part of a + \isa{point}. + + To define generic operations, we need to know a bit more about + records. Our declaration of \isa{point} above generated two type + abbreviations: + + \smallskip + \begin{tabular}{l} + \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\ + \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\ + \end{tabular} + \smallskip + + Type \isa{point} is for rigid records having exactly the two fields + \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two + fields, recall that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}. For example, let us define two operations --- methods, if + we regard records as objects --- to get and set any point's \isa{Xcoord} field.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequote}\isanewline +\ \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +Here is a generic method that modifies a point, incrementing its + \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields + are copied across. It works for any record type scheme derived from + \isa{point}, such as \isa{cpoint}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline +\ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\isanewline +\ \ \ \ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +Generic theorems can be proved about generic methods. This trivial + lemma relates \isa{incX} to \isa{getX} and \isa{setX}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptext}% +\begin{warn} + If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}, + then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather + than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''. Mixing the ASCII + and symbolic versions causes a syntax error. (The two versions are + more distinct on screen than they are on paper.) + \end{warn}%\index{records!extensible|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record Equality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Two records are equal\index{equality!of records} if all pairs of + corresponding fields are equal. Record equalities are simplified + automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharprime}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isacharequal}\isanewline +\ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +The following equality is similar, but generic, in that \isa{r} + can be any instance of \isa{point{\isacharunderscore}scheme}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +We see above the syntax for iterated updates. We could equivalently + have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}. + + Record equality is \emph{extensional}: \index{extensionality!for + records} a record is determined entirely by the values of its + fields.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +The generic version of this equality includes the field \isa{more}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ simp\isamarkupfalse% +% +\begin{isamarkuptext}% +Note that the \isa{r} is of a different (more general) type than + the previous one. + + \medskip The simplifier can prove many record equalities + automatically, but general equality reasoning can be tricky. + Consider proving this obvious fact:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}\ simp{\isacharquery}\isanewline +\ \ \isamarkupfalse% +\isacommand{oops}\isamarkupfalse% +% +\begin{isamarkuptext}% +The simplifier can do nothing, since general record equality is not + eliminated automatically. One way to proceed is by an explicit + forward step that applies the selector \isa{Xcoord} to both sides + of the assumed record equality:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isacharparenright}\ {\isacharequal}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}% +\end{isabelle} + Now, \isa{simp} will reduce the assumption to the desired + conclusion.% +\end{isamarkuptxt}% +\ \ \isamarkuptrue% +\isacommand{apply}\ simp\isanewline +\ \ \isamarkupfalse% +\isacommand{done}\isamarkupfalse% +% +\begin{isamarkuptext}% +The \isa{cases} method is preferable to such a forward proof. + State the desired lemma again:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptxt}% +The \methdx{cases} method adds an equality to replace the named + record variable by an explicit record, listing all fields. It + even includes the pseudo-field \isa{more}, since the record + equality stated above is generic.% +\end{isamarkuptxt}% +\ \ \isamarkuptrue% +\isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}% +\end{isabelle} + Again, \isa{simp} finishes the proof. Because \isa{r} has + become an explicit record expression, the updates can be applied + and the record equality can be replaced by equality of the + corresponding fields (due to injectivity).% +\end{isamarkuptxt}% +\ \ \isamarkuptrue% +\isacommand{apply}\ simp\isanewline +\ \ \isamarkupfalse% +\isacommand{done}\isamarkupfalse% +% +\isamarkupsubsection{Extending and Truncating Records% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Each record declaration introduces functions to refer collectively + to a record's fields and to convert between related record types. + They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or to convert a \isa{cpoint} to a \isa{point} by forgetting its colour. + + \begin{itemize} + + \item Function \cdx{make} takes as arguments all of the record's + fields. It returns the corresponding record. + + \item Function \cdx{fields} takes the record's new fields and + returns a record fragment consisting of just those fields. This may + be filled into the \isa{more} part of the parent record scheme. + + \item Function \cdx{extend} takes two arguments: a record to be + extended and a record containing the new fields. + + \item Function \cdx{truncate} takes a record (possibly an extension + of the original record type) and returns a fixed record, removing + any additional fields. + + \end{itemize} + + These functions merely provide handsome abbreviations for standard + record expressions involving constructors and selectors. The + definitions, which are \emph{not} unfolded by default, are made + available by the collective name of \isa{defs} (e.g.\ \isa{point{\isachardot}defs} or \isa{cpoint{\isachardot}defs}). + + For example, here are the versions of those functions generated for + record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to + be the same as \isa{point{\isachardot}make}. + + \begin{isabelle}% +point{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isasymrparr}\isanewline +point{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline +point{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isasymrparr}% +\end{isabelle} + + Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular. + + \begin{isabelle}% +cpoint{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isacharquery}col\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isacharcomma}\ col\ {\isacharequal}\ {\isacharquery}col{\isasymrparr}\isanewline +cpoint{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline +cpoint{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isasymrparr}% +\end{isabelle} + + To demonstrate these functions, we declare a new coloured point by + extending an ordinary point. Function \isa{point{\isachardot}extend} augments + \isa{pt{\isadigit{1}}} with a colour, which is converted into an appropriate + record fragment by \isa{cpoint{\isachardot}fields}.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{constdefs}\isanewline +\ \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline +\ \ {\isachardoublequote}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% +\begin{isamarkuptext}% +The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The + proof is trivial, by unfolding all the definitions. We deliberately + omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying + comparison on type \isa{point}.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}% +\end{isabelle}% +\end{isamarkuptxt}% +\ \ \isamarkuptrue% +\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{done}\isamarkupfalse% +% +\begin{isamarkuptext}% +In the example below, a coloured point is truncated to leave a + point. We must use the \isa{truncate} function of the shorter + record.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}\isamarkupfalse% +% +\begin{isamarkuptext}% +\begin{exercise} + Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with coercions among the + three record types. + \end{exercise} + + \begin{exercise} + (For Java programmers.) + Model a small class hierarchy using records. + \end{exercise} + \index{records|)}% +\end{isamarkuptext}% +\isamarkuptrue% +\isamarkupfalse% +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: