
diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/Records.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Records.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,665 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Records}%
+%
+\isamarkupheader{Records \label{sec:records}%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\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 record of Isabelle/HOL covers a collection 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; 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 delicate
+  internal representation \cite{NaraschewskiW-TPHOLs98}, 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
+  the record as a distinguished entity.  Here is a simple example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{record}\isamarkupfalse%
+\ point\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
+\ \ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int%
+\begin{isamarkuptext}%
+\noindent
+  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{definition}\isamarkupfalse%
+\ pt{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ point\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}pt{\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+  We see above the ASCII notation for record brackets.  You can also
+  use the symbolic brackets \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}} and \isa{{\isaliteral{5C3C72706172723E}{\isasymrparr}}}.  Record type
+  expressions can be also written directly with individual fields.
+  The type name above is merely an abbreviation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ pt{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}pt{\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isadigit{5}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{7}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+For each field, there is a \emph{selector}\index{selector!record}
+  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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Xcoord\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The \emph{update}\index{update!record} operation is functional.  For
+  example, \isa{p{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}} is a record whose \isa{Xcoord}
+  value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates of explicit records are also simplified automatically:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ \ \ \ \ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\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}.
+  \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}\isamarkupfalse%
+\ colour\ {\isaliteral{3D}{\isacharequal}}\ Red\ {\isaliteral{7C}{\isacharbar}}\ Green\ {\isaliteral{7C}{\isacharbar}}\ Blue\isanewline
+\isanewline
+\isacommand{record}\isamarkupfalse%
+\ cpoint\ {\isaliteral{3D}{\isacharequal}}\ point\ {\isaliteral{2B}{\isacharplus}}\isanewline
+\ \ col\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ colour%
+\begin{isamarkuptext}%
+\noindent
+  The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
+  \isa{col}, in that order.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ cpt{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ cpoint\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\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{{\isaliteral{27}{\isacharprime}}a}.  When a fixed record value is expressed
+  using just its standard fields, the value of \isa{more} is
+  implicitly set to \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}}, the empty tuple, which has type
+  \isa{unit}.  Within the record brackets, you can refer to the
+  \isa{more} field by writing ``\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}'' (three dots):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Xcoord\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}.  Note that \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}} is exactly the same as \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}}.  Selectors and updates are always polymorphic wrt.\ the
+  \isa{more} part of a record scheme, its value is just ignored (for
+  select) or copied (for update).
+
+  The \isa{more} pseudo-field may be manipulated directly as well,
+  but the identifier needs to be qualified:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}point{\isaliteral{2E}{\isachardot}}more\ cpt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ cpt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+  We see that the colour part attached to this \isa{point} is a
+  rudimentary record in its own right, namely \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}}.  In order to select or update \isa{col}, this fragment
+  needs to be put back into the context of the parent type scheme, say
+  as \isa{more} part of another \isa{point}.
+
+  To define generic operations, we need to know a bit more about
+  records.  Our definition of \isa{point} above has generated two
+  type abbreviations:
+
+  \medskip
+  \begin{tabular}{l}
+  \isa{point}~\isa{{\isaliteral{3D}{\isacharequal}}}~\isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{5C3C72706172723E}{\isasymrparr}}} \\
+  \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme}~\isa{{\isaliteral{3D}{\isacharequal}}}~\isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C72706172723E}{\isasymrparr}}} \\
+  \end{tabular}
+  \medskip
+  
+\noindent
+  Type \isa{point} is for fixed records having exactly the two fields
+  \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme} comprises all possible extensions to those two
+  fields.  Note that \isa{unit\ point{\isaliteral{5F}{\isacharunderscore}}scheme} coincides with \isa{point}, and \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ colour{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ point{\isaliteral{5F}{\isacharunderscore}}scheme} with \isa{cpoint}.
+
+  In the following example we define two operations --- methods, if we
+  regard records as objects --- to get and set any point's \isa{Xcoord} field.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ getX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}getX\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ Xcoord\ r{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ setX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}setX\ r\ a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\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} (including \isa{cpoint} etc.):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ incX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}incX\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline
+\ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ point{\isaliteral{2E}{\isachardot}}more\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}incX\ r\ {\isaliteral{3D}{\isacharequal}}\ setX\ r\ {\isaliteral{28}{\isacharparenleft}}getX\ r\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ getX{\isaliteral{5F}{\isacharunderscore}}def\ setX{\isaliteral{5F}{\isacharunderscore}}def\ incX{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{warn}
+  If you use the symbolic record brackets \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}} and \isa{{\isaliteral{5C3C72706172723E}{\isasymrparr}}},
+  then you must also use the symbolic ellipsis, ``\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}'', rather
+  than three consecutive periods, ``\isa{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\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.  Concrete record equalities are
+  simplified automatically:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The following equality is similar, but generic, in that \isa{r}
+  can be any instance of \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+  We see above the syntax for iterated updates.  We could equivalently
+  have written the left-hand side as \isa{r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+  The generic version of this equality includes the pseudo-field
+  \isa{more}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ point{\isaliteral{2E}{\isachardot}}more\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ simp{\isaliteral{3F}{\isacharquery}}\isanewline
+\ \ \isacommand{oops}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent
+  Here 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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}drule{\isaliteral{5F}{\isacharunderscore}}tac\ f\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ \isakeyword{in}\ arg{\isaliteral{5F}{\isacharunderscore}}cong{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Xcoord\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}%
+\end{isabelle}
+    Now, \isa{simp} will reduce the assumption to the desired
+    conclusion.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{apply}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The \isa{cases} method is preferable to such a forward proof.  We
+  state the desired lemma again:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+The \methdx{cases} method adds an equality to replace the
+  named record term by an explicit record expression, listing all
+  fields.  It even includes the pseudo-field \isa{more}, since the
+  record equality stated here is generic for all extensions.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}Xcoord\ Ycoord\ more{\isaliteral{2E}{\isachardot}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}%
+\end{isabelle} Again, \isa{simp} finishes the proof.  Because \isa{r} is now represented as
+  an explicit record construction, 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}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+The generic cases method does not admit references to locally bound
+  parameters of a goal.  In longer proof scripts one might have to
+  fall back on the primitive \isa{rule{\isaliteral{5F}{\isacharunderscore}}tac} used together with the
+  internal field representation rules of records.  The above use of
+  \isa{{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}} would become \isa{{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ r\ {\isaliteral{3D}{\isacharequal}}\ r\ in\ point{\isaliteral{2E}{\isachardot}}cases{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{29}{\isacharparenright}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Extending and Truncating Records%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Each record declaration introduces a number of derived operations to
+  refer collectively to a record's fields and to convert between fixed
+  record types.  They can, for instance, convert between types \isa{point} and \isa{cpoint}.  We can add a colour to a point or 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 (including those inherited from ancestors).  It returns the
+  corresponding record.
+
+  \item Function \cdx{fields} takes the record's very own 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 provide useful 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} (\isa{point{\isaliteral{2E}{\isachardot}}defs}, \isa{cpoint{\isaliteral{2E}{\isachardot}}defs}, etc.).
+  For example, here are the versions of those functions generated for
+  record \isa{point}.  We omit \isa{point{\isaliteral{2E}{\isachardot}}fields}, which happens to
+  be the same as \isa{point{\isaliteral{2E}{\isachardot}}make}.
+
+  \begin{isabelle}%
+point{\isaliteral{2E}{\isachardot}}make\ Xcoord\ Ycoord\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline%
+point{\isaliteral{2E}{\isachardot}}extend\ r\ more\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline
+{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline%
+point{\isaliteral{2E}{\isachardot}}truncate\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}%
+\end{isabelle}
+  Contrast those with the corresponding functions for record \isa{cpoint}.  Observe \isa{cpoint{\isaliteral{2E}{\isachardot}}fields} in particular.
+  \begin{isabelle}%
+cpoint{\isaliteral{2E}{\isachardot}}make\ Xcoord\ Ycoord\ col\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline
+{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline%
+cpoint{\isaliteral{2E}{\isachardot}}fields\ col\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ col{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline%
+cpoint{\isaliteral{2E}{\isachardot}}extend\ r\ more\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline
+{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline%
+cpoint{\isaliteral{2E}{\isachardot}}truncate\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline
+{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}%
+\end{isabelle}
+
+  To demonstrate these functions, we declare a new coloured point by
+  extending an ordinary point.  Function \isa{point{\isaliteral{2E}{\isachardot}}extend} augments
+  \isa{pt{\isadigit{1}}} with a colour value, which is converted into an
+  appropriate record fragment by \isa{cpoint{\isaliteral{2E}{\isachardot}}fields}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ cpt{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ cpoint\ \isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ point{\isaliteral{2E}{\isachardot}}extend\ pt{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}cpoint{\isaliteral{2E}{\isachardot}}fields\ Green{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\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}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ cpt{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ cpt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def\ cpt{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}def\ point{\isaliteral{2E}{\isachardot}}defs\ cpoint{\isaliteral{2E}{\isachardot}}defs{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Xcoord\ pt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Ycoord\ pt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{apply}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ pt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+In the example below, a coloured point is truncated to leave a
+  point.  We use the \isa{truncate} function of the target record.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}point{\isaliteral{2E}{\isachardot}}truncate\ cpt{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ pt{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ pt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def\ cpt{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}def\ point{\isaliteral{2E}{\isachardot}}defs{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\begin{exercise}
+  Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}.  Experiment with generic operations
+  (using polymorphic selectors and updates) and explicit coercions
+  (using \isa{extend}, \isa{truncate} etc.) 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%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:




