1.1 --- a/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 07 18:58:35 2002 +0100
     1.2 +++ b/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 07 18:58:45 2002 +0100
     1.3 @@ -37,10 +37,11 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  Record types are not primitive in Isabelle and have a delicate
     1.7 -  internal representation based on nested copies of the primitive
     1.8 -  product type.  A \commdx{record} declaration introduces a new record
     1.9 -  type scheme by specifying its fields, which are packaged internally
    1.10 -  to hold up the perception of the record as a distinguished entity.%
    1.11 +  internal representation \cite{NaraschewskiW-TPHOLs98}, based on
    1.12 +  nested copies of the primitive product type.  A \commdx{record}
    1.13 +  declaration introduces a new record type scheme by specifying its
    1.14 +  fields, which are packaged internally to hold up the perception of
    1.15 +  the record as a distinguished entity.  Here is a simply example.%
    1.16  \end{isamarkuptext}%
    1.17  \isamarkuptrue%
    1.18  \isacommand{record}\ point\ {\isacharequal}\isanewline
    1.19 @@ -60,9 +61,8 @@
    1.20  \begin{isamarkuptext}%
    1.21  We see above the ASCII notation for record brackets.  You can also
    1.22    use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}.  Record type
    1.23 -  expressions can be written directly as well, without referring to
    1.24 -  previously declared names (which happen to be mere type
    1.25 -  abbreviations):%
    1.26 +  expressions can be also written directly with individual fields.
    1.27 +  The type name above is merely an abbreviations.%
    1.28  \end{isamarkuptext}%
    1.29  \isamarkuptrue%
    1.30  \isacommand{constdefs}\isanewline
    1.31 @@ -82,7 +82,7 @@
    1.32  \begin{isamarkuptext}%
    1.33  The \emph{update}\index{update!record} operation is functional.  For
    1.34    example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
    1.35 -  value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates are also simplified automatically:%
    1.36 +  value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates of explicit records are also simplified automatically:%
    1.37  \end{isamarkuptext}%
    1.38  \isamarkuptrue%
    1.39  \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
    1.40 @@ -118,7 +118,7 @@
    1.41  %
    1.42  \begin{isamarkuptext}%
    1.43  The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
    1.44 -  \isa{col}, in that order:%
    1.45 +  \isa{col}, in that order.%
    1.46  \end{isamarkuptext}%
    1.47  \isamarkuptrue%
    1.48  \isacommand{constdefs}\isanewline
    1.49 @@ -127,14 +127,15 @@
    1.50  %
    1.51  \begin{isamarkuptext}%
    1.52  We can define generic operations that work on arbitrary instances of
    1.53 -  a record scheme, e.g.\ covering \isa{point}, \isa{cpoint} and any
    1.54 +  a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any
    1.55    further extensions.  Every record structure has an implicit
    1.56    pseudo-field, \cdx{more}, that keeps the extension as an explicit
    1.57    value.  Its type is declared as completely polymorphic:~\isa{{\isacharprime}a}.
    1.58    When a fixed record value is expressed using just its standard
    1.59    fields, the value of \isa{more} is implicitly set to \isa{{\isacharparenleft}{\isacharparenright}},
    1.60    the empty tuple, which has type \isa{unit}.  Within the record
    1.61 -  brackets, you can refer to the \isa{more} field by writing \isa{{\isasymdots}} (three dots):%
    1.62 +  brackets, you can refer to the \isa{more} field by writing
    1.63 +  ``\isa{{\isasymdots}}'' (three dots):%
    1.64  \end{isamarkuptext}%
    1.65  \isamarkuptrue%
    1.66  \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
    1.67 @@ -142,7 +143,8 @@
    1.68  \isacommand{by}\ simp\isamarkupfalse%
    1.69  %
    1.70  \begin{isamarkuptext}%
    1.71 -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
    1.72 +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
    1.73 +  \isa{more} part of a record scheme, its value is just ignored (for
    1.74    select) or copied (for update).
    1.75  
    1.76    The \isa{more} pseudo-field may be manipulated directly as well,
    1.77 @@ -154,14 +156,14 @@
    1.78  \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
    1.79  %
    1.80  \begin{isamarkuptext}%
    1.81 -We see that the colour attached to this \isa{point} is a
    1.82 +We see that the colour part attached to this \isa{point} is a
    1.83    (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
    1.84    needs to be put back into the context of the parent type scheme, say
    1.85    as \isa{more} part of another \isa{point}.
    1.86  
    1.87    To define generic operations, we need to know a bit more about
    1.88 -  records.  Our definition of \isa{point} above generated two type
    1.89 -  abbreviations:
    1.90 +  records.  Our definition of \isa{point} above has generated two
    1.91 +  type abbreviations:
    1.92  
    1.93    \medskip
    1.94    \begin{tabular}{l}
    1.95 @@ -193,8 +195,8 @@
    1.96  \isamarkuptrue%
    1.97  \isacommand{constdefs}\isanewline
    1.98  \ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequote}\isanewline
    1.99 -\ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\isanewline
   1.100 -\ \ \ \ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
   1.101 +\ \ {\isachardoublequote}incX\ r\ {\isasymequiv}\isanewline
   1.102 +\ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
   1.103  %
   1.104  \begin{isamarkuptext}%
   1.105  Generic theorems can be proved about generic methods.  This trivial
   1.106 @@ -223,8 +225,8 @@
   1.107  %
   1.108  \begin{isamarkuptext}%
   1.109  Two records are equal\index{equality!of records} if all pairs of
   1.110 -  corresponding fields are equal.  Record equalities are simplified
   1.111 -  automatically:%
   1.112 +  corresponding fields are equal.  Concrete record equalities are
   1.113 +  simplified automatically:%
   1.114  \end{isamarkuptext}%
   1.115  \isamarkuptrue%
   1.116  \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
   1.117 @@ -334,8 +336,8 @@
   1.118  The generic cases method does not admit references to locally bound
   1.119    parameters of a goal.  In longer proof scripts one might have to
   1.120    fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
   1.121 -  internal representation rules of records.  E.g.\ the above use of
   1.122 -  \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
   1.123 +  internal field representation rules of records.  E.g.\ the above use
   1.124 +  of \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
   1.125  \end{isamarkuptext}%
   1.126  \isamarkuptrue%
   1.127  %