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




