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