35 Record types are not primitive in Isabelle and have a delicate |
35 Record types are not primitive in Isabelle and have a delicate |
36 internal representation \cite{NaraschewskiW-TPHOLs98}, based on |
36 internal representation \cite{NaraschewskiW-TPHOLs98}, based on |
37 nested copies of the primitive product type. A \commdx{record} |
37 nested copies of the primitive product type. A \commdx{record} |
38 declaration introduces a new record type scheme by specifying its |
38 declaration introduces a new record type scheme by specifying its |
39 fields, which are packaged internally to hold up the perception of |
39 fields, which are packaged internally to hold up the perception of |
40 the record as a distinguished entity. Here is a simply example. |
40 the record as a distinguished entity. Here is a very simply example: |
41 *} |
41 *} |
42 |
42 |
43 record point = |
43 record point = |
44 Xcoord :: int |
44 Xcoord :: int |
45 Ycoord :: int |
45 Ycoord :: int |
118 constdefs |
118 constdefs |
119 cpt1 :: cpoint |
119 cpt1 :: cpoint |
120 "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>" |
120 "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>" |
121 |
121 |
122 text {* |
122 text {* |
123 We can define generic operations that work on arbitrary instances of |
123 \medskip We can define generic operations that work on arbitrary |
124 a record scheme, e.g.\ covering @{typ point}, @{typ cpoint}, and any |
124 instances of a record scheme, e.g.\ covering @{typ point}, @{typ |
125 further extensions. Every record structure has an implicit |
125 cpoint}, and any further extensions. Every record structure has an |
126 pseudo-field, \cdx{more}, that keeps the extension as an explicit |
126 implicit pseudo-field, \cdx{more}, that keeps the extension as an |
127 value. Its type is declared as completely polymorphic:~@{typ 'a}. |
127 explicit value. Its type is declared as completely |
128 When a fixed record value is expressed using just its standard |
128 polymorphic:~@{typ 'a}. When a fixed record value is expressed |
129 fields, the value of @{text more} is implicitly set to @{text "()"}, |
129 using just its standard fields, the value of @{text more} is |
130 the empty tuple, which has type @{typ unit}. Within the record |
130 implicitly set to @{text "()"}, the empty tuple, which has type |
131 brackets, you can refer to the @{text more} field by writing |
131 @{typ unit}. Within the record brackets, you can refer to the |
132 ``@{text "\<dots>"}'' (three dots): |
132 @{text more} field by writing ``@{text "\<dots>"}'' (three dots): |
133 *} |
133 *} |
134 |
134 |
135 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a" |
135 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a" |
136 by simp |
136 by simp |
137 |
137 |
309 |
309 |
310 text {* |
310 text {* |
311 The generic cases method does not admit references to locally bound |
311 The generic cases method does not admit references to locally bound |
312 parameters of a goal. In longer proof scripts one might have to |
312 parameters of a goal. In longer proof scripts one might have to |
313 fall back on the primitive @{text rule_tac} used together with the |
313 fall back on the primitive @{text rule_tac} used together with the |
314 internal field representation rules of records. E.g.\ the above use |
314 internal field representation rules of records. The above use of |
315 of @{text "(cases r)"} would become @{text "(rule_tac r = r in |
315 @{text "(cases r)"} would become @{text "(rule_tac r = r in |
316 point.cases_scheme)"}. |
316 point.cases_scheme)"}. |
317 *} |
317 *} |
318 |
318 |
319 |
319 |
320 subsection {* Extending and Truncating Records *} |
320 subsection {* Extending and Truncating Records *} |