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