doc-src/TutorialI/Types/document/Records.tex

 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Record types are not primitive in Isabelle and have a delicate
-  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 the record as a distinguished entity.%
+  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 simply example.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{record}\ point\ {\isacharequal}\isanewline
 \ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline
 \ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int\isamarkupfalse%

 \ \ {\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):%
+  expressions can be also written directly with individual fields.
+  The type name above is merely an 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%

 \isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The \emph{update}\index{update!record} 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:%
+  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}\ {\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{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:%
+  \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
+  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):%
+  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 really the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}.  Selectors and updates are always polymorphic wrt.\ the \isa{more} part of a record scheme, its value is just ignored (for
+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
+  \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}%

 \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
+We see that the colour part 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}, 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 generated two type
-  abbreviations:
+  records.  Our definition of \isa{point} above has generated two
+  type abbreviations:
 
   \medskip
   \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}} \\

   \isa{point} (including \isa{cpoint} etc.):%
 \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%
+\ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\isanewline
+\ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ 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%
 %
 \begin{isamarkuptext}%
 Two records are equal\index{equality!of records} if all pairs of
-  corresponding fields are equal.  Record equalities are simplified
-  automatically:%
+  corresponding fields are equal.  Concrete 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%

 %
 \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{\isacharunderscore}tac} used together with the
-  internal representation rules of records.  E.g.\ the above use of
-  \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
+  internal field representation rules of records.  E.g.\ the above use
+  of \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Extending and Truncating Records%
 }