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 %