doc-src/TutorialI/Types/document/Records.tex
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 17187 45bee2f6e61f
child 26318 967323f93c67
permissions -rw-r--r--
updated;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Records}%
     4 %
     5 \isamarkupheader{Records \label{sec:records}%
     6 }
     7 \isamarkuptrue%
     8 %
     9 \isadelimtheory
    10 %
    11 \endisadelimtheory
    12 %
    13 \isatagtheory
    14 %
    15 \endisatagtheory
    16 {\isafoldtheory}%
    17 %
    18 \isadelimtheory
    19 %
    20 \endisadelimtheory
    21 %
    22 \begin{isamarkuptext}%
    23 \index{records|(}%
    24   Records are familiar from programming languages.  A record of $n$
    25   fields is essentially an $n$-tuple, but the record's components have
    26   names, which can make expressions easier to read and reduces the
    27   risk of confusing one field for another.
    28 
    29   A record of Isabelle/HOL covers a collection of fields, with select
    30   and update operations.  Each field has a specified type, which may
    31   be polymorphic.  The field names are part of the record type, and
    32   the order of the fields is significant --- as it is in Pascal but
    33   not in Standard ML.  If two different record types have field names
    34   in common, then the ambiguity is resolved in the usual way, by
    35   qualified names.
    36 
    37   Record types can also be defined by extending other record types.
    38   Extensible records make use of the reserved pseudo-field \cdx{more},
    39   which is present in every record type.  Generic record operations
    40   work on all possible extensions of a given type scheme; polymorphism
    41   takes care of structural sub-typing behind the scenes.  There are
    42   also explicit coercion functions between fixed record types.%
    43 \end{isamarkuptext}%
    44 \isamarkuptrue%
    45 %
    46 \isamarkupsubsection{Record Basics%
    47 }
    48 \isamarkuptrue%
    49 %
    50 \begin{isamarkuptext}%
    51 Record types are not primitive in Isabelle and have a delicate
    52   internal representation \cite{NaraschewskiW-TPHOLs98}, based on
    53   nested copies of the primitive product type.  A \commdx{record}
    54   declaration introduces a new record type scheme by specifying its
    55   fields, which are packaged internally to hold up the perception of
    56   the record as a distinguished entity.  Here is a simple example:%
    57 \end{isamarkuptext}%
    58 \isamarkuptrue%
    59 \isacommand{record}\isamarkupfalse%
    60 \ point\ {\isacharequal}\isanewline
    61 \ \ Xcoord\ {\isacharcolon}{\isacharcolon}\ int\isanewline
    62 \ \ Ycoord\ {\isacharcolon}{\isacharcolon}\ int%
    63 \begin{isamarkuptext}%
    64 Records of type \isa{point} have two fields named \isa{Xcoord}
    65   and \isa{Ycoord}, both of type~\isa{int}.  We now define a
    66   constant of type \isa{point}:%
    67 \end{isamarkuptext}%
    68 \isamarkuptrue%
    69 \isacommand{constdefs}\isamarkupfalse%
    70 \isanewline
    71 \ \ pt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ point\isanewline
    72 \ \ {\isachardoublequoteopen}pt{\isadigit{1}}\ {\isasymequiv}\ {\isacharparenleft}{\isacharbar}\ Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}\ {\isacharbar}{\isacharparenright}{\isachardoublequoteclose}%
    73 \begin{isamarkuptext}%
    74 We see above the ASCII notation for record brackets.  You can also
    75   use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}.  Record type
    76   expressions can be also written directly with individual fields.
    77   The type name above is merely an abbreviation.%
    78 \end{isamarkuptext}%
    79 \isamarkuptrue%
    80 \isacommand{constdefs}\isamarkupfalse%
    81 \isanewline
    82 \ \ pt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}{\isachardoublequoteclose}\isanewline
    83 \ \ {\isachardoublequoteopen}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequoteclose}%
    84 \begin{isamarkuptext}%
    85 For each field, there is a \emph{selector}\index{selector!record}
    86   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
    87   of explicit records are simplified automatically:%
    88 \end{isamarkuptext}%
    89 \isamarkuptrue%
    90 \isacommand{lemma}\isamarkupfalse%
    91 \ {\isachardoublequoteopen}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
    92 %
    93 \isadelimproof
    94 \ \ %
    95 \endisadelimproof
    96 %
    97 \isatagproof
    98 \isacommand{by}\isamarkupfalse%
    99 \ simp%
   100 \endisatagproof
   101 {\isafoldproof}%
   102 %
   103 \isadelimproof
   104 %
   105 \endisadelimproof
   106 %
   107 \begin{isamarkuptext}%
   108 The \emph{update}\index{update!record} operation is functional.  For
   109   example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
   110   value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates of explicit records are also simplified automatically:%
   111 \end{isamarkuptext}%
   112 \isamarkuptrue%
   113 \isacommand{lemma}\isamarkupfalse%
   114 \ {\isachardoublequoteopen}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
   115 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequoteclose}\isanewline
   116 %
   117 \isadelimproof
   118 \ \ %
   119 \endisadelimproof
   120 %
   121 \isatagproof
   122 \isacommand{by}\isamarkupfalse%
   123 \ simp%
   124 \endisatagproof
   125 {\isafoldproof}%
   126 %
   127 \isadelimproof
   128 %
   129 \endisadelimproof
   130 %
   131 \begin{isamarkuptext}%
   132 \begin{warn}
   133   Field names are declared as constants and can no longer be used as
   134   variables.  It would be unwise, for example, to call the fields of
   135   type \isa{point} simply \isa{x} and~\isa{y}.
   136   \end{warn}%
   137 \end{isamarkuptext}%
   138 \isamarkuptrue%
   139 %
   140 \isamarkupsubsection{Extensible Records and Generic Operations%
   141 }
   142 \isamarkuptrue%
   143 %
   144 \begin{isamarkuptext}%
   145 \index{records!extensible|(}%
   146 
   147   Now, let us define coloured points (type \isa{cpoint}) to be
   148   points extended with a field \isa{col} of type \isa{colour}:%
   149 \end{isamarkuptext}%
   150 \isamarkuptrue%
   151 \isacommand{datatype}\isamarkupfalse%
   152 \ colour\ {\isacharequal}\ Red\ {\isacharbar}\ Green\ {\isacharbar}\ Blue\isanewline
   153 \isanewline
   154 \isacommand{record}\isamarkupfalse%
   155 \ cpoint\ {\isacharequal}\ point\ {\isacharplus}\isanewline
   156 \ \ col\ {\isacharcolon}{\isacharcolon}\ colour%
   157 \begin{isamarkuptext}%
   158 The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and
   159   \isa{col}, in that order.%
   160 \end{isamarkuptext}%
   161 \isamarkuptrue%
   162 \isacommand{constdefs}\isamarkupfalse%
   163 \isanewline
   164 \ \ cpt{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
   165 \ \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}%
   166 \begin{isamarkuptext}%
   167 \medskip We can define generic operations that work on arbitrary
   168   instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions.  Every record structure has an
   169   implicit pseudo-field, \cdx{more}, that keeps the extension as an
   170   explicit value.  Its type is declared as completely
   171   polymorphic:~\isa{{\isacharprime}a}.  When a fixed record value is expressed
   172   using just its standard fields, the value of \isa{more} is
   173   implicitly set to \isa{{\isacharparenleft}{\isacharparenright}}, the empty tuple, which has type
   174   \isa{unit}.  Within the record brackets, you can refer to the
   175   \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
   176 \end{isamarkuptext}%
   177 \isamarkuptrue%
   178 \isacommand{lemma}\isamarkupfalse%
   179 \ {\isachardoublequoteopen}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
   180 %
   181 \isadelimproof
   182 \ \ %
   183 \endisadelimproof
   184 %
   185 \isatagproof
   186 \isacommand{by}\isamarkupfalse%
   187 \ simp%
   188 \endisatagproof
   189 {\isafoldproof}%
   190 %
   191 \isadelimproof
   192 %
   193 \endisadelimproof
   194 %
   195 \begin{isamarkuptext}%
   196 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
   197   \isa{more} part of a record scheme, its value is just ignored (for
   198   select) or copied (for update).
   199 
   200   The \isa{more} pseudo-field may be manipulated directly as well,
   201   but the identifier needs to be qualified:%
   202 \end{isamarkuptext}%
   203 \isamarkuptrue%
   204 \isacommand{lemma}\isamarkupfalse%
   205 \ {\isachardoublequoteopen}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequoteclose}\isanewline
   206 %
   207 \isadelimproof
   208 \ \ %
   209 \endisadelimproof
   210 %
   211 \isatagproof
   212 \isacommand{by}\isamarkupfalse%
   213 \ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
   214 \endisatagproof
   215 {\isafoldproof}%
   216 %
   217 \isadelimproof
   218 %
   219 \endisadelimproof
   220 %
   221 \begin{isamarkuptext}%
   222 We see that the colour part attached to this \isa{point} is a
   223   rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
   224   needs to be put back into the context of the parent type scheme, say
   225   as \isa{more} part of another \isa{point}.
   226 
   227   To define generic operations, we need to know a bit more about
   228   records.  Our definition of \isa{point} above has generated two
   229   type abbreviations:
   230 
   231   \medskip
   232   \begin{tabular}{l}
   233   \isa{point}~\isa{{\isacharequal}}~\isa{point} \\
   234   \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\
   235   \end{tabular}
   236   \medskip
   237 
   238   Type \isa{point} is for fixed records having exactly the two fields
   239   \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two
   240   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}.
   241 
   242   In the following example we define two operations --- methods, if we
   243   regard records as objects --- to get and set any point's \isa{Xcoord} field.%
   244 \end{isamarkuptext}%
   245 \isamarkuptrue%
   246 \isacommand{constdefs}\isamarkupfalse%
   247 \isanewline
   248 \ \ getX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
   249 \ \ {\isachardoublequoteopen}getX\ r\ {\isasymequiv}\ Xcoord\ r{\isachardoublequoteclose}\isanewline
   250 \ \ setX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\isanewline
   251 \ \ {\isachardoublequoteopen}setX\ r\ a\ {\isasymequiv}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequoteclose}%
   252 \begin{isamarkuptext}%
   253 Here is a generic method that modifies a point, incrementing its
   254   \isa{Xcoord} field.  The \isa{Ycoord} and \isa{more} fields
   255   are copied across.  It works for any record type scheme derived from
   256   \isa{point} (including \isa{cpoint} etc.):%
   257 \end{isamarkuptext}%
   258 \isamarkuptrue%
   259 \isacommand{constdefs}\isamarkupfalse%
   260 \isanewline
   261 \ \ incX\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ point{\isacharunderscore}scheme\ {\isasymRightarrow}\ {\isacharprime}a\ point{\isacharunderscore}scheme{\isachardoublequoteclose}\isanewline
   262 \ \ {\isachardoublequoteopen}incX\ r\ {\isasymequiv}\isanewline
   263 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}%
   264 \begin{isamarkuptext}%
   265 Generic theorems can be proved about generic methods.  This trivial
   266   lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
   267 \end{isamarkuptext}%
   268 \isamarkuptrue%
   269 \isacommand{lemma}\isamarkupfalse%
   270 \ {\isachardoublequoteopen}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   271 %
   272 \isadelimproof
   273 \ \ %
   274 \endisadelimproof
   275 %
   276 \isatagproof
   277 \isacommand{by}\isamarkupfalse%
   278 \ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}%
   279 \endisatagproof
   280 {\isafoldproof}%
   281 %
   282 \isadelimproof
   283 %
   284 \endisadelimproof
   285 %
   286 \begin{isamarkuptext}%
   287 \begin{warn}
   288   If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
   289   then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
   290   than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''.  Mixing the ASCII
   291   and symbolic versions causes a syntax error.  (The two versions are
   292   more distinct on screen than they are on paper.)
   293   \end{warn}%
   294   \index{records!extensible|)}%
   295 \end{isamarkuptext}%
   296 \isamarkuptrue%
   297 %
   298 \isamarkupsubsection{Record Equality%
   299 }
   300 \isamarkuptrue%
   301 %
   302 \begin{isamarkuptext}%
   303 Two records are equal\index{equality!of records} if all pairs of
   304   corresponding fields are equal.  Concrete record equalities are
   305   simplified automatically:%
   306 \end{isamarkuptext}%
   307 \isamarkuptrue%
   308 \isacommand{lemma}\isamarkupfalse%
   309 \ {\isachardoublequoteopen}{\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
   310 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   311 %
   312 \isadelimproof
   313 \ \ %
   314 \endisadelimproof
   315 %
   316 \isatagproof
   317 \isacommand{by}\isamarkupfalse%
   318 \ simp%
   319 \endisatagproof
   320 {\isafoldproof}%
   321 %
   322 \isadelimproof
   323 %
   324 \endisadelimproof
   325 %
   326 \begin{isamarkuptext}%
   327 The following equality is similar, but generic, in that \isa{r}
   328   can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
   329 \end{isamarkuptext}%
   330 \isamarkuptrue%
   331 \isacommand{lemma}\isamarkupfalse%
   332 \ {\isachardoublequoteopen}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}{\isachardoublequoteclose}\isanewline
   333 %
   334 \isadelimproof
   335 \ \ %
   336 \endisadelimproof
   337 %
   338 \isatagproof
   339 \isacommand{by}\isamarkupfalse%
   340 \ simp%
   341 \endisatagproof
   342 {\isafoldproof}%
   343 %
   344 \isadelimproof
   345 %
   346 \endisadelimproof
   347 %
   348 \begin{isamarkuptext}%
   349 We see above the syntax for iterated updates.  We could equivalently
   350   have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
   351 
   352   \medskip Record equality is \emph{extensional}:
   353   \index{extensionality!for records} a record is determined entirely
   354   by the values of its fields.%
   355 \end{isamarkuptext}%
   356 \isamarkuptrue%
   357 \isacommand{lemma}\isamarkupfalse%
   358 \ {\isachardoublequoteopen}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequoteclose}\isanewline
   359 %
   360 \isadelimproof
   361 \ \ %
   362 \endisadelimproof
   363 %
   364 \isatagproof
   365 \isacommand{by}\isamarkupfalse%
   366 \ simp%
   367 \endisatagproof
   368 {\isafoldproof}%
   369 %
   370 \isadelimproof
   371 %
   372 \endisadelimproof
   373 %
   374 \begin{isamarkuptext}%
   375 The generic version of this equality includes the pseudo-field
   376   \isa{more}:%
   377 \end{isamarkuptext}%
   378 \isamarkuptrue%
   379 \isacommand{lemma}\isamarkupfalse%
   380 \ {\isachardoublequoteopen}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequoteclose}\isanewline
   381 %
   382 \isadelimproof
   383 \ \ %
   384 \endisadelimproof
   385 %
   386 \isatagproof
   387 \isacommand{by}\isamarkupfalse%
   388 \ simp%
   389 \endisatagproof
   390 {\isafoldproof}%
   391 %
   392 \isadelimproof
   393 %
   394 \endisadelimproof
   395 %
   396 \begin{isamarkuptext}%
   397 \medskip The simplifier can prove many record equalities
   398   automatically, but general equality reasoning can be tricky.
   399   Consider proving this obvious fact:%
   400 \end{isamarkuptext}%
   401 \isamarkuptrue%
   402 \isacommand{lemma}\isamarkupfalse%
   403 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}\isanewline
   404 %
   405 \isadelimproof
   406 \ \ %
   407 \endisadelimproof
   408 %
   409 \isatagproof
   410 \isacommand{apply}\isamarkupfalse%
   411 \ simp{\isacharquery}\isanewline
   412 \ \ \isacommand{oops}\isamarkupfalse%
   413 %
   414 \endisatagproof
   415 {\isafoldproof}%
   416 %
   417 \isadelimproof
   418 %
   419 \endisadelimproof
   420 %
   421 \begin{isamarkuptext}%
   422 Here the simplifier can do nothing, since general record equality is
   423   not eliminated automatically.  One way to proceed is by an explicit
   424   forward step that applies the selector \isa{Xcoord} to both sides
   425   of the assumed record equality:%
   426 \end{isamarkuptext}%
   427 \isamarkuptrue%
   428 \isacommand{lemma}\isamarkupfalse%
   429 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}\isanewline
   430 %
   431 \isadelimproof
   432 \ \ %
   433 \endisadelimproof
   434 %
   435 \isatagproof
   436 \isacommand{apply}\isamarkupfalse%
   437 \ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}%
   438 \begin{isamarkuptxt}%
   439 \begin{isabelle}%
   440 \ {\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}%
   441 \end{isabelle}
   442     Now, \isa{simp} will reduce the assumption to the desired
   443     conclusion.%
   444 \end{isamarkuptxt}%
   445 \isamarkuptrue%
   446 \ \ \isacommand{apply}\isamarkupfalse%
   447 \ simp\isanewline
   448 \ \ \isacommand{done}\isamarkupfalse%
   449 %
   450 \endisatagproof
   451 {\isafoldproof}%
   452 %
   453 \isadelimproof
   454 %
   455 \endisadelimproof
   456 %
   457 \begin{isamarkuptext}%
   458 The \isa{cases} method is preferable to such a forward proof.  We
   459   state the desired lemma again:%
   460 \end{isamarkuptext}%
   461 \isamarkuptrue%
   462 \isacommand{lemma}\isamarkupfalse%
   463 \ {\isachardoublequoteopen}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequoteclose}%
   464 \isadelimproof
   465 %
   466 \endisadelimproof
   467 %
   468 \isatagproof
   469 %
   470 \begin{isamarkuptxt}%
   471 The \methdx{cases} method adds an equality to replace the
   472   named record term by an explicit record expression, listing all
   473   fields.  It even includes the pseudo-field \isa{more}, since the
   474   record equality stated here is generic for all extensions.%
   475 \end{isamarkuptxt}%
   476 \isamarkuptrue%
   477 \ \ \isacommand{apply}\isamarkupfalse%
   478 \ {\isacharparenleft}cases\ r{\isacharparenright}%
   479 \begin{isamarkuptxt}%
   480 \begin{isabelle}%
   481 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
   482 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
   483 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
   484 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
   485 \end{isabelle} Again, \isa{simp} finishes the proof.  Because \isa{r} is now represented as
   486   an explicit record construction, the updates can be applied and the
   487   record equality can be replaced by equality of the corresponding
   488   fields (due to injectivity).%
   489 \end{isamarkuptxt}%
   490 \isamarkuptrue%
   491 \ \ \isacommand{apply}\isamarkupfalse%
   492 \ simp\isanewline
   493 \ \ \isacommand{done}\isamarkupfalse%
   494 %
   495 \endisatagproof
   496 {\isafoldproof}%
   497 %
   498 \isadelimproof
   499 %
   500 \endisadelimproof
   501 %
   502 \begin{isamarkuptext}%
   503 The generic cases method does not admit references to locally bound
   504   parameters of a goal.  In longer proof scripts one might have to
   505   fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
   506   internal field representation rules of records.  The above use of
   507   \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
   508 \end{isamarkuptext}%
   509 \isamarkuptrue%
   510 %
   511 \isamarkupsubsection{Extending and Truncating Records%
   512 }
   513 \isamarkuptrue%
   514 %
   515 \begin{isamarkuptext}%
   516 Each record declaration introduces a number of derived operations to
   517   refer collectively to a record's fields and to convert between fixed
   518   record types.  They can, for instance, convert between types \isa{point} and \isa{cpoint}.  We can add a colour to a point or convert
   519   a \isa{cpoint} to a \isa{point} by forgetting its colour.
   520 
   521   \begin{itemize}
   522 
   523   \item Function \cdx{make} takes as arguments all of the record's
   524   fields (including those inherited from ancestors).  It returns the
   525   corresponding record.
   526 
   527   \item Function \cdx{fields} takes the record's very own fields and
   528   returns a record fragment consisting of just those fields.  This may
   529   be filled into the \isa{more} part of the parent record scheme.
   530 
   531   \item Function \cdx{extend} takes two arguments: a record to be
   532   extended and a record containing the new fields.
   533 
   534   \item Function \cdx{truncate} takes a record (possibly an extension
   535   of the original record type) and returns a fixed record, removing
   536   any additional fields.
   537 
   538   \end{itemize}
   539 
   540   These functions provide useful abbreviations for standard
   541   record expressions involving constructors and selectors.  The
   542   definitions, which are \emph{not} unfolded by default, are made
   543   available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).
   544 
   545   For example, here are the versions of those functions generated for
   546   record \isa{point}.  We omit \isa{point{\isachardot}fields}, which happens to
   547   be the same as \isa{point{\isachardot}make}.
   548 
   549   \begin{isabelle}%
   550 point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\isanewline
   551 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   552 point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
   553 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
   554 point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
   555 \end{isabelle}
   556 
   557   Contrast those with the corresponding functions for record \isa{cpoint}.  Observe \isa{cpoint{\isachardot}fields} in particular.
   558 
   559   \begin{isabelle}%
   560 cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline
   561 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   562 cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}\isasep\isanewline%
   563 cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline
   564 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isasep\isanewline%
   565 cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline
   566 {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}%
   567 \end{isabelle}
   568 
   569   To demonstrate these functions, we declare a new coloured point by
   570   extending an ordinary point.  Function \isa{point{\isachardot}extend} augments
   571   \isa{pt{\isadigit{1}}} with a colour value, which is converted into an
   572   appropriate record fragment by \isa{cpoint{\isachardot}fields}.%
   573 \end{isamarkuptext}%
   574 \isamarkuptrue%
   575 \isacommand{constdefs}\isamarkupfalse%
   576 \isanewline
   577 \ \ cpt{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ cpoint\isanewline
   578 \ \ {\isachardoublequoteopen}cpt{\isadigit{2}}\ {\isasymequiv}\ point{\isachardot}extend\ pt{\isadigit{1}}\ {\isacharparenleft}cpoint{\isachardot}fields\ Green{\isacharparenright}{\isachardoublequoteclose}%
   579 \begin{isamarkuptext}%
   580 The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal.  The
   581   proof is trivial, by unfolding all the definitions.  We deliberately
   582   omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying
   583   comparison on type \isa{point}.%
   584 \end{isamarkuptext}%
   585 \isamarkuptrue%
   586 \isacommand{lemma}\isamarkupfalse%
   587 \ {\isachardoublequoteopen}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequoteclose}\isanewline
   588 %
   589 \isadelimproof
   590 \ \ %
   591 \endisadelimproof
   592 %
   593 \isatagproof
   594 \isacommand{apply}\isamarkupfalse%
   595 \ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}%
   596 \begin{isamarkuptxt}%
   597 \begin{isabelle}%
   598 \ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
   599 \end{isabelle}%
   600 \end{isamarkuptxt}%
   601 \isamarkuptrue%
   602 \ \ \isacommand{apply}\isamarkupfalse%
   603 \ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
   604 \ \ \isacommand{done}\isamarkupfalse%
   605 %
   606 \endisatagproof
   607 {\isafoldproof}%
   608 %
   609 \isadelimproof
   610 %
   611 \endisadelimproof
   612 %
   613 \begin{isamarkuptext}%
   614 In the example below, a coloured point is truncated to leave a
   615   point.  We use the \isa{truncate} function of the target record.%
   616 \end{isamarkuptext}%
   617 \isamarkuptrue%
   618 \isacommand{lemma}\isamarkupfalse%
   619 \ {\isachardoublequoteopen}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequoteclose}\isanewline
   620 %
   621 \isadelimproof
   622 \ \ %
   623 \endisadelimproof
   624 %
   625 \isatagproof
   626 \isacommand{by}\isamarkupfalse%
   627 \ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}%
   628 \endisatagproof
   629 {\isafoldproof}%
   630 %
   631 \isadelimproof
   632 %
   633 \endisadelimproof
   634 %
   635 \begin{isamarkuptext}%
   636 \begin{exercise}
   637   Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}.  Experiment with generic operations
   638   (using polymorphic selectors and updates) and explicit coercions
   639   (using \isa{extend}, \isa{truncate} etc.) among the three record
   640   types.
   641   \end{exercise}
   642 
   643   \begin{exercise}
   644   (For Java programmers.)
   645   Model a small class hierarchy using records.
   646   \end{exercise}
   647   \index{records|)}%
   648 \end{isamarkuptext}%
   649 \isamarkuptrue%
   650 %
   651 \isadelimtheory
   652 %
   653 \endisadelimtheory
   654 %
   655 \isatagtheory
   656 %
   657 \endisatagtheory
   658 {\isafoldtheory}%
   659 %
   660 \isadelimtheory
   661 %
   662 \endisadelimtheory
   663 \end{isabellebody}%
   664 %%% Local Variables:
   665 %%% mode: latex
   666 %%% TeX-master: "root"
   667 %%% End: