doc-src/TutorialI/Types/document/Records.tex
changeset 15481 fc075ae929e4
parent 14379 ea10a8c3e9cf
child 15873 02d9f110ecc1
equal deleted inserted replaced
15480:cb3612cc41a3 15481:fc075ae929e4
    75   of explicit records are simplified automatically:%
    75   of explicit records are simplified automatically:%
    76 \end{isamarkuptext}%
    76 \end{isamarkuptext}%
    77 \isamarkuptrue%
    77 \isamarkuptrue%
    78 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
    78 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
    79 \ \ \isamarkupfalse%
    79 \ \ \isamarkupfalse%
    80 \isacommand{by}\ simp\isamarkupfalse%
    80 \isamarkupfalse%
    81 %
    81 %
    82 \begin{isamarkuptext}%
    82 \begin{isamarkuptext}%
    83 The \emph{update}\index{update!record} operation is functional.  For
    83 The \emph{update}\index{update!record} operation is functional.  For
    84   example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
    84   example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}} is a record whose \isa{Xcoord}
    85   value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates of explicit records are also simplified automatically:%
    85   value is zero and whose \isa{Ycoord} value is copied from~\isa{p}.  Updates of explicit records are also simplified automatically:%
    86 \end{isamarkuptext}%
    86 \end{isamarkuptext}%
    87 \isamarkuptrue%
    87 \isamarkuptrue%
    88 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
    88 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
    89 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline
    89 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline
    90 \ \ \isamarkupfalse%
    90 \ \ \isamarkupfalse%
    91 \isacommand{by}\ simp\isamarkupfalse%
    91 \isamarkupfalse%
    92 %
    92 %
    93 \begin{isamarkuptext}%
    93 \begin{isamarkuptext}%
    94 \begin{warn}
    94 \begin{warn}
    95   Field names are declared as constants and can no longer be used as
    95   Field names are declared as constants and can no longer be used as
    96   variables.  It would be unwise, for example, to call the fields of
    96   variables.  It would be unwise, for example, to call the fields of
   137   \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
   137   \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
   138 \end{isamarkuptext}%
   138 \end{isamarkuptext}%
   139 \isamarkuptrue%
   139 \isamarkuptrue%
   140 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
   140 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
   141 \ \ \isamarkupfalse%
   141 \ \ \isamarkupfalse%
   142 \isacommand{by}\ simp\isamarkupfalse%
   142 \isamarkupfalse%
   143 %
   143 %
   144 \begin{isamarkuptext}%
   144 \begin{isamarkuptext}%
   145 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
   145 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
   146   \isa{more} part of a record scheme, its value is just ignored (for
   146   \isa{more} part of a record scheme, its value is just ignored (for
   147   select) or copied (for update).
   147   select) or copied (for update).
   150   but the identifier needs to be qualified:%
   150   but the identifier needs to be qualified:%
   151 \end{isamarkuptext}%
   151 \end{isamarkuptext}%
   152 \isamarkuptrue%
   152 \isamarkuptrue%
   153 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline
   153 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline
   154 \ \ \isamarkupfalse%
   154 \ \ \isamarkupfalse%
   155 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
   155 \isamarkupfalse%
   156 %
   156 %
   157 \begin{isamarkuptext}%
   157 \begin{isamarkuptext}%
   158 We see that the colour part attached to this \isa{point} is a
   158 We see that the colour part attached to this \isa{point} is a
   159   rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
   159   rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
   160   needs to be put back into the context of the parent type scheme, say
   160   needs to be put back into the context of the parent type scheme, say
   202   lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
   202   lemma relates \isa{incX} to \isa{getX} and \isa{setX}:%
   203 \end{isamarkuptext}%
   203 \end{isamarkuptext}%
   204 \isamarkuptrue%
   204 \isamarkuptrue%
   205 \isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
   205 \isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
   206 \ \ \isamarkupfalse%
   206 \ \ \isamarkupfalse%
   207 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
   207 \isamarkupfalse%
   208 %
   208 %
   209 \begin{isamarkuptext}%
   209 \begin{isamarkuptext}%
   210 \begin{warn}
   210 \begin{warn}
   211   If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
   211   If you use the symbolic record brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}},
   212   then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
   212   then you must also use the symbolic ellipsis, ``\isa{{\isasymdots}}'', rather
   229 \end{isamarkuptext}%
   229 \end{isamarkuptext}%
   230 \isamarkuptrue%
   230 \isamarkuptrue%
   231 \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
   231 \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
   232 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline
   232 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline
   233 \ \ \isamarkupfalse%
   233 \ \ \isamarkupfalse%
   234 \isacommand{by}\ simp\isamarkupfalse%
   234 \isamarkupfalse%
   235 %
   235 %
   236 \begin{isamarkuptext}%
   236 \begin{isamarkuptext}%
   237 The following equality is similar, but generic, in that \isa{r}
   237 The following equality is similar, but generic, in that \isa{r}
   238   can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
   238   can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:%
   239 \end{isamarkuptext}%
   239 \end{isamarkuptext}%
   240 \isamarkuptrue%
   240 \isamarkuptrue%
   241 \isacommand{lemma}\ {\isachardoublequote}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}{\isachardoublequote}\isanewline
   241 \isacommand{lemma}\ {\isachardoublequote}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}{\isachardoublequote}\isanewline
   242 \ \ \isamarkupfalse%
   242 \ \ \isamarkupfalse%
   243 \isacommand{by}\ simp\isamarkupfalse%
   243 \isamarkupfalse%
   244 %
   244 %
   245 \begin{isamarkuptext}%
   245 \begin{isamarkuptext}%
   246 We see above the syntax for iterated updates.  We could equivalently
   246 We see above the syntax for iterated updates.  We could equivalently
   247   have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
   247   have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}.
   248 
   248 
   251   by the values of its fields.%
   251   by the values of its fields.%
   252 \end{isamarkuptext}%
   252 \end{isamarkuptext}%
   253 \isamarkuptrue%
   253 \isamarkuptrue%
   254 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
   254 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
   255 \ \ \isamarkupfalse%
   255 \ \ \isamarkupfalse%
   256 \isacommand{by}\ simp\isamarkupfalse%
   256 \isamarkupfalse%
   257 %
   257 %
   258 \begin{isamarkuptext}%
   258 \begin{isamarkuptext}%
   259 The generic version of this equality includes the pseudo-field
   259 The generic version of this equality includes the pseudo-field
   260   \isa{more}:%
   260   \isa{more}:%
   261 \end{isamarkuptext}%
   261 \end{isamarkuptext}%
   262 \isamarkuptrue%
   262 \isamarkuptrue%
   263 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline
   263 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline
   264 \ \ \isamarkupfalse%
   264 \ \ \isamarkupfalse%
   265 \isacommand{by}\ simp\isamarkupfalse%
   265 \isamarkupfalse%
   266 %
   266 %
   267 \begin{isamarkuptext}%
   267 \begin{isamarkuptext}%
   268 \medskip The simplifier can prove many record equalities
   268 \medskip The simplifier can prove many record equalities
   269   automatically, but general equality reasoning can be tricky.
   269   automatically, but general equality reasoning can be tricky.
   270   Consider proving this obvious fact:%
   270   Consider proving this obvious fact:%
   271 \end{isamarkuptext}%
   271 \end{isamarkuptext}%
   272 \isamarkuptrue%
   272 \isamarkuptrue%
   273 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
   273 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
   274 \ \ \isamarkupfalse%
   274 \ \ \isamarkupfalse%
   275 \isacommand{apply}\ simp{\isacharquery}\isanewline
   275 \isamarkupfalse%
   276 \ \ \isamarkupfalse%
   276 \isamarkupfalse%
   277 \isacommand{oops}\isamarkupfalse%
       
   278 %
   277 %
   279 \begin{isamarkuptext}%
   278 \begin{isamarkuptext}%
   280 Here the simplifier can do nothing, since general record equality is
   279 Here the simplifier can do nothing, since general record equality is
   281   not eliminated automatically.  One way to proceed is by an explicit
   280   not eliminated automatically.  One way to proceed is by an explicit
   282   forward step that applies the selector \isa{Xcoord} to both sides
   281   forward step that applies the selector \isa{Xcoord} to both sides
   283   of the assumed record equality:%
   282   of the assumed record equality:%
   284 \end{isamarkuptext}%
   283 \end{isamarkuptext}%
   285 \isamarkuptrue%
   284 \isamarkuptrue%
   286 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
   285 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
   287 \ \ \isamarkupfalse%
   286 \ \ \isamarkupfalse%
   288 \isacommand{apply}\ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
   287 \isamarkupfalse%
   289 %
   288 \isamarkuptrue%
   290 \begin{isamarkuptxt}%
   289 \isamarkupfalse%
   291 \begin{isabelle}%
   290 \isamarkupfalse%
   292 \ {\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}%
       
   293 \end{isabelle}
       
   294     Now, \isa{simp} will reduce the assumption to the desired
       
   295     conclusion.%
       
   296 \end{isamarkuptxt}%
       
   297 \ \ \isamarkuptrue%
       
   298 \isacommand{apply}\ simp\isanewline
       
   299 \ \ \isamarkupfalse%
       
   300 \isacommand{done}\isamarkupfalse%
       
   301 %
   291 %
   302 \begin{isamarkuptext}%
   292 \begin{isamarkuptext}%
   303 The \isa{cases} method is preferable to such a forward proof.  We
   293 The \isa{cases} method is preferable to such a forward proof.  We
   304   state the desired lemma again:%
   294   state the desired lemma again:%
   305 \end{isamarkuptext}%
   295 \end{isamarkuptext}%
   306 \isamarkuptrue%
   296 \isamarkuptrue%
   307 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse%
   297 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse%
   308 %
   298 \isamarkuptrue%
   309 \begin{isamarkuptxt}%
   299 \isamarkupfalse%
   310 The \methdx{cases} method adds an equality to replace the
   300 \isamarkuptrue%
   311   named record term by an explicit record expression, listing all
   301 \isamarkupfalse%
   312   fields.  It even includes the pseudo-field \isa{more}, since the
   302 \isamarkupfalse%
   313   record equality stated here is generic for all extensions.%
       
   314 \end{isamarkuptxt}%
       
   315 \ \ \isamarkuptrue%
       
   316 \isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse%
       
   317 %
       
   318 \begin{isamarkuptxt}%
       
   319 \begin{isabelle}%
       
   320 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
       
   321 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
       
   322 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
       
   323 \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
       
   324 \end{isabelle} Again, \isa{simp} finishes the proof.  Because \isa{r} is now represented as
       
   325   an explicit record construction, the updates can be applied and the
       
   326   record equality can be replaced by equality of the corresponding
       
   327   fields (due to injectivity).%
       
   328 \end{isamarkuptxt}%
       
   329 \ \ \isamarkuptrue%
       
   330 \isacommand{apply}\ simp\isanewline
       
   331 \ \ \isamarkupfalse%
       
   332 \isacommand{done}\isamarkupfalse%
       
   333 %
   303 %
   334 \begin{isamarkuptext}%
   304 \begin{isamarkuptext}%
   335 The generic cases method does not admit references to locally bound
   305 The generic cases method does not admit references to locally bound
   336   parameters of a goal.  In longer proof scripts one might have to
   306   parameters of a goal.  In longer proof scripts one might have to
   337   fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
   307   fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
   414   comparison on type \isa{point}.%
   384   comparison on type \isa{point}.%
   415 \end{isamarkuptext}%
   385 \end{isamarkuptext}%
   416 \isamarkuptrue%
   386 \isamarkuptrue%
   417 \isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline
   387 \isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline
   418 \ \ \isamarkupfalse%
   388 \ \ \isamarkupfalse%
   419 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}\isamarkupfalse%
   389 \isamarkupfalse%
   420 %
   390 \isamarkuptrue%
   421 \begin{isamarkuptxt}%
   391 \isamarkupfalse%
   422 \begin{isabelle}%
   392 \isamarkupfalse%
   423 \ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
       
   424 \end{isabelle}%
       
   425 \end{isamarkuptxt}%
       
   426 \ \ \isamarkuptrue%
       
   427 \isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
       
   428 \ \ \isamarkupfalse%
       
   429 \isacommand{done}\isamarkupfalse%
       
   430 %
   393 %
   431 \begin{isamarkuptext}%
   394 \begin{isamarkuptext}%
   432 In the example below, a coloured point is truncated to leave a
   395 In the example below, a coloured point is truncated to leave a
   433   point.  We use the \isa{truncate} function of the target record.%
   396   point.  We use the \isa{truncate} function of the target record.%
   434 \end{isamarkuptext}%
   397 \end{isamarkuptext}%
   435 \isamarkuptrue%
   398 \isamarkuptrue%
   436 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
   399 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
   437 \ \ \isamarkupfalse%
   400 \ \ \isamarkupfalse%
   438 \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}\isamarkupfalse%
   401 \isamarkupfalse%
   439 %
   402 %
   440 \begin{isamarkuptext}%
   403 \begin{isamarkuptext}%
   441 \begin{exercise}
   404 \begin{exercise}
   442   Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}.  Experiment with generic operations
   405   Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}.  Experiment with generic operations
   443   (using polymorphic selectors and updates) and explicit coercions
   406   (using polymorphic selectors and updates) and explicit coercions