diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/Records.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/document/Records.tex Thu Jul 26 19:59:06 2012 +0200 @@ -0,0 +1,665 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Records}% +% +\isamarkupheader{Records \label{sec:records}% +} +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\begin{isamarkuptext}% +\index{records|(}% + Records are familiar from programming languages. A record of $n$ + fields is essentially an $n$-tuple, but the record's components have + names, which can make expressions easier to read and reduces the + risk of confusing one field for another. + + A record of Isabelle/HOL covers a collection of fields, with select + and update operations. Each field has a specified type, which may + be polymorphic. The field names are part of the record type, and + the order of the fields is significant --- as it is in Pascal but + not in Standard ML. If two different record types have field names + in common, then the ambiguity is resolved in the usual way, by + qualified names. + + Record types can also be defined by extending other record types. + Extensible records make use of the reserved pseudo-field \cdx{more}, + which is present in every record type. Generic record operations + work on all possible extensions of a given type scheme; polymorphism + takes care of structural sub-typing behind the scenes. There are + also explicit coercion functions between fixed record types.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record Basics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Record types are not primitive in Isabelle and have a delicate + internal representation \cite{NaraschewskiW-TPHOLs98}, based on + nested copies of the primitive product type. A \commdx{record} + declaration introduces a new record type scheme by specifying its + fields, which are packaged internally to hold up the perception of + the record as a distinguished entity. Here is a simple example:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{record}\isamarkupfalse% +\ point\ {\isaliteral{3D}{\isacharequal}}\isanewline +\ \ Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline +\ \ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int% +\begin{isamarkuptext}% +\noindent + Records of type \isa{point} have two fields named \isa{Xcoord} + and \isa{Ycoord}, both of type~\isa{int}. We now define a + constant of type \isa{point}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ pt{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ point\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}pt{\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +\noindent + We see above the ASCII notation for record brackets. You can also + use the symbolic brackets \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}} and \isa{{\isaliteral{5C3C72706172723E}{\isasymrparr}}}. Record type + expressions can be also written directly with individual fields. + The type name above is merely an abbreviation.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ pt{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}pt{\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{4}}{\isadigit{5}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{7}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +For each field, there is a \emph{selector}\index{selector!record} + 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 + of explicit records are simplified automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}Xcoord\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The \emph{update}\index{update!record} operation is functional. For + example, \isa{p{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}} is a record whose \isa{Xcoord} + value is zero and whose \isa{Ycoord} value is copied from~\isa{p}. Updates of explicit records are also simplified automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\isanewline +\ \ \ \ \ \ \ \ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\begin{warn} + Field names are declared as constants and can no longer be used as + variables. It would be unwise, for example, to call the fields of + type \isa{point} simply \isa{x} and~\isa{y}. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Extensible Records and Generic Operations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\index{records!extensible|(}% + + Now, let us define coloured points (type \isa{cpoint}) to be + points extended with a field \isa{col} of type \isa{colour}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{datatype}\isamarkupfalse% +\ colour\ {\isaliteral{3D}{\isacharequal}}\ Red\ {\isaliteral{7C}{\isacharbar}}\ Green\ {\isaliteral{7C}{\isacharbar}}\ Blue\isanewline +\isanewline +\isacommand{record}\isamarkupfalse% +\ cpoint\ {\isaliteral{3D}{\isacharequal}}\ point\ {\isaliteral{2B}{\isacharplus}}\isanewline +\ \ col\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ colour% +\begin{isamarkuptext}% +\noindent + The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and + \isa{col}, in that order.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ cpt{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ cpoint\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{1}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +We can define generic operations that work on arbitrary + instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions. Every record structure has an + implicit pseudo-field, \cdx{more}, that keeps the extension as an + explicit value. Its type is declared as completely + polymorphic:~\isa{{\isaliteral{27}{\isacharprime}}a}. When a fixed record value is expressed + using just its standard fields, the value of \isa{more} is + implicitly set to \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}}, the empty tuple, which has type + \isa{unit}. Within the record brackets, you can refer to the + \isa{more} field by writing ``\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}'' (three dots):% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}Xcoord\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Note that \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}} is exactly the same as \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}}. Selectors and updates are always polymorphic wrt.\ the + \isa{more} part of a record scheme, its value is just ignored (for + select) or copied (for update). + + The \isa{more} pseudo-field may be manipulated directly as well, + but the identifier needs to be qualified:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}point{\isaliteral{2E}{\isachardot}}more\ cpt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ cpt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent + We see that the colour part attached to this \isa{point} is a + rudimentary record in its own right, namely \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ Green{\isaliteral{5C3C72706172723E}{\isasymrparr}}}. In order to select or update \isa{col}, this fragment + needs to be put back into the context of the parent type scheme, say + as \isa{more} part of another \isa{point}. + + To define generic operations, we need to know a bit more about + records. Our definition of \isa{point} above has generated two + type abbreviations: + + \medskip + \begin{tabular}{l} + \isa{point}~\isa{{\isaliteral{3D}{\isacharequal}}}~\isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{5C3C72706172723E}{\isasymrparr}}} \\ + \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme}~\isa{{\isaliteral{3D}{\isacharequal}}}~\isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C72706172723E}{\isasymrparr}}} \\ + \end{tabular} + \medskip + +\noindent + Type \isa{point} is for fixed records having exactly the two fields + \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme} comprises all possible extensions to those two + fields. Note that \isa{unit\ point{\isaliteral{5F}{\isacharunderscore}}scheme} coincides with \isa{point}, and \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ colour{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ point{\isaliteral{5F}{\isacharunderscore}}scheme} with \isa{cpoint}. + + In the following example we define two operations --- methods, if we + regard records as objects --- to get and set any point's \isa{Xcoord} field.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ getX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}getX\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ Xcoord\ r{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isacommand{definition}\isamarkupfalse% +\ setX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}setX\ r\ a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +Here is a generic method that modifies a point, incrementing its + \isa{Xcoord} field. The \isa{Ycoord} and \isa{more} fields + are copied across. It works for any record type scheme derived from + \isa{point} (including \isa{cpoint} etc.):% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ incX\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}incX\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline +\ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ point{\isaliteral{2E}{\isachardot}}more\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +Generic theorems can be proved about generic methods. This trivial + lemma relates \isa{incX} to \isa{getX} and \isa{setX}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}incX\ r\ {\isaliteral{3D}{\isacharequal}}\ setX\ r\ {\isaliteral{28}{\isacharparenleft}}getX\ r\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ getX{\isaliteral{5F}{\isacharunderscore}}def\ setX{\isaliteral{5F}{\isacharunderscore}}def\ incX{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\begin{warn} + If you use the symbolic record brackets \isa{{\isaliteral{5C3C6C706172723E}{\isasymlparr}}} and \isa{{\isaliteral{5C3C72706172723E}{\isasymrparr}}}, + then you must also use the symbolic ellipsis, ``\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}'', rather + than three consecutive periods, ``\isa{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}''. Mixing the ASCII + and symbolic versions causes a syntax error. (The two versions are + more distinct on screen than they are on paper.) + \end{warn}% + \index{records!extensible|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record Equality% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Two records are equal\index{equality!of records} if all pairs of + corresponding fields are equal. Concrete record equalities are + simplified automatically:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The following equality is similar, but generic, in that \isa{r} + can be any instance of \isa{{\isaliteral{27}{\isacharprime}}a\ point{\isaliteral{5F}{\isacharunderscore}}scheme}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent + We see above the syntax for iterated updates. We could equivalently + have written the left-hand side as \isa{r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Ycoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}}. + + Record equality is \emph{extensional}: + \index{extensionality!for records} a record is determined entirely + by the values of its fields.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent + The generic version of this equality includes the pseudo-field + \isa{more}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ point{\isaliteral{2E}{\isachardot}}more\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ simp% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The simplifier can prove many record equalities + automatically, but general equality reasoning can be tricky. + Consider proving this obvious fact:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ simp{\isaliteral{3F}{\isacharquery}}\isanewline +\ \ \isacommand{oops}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent + Here the simplifier can do nothing, since general record equality is + not eliminated automatically. One way to proceed is by an explicit + forward step that applies the selector \isa{Xcoord} to both sides + of the assumed record equality:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}drule{\isaliteral{5F}{\isacharunderscore}}tac\ f\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ \isakeyword{in}\ arg{\isaliteral{5F}{\isacharunderscore}}cong{\isaliteral{29}{\isacharparenright}}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Xcoord\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}% +\end{isabelle} + Now, \isa{simp} will reduce the assumption to the desired + conclusion.% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \isacommand{apply}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The \isa{cases} method is preferable to such a forward proof. We + state the desired lemma again:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +% +\endisadelimproof +% +\isatagproof +% +\begin{isamarkuptxt}% +The \methdx{cases} method adds an equality to replace the + named record term by an explicit record expression, listing all + fields. It even includes the pseudo-field \isa{more}, since the + record equality stated here is generic for all extensions.% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}Xcoord\ Ycoord\ more{\isaliteral{2E}{\isachardot}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }r\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{27}{\isacharprime}}% +\end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{r} is now represented as + an explicit record construction, the updates can be applied and the + record equality can be replaced by equality of the corresponding + fields (due to injectivity).% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \isacommand{apply}\isamarkupfalse% +\ simp\isanewline +\ \ \isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +The generic cases method does not admit references to locally bound + parameters of a goal. In longer proof scripts one might have to + fall back on the primitive \isa{rule{\isaliteral{5F}{\isacharunderscore}}tac} used together with the + internal field representation rules of records. The above use of + \isa{{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}} would become \isa{{\isaliteral{28}{\isacharparenleft}}rule{\isaliteral{5F}{\isacharunderscore}}tac\ r\ {\isaliteral{3D}{\isacharequal}}\ r\ in\ point{\isaliteral{2E}{\isachardot}}cases{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{29}{\isacharparenright}}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Extending and Truncating Records% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Each record declaration introduces a number of derived operations to + refer collectively to a record's fields and to convert between fixed + record types. They can, for instance, convert between types \isa{point} and \isa{cpoint}. We can add a colour to a point or convert + a \isa{cpoint} to a \isa{point} by forgetting its colour. + + \begin{itemize} + + \item Function \cdx{make} takes as arguments all of the record's + fields (including those inherited from ancestors). It returns the + corresponding record. + + \item Function \cdx{fields} takes the record's very own fields and + returns a record fragment consisting of just those fields. This may + be filled into the \isa{more} part of the parent record scheme. + + \item Function \cdx{extend} takes two arguments: a record to be + extended and a record containing the new fields. + + \item Function \cdx{truncate} takes a record (possibly an extension + of the original record type) and returns a fixed record, removing + any additional fields. + + \end{itemize} + These functions provide useful abbreviations for standard + record expressions involving constructors and selectors. The + definitions, which are \emph{not} unfolded by default, are made + available by the collective name of \isa{defs} (\isa{point{\isaliteral{2E}{\isachardot}}defs}, \isa{cpoint{\isaliteral{2E}{\isachardot}}defs}, etc.). + For example, here are the versions of those functions generated for + record \isa{point}. We omit \isa{point{\isaliteral{2E}{\isachardot}}fields}, which happens to + be the same as \isa{point{\isaliteral{2E}{\isachardot}}make}. + + \begin{isabelle}% +point{\isaliteral{2E}{\isachardot}}make\ Xcoord\ Ycoord\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline% +point{\isaliteral{2E}{\isachardot}}extend\ r\ more\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline +{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline% +point{\isaliteral{2E}{\isachardot}}truncate\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}% +\end{isabelle} + Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isaliteral{2E}{\isachardot}}fields} in particular. + \begin{isabelle}% +cpoint{\isaliteral{2E}{\isachardot}}make\ Xcoord\ Ycoord\ col\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline +{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline% +cpoint{\isaliteral{2E}{\isachardot}}fields\ col\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}col\ {\isaliteral{3D}{\isacharequal}}\ col{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline% +cpoint{\isaliteral{2E}{\isachardot}}extend\ r\ more\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline +{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col\ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ more{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isasep\isanewline% +cpoint{\isaliteral{2E}{\isachardot}}truncate\ r\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\isanewline +{\isaliteral{5C3C6C706172723E}{\isasymlparr}}Xcoord\ {\isaliteral{3D}{\isacharequal}}\ Xcoord\ r{\isaliteral{2C}{\isacharcomma}}\ Ycoord\ {\isaliteral{3D}{\isacharequal}}\ Ycoord\ r{\isaliteral{2C}{\isacharcomma}}\ col\ {\isaliteral{3D}{\isacharequal}}\ col\ r{\isaliteral{5C3C72706172723E}{\isasymrparr}}% +\end{isabelle} + + To demonstrate these functions, we declare a new coloured point by + extending an ordinary point. Function \isa{point{\isaliteral{2E}{\isachardot}}extend} augments + \isa{pt{\isadigit{1}}} with a colour value, which is converted into an + appropriate record fragment by \isa{cpoint{\isaliteral{2E}{\isachardot}}fields}.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{definition}\isamarkupfalse% +\ cpt{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ cpoint\ \isakeyword{where}\isanewline +{\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{2}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ point{\isaliteral{2E}{\isachardot}}extend\ pt{\isadigit{1}}\ {\isaliteral{28}{\isacharparenleft}}cpoint{\isaliteral{2E}{\isachardot}}fields\ Green{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\begin{isamarkuptext}% +The coloured points \isa{cpt{\isadigit{1}}} and \isa{cpt{\isadigit{2}}} are equal. The + proof is trivial, by unfolding all the definitions. We deliberately + omit the definition of~\isa{pt{\isadigit{1}}} in order to reveal the underlying + comparison on type \isa{point}.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}cpt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ cpt{\isadigit{2}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ cpt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def\ cpt{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}def\ point{\isaliteral{2E}{\isachardot}}defs\ cpoint{\isaliteral{2E}{\isachardot}}defs{\isaliteral{29}{\isacharparenright}}% +\begin{isamarkuptxt}% +\begin{isabelle}% +\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Xcoord\ pt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Ycoord\ pt{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isadigit{3}}% +\end{isabelle}% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \isacommand{apply}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ pt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \isacommand{done}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +In the example below, a coloured point is truncated to leave a + point. We use the \isa{truncate} function of the target record.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}point{\isaliteral{2E}{\isachardot}}truncate\ cpt{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ pt{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ pt{\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}def\ cpt{\isadigit{2}}{\isaliteral{5F}{\isacharunderscore}}def\ point{\isaliteral{2E}{\isachardot}}defs{\isaliteral{29}{\isacharparenright}}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\begin{exercise} + Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with generic operations + (using polymorphic selectors and updates) and explicit coercions + (using \isa{extend}, \isa{truncate} etc.) among the three record + types. + \end{exercise} + + \begin{exercise} + (For Java programmers.) + Model a small class hierarchy using records. + \end{exercise} + \index{records|)}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: