doc-src/TutorialI/Types/Records.thy
author nipkow
Thu, 29 May 2008 22:45:33 +0200
changeset 27015 f8537d69f514
parent 16417 9bc16273c2d4
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     1
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     2
header {* Records \label{sec:records} *}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     3
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     4
(*<*)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15905
diff changeset
     5
theory Records imports Main begin
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     6
(*>*)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     7
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     8
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
     9
  \index{records|(}%
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    10
  Records are familiar from programming languages.  A record of $n$
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    11
  fields is essentially an $n$-tuple, but the record's components have
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    12
  names, which can make expressions easier to read and reduces the
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    13
  risk of confusing one field for another.
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    14
12586
wenzelm
parents: 12567
diff changeset
    15
  A record of Isabelle/HOL covers a collection of fields, with select
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    16
  and update operations.  Each field has a specified type, which may
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    17
  be polymorphic.  The field names are part of the record type, and
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    18
  the order of the fields is significant --- as it is in Pascal but
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    19
  not in Standard ML.  If two different record types have field names
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    20
  in common, then the ambiguity is resolved in the usual way, by
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    21
  qualified names.
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    22
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    23
  Record types can also be defined by extending other record types.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    24
  Extensible records make use of the reserved pseudo-field \cdx{more},
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    25
  which is present in every record type.  Generic record operations
12586
wenzelm
parents: 12567
diff changeset
    26
  work on all possible extensions of a given type scheme; polymorphism
wenzelm
parents: 12567
diff changeset
    27
  takes care of structural sub-typing behind the scenes.  There are
wenzelm
parents: 12567
diff changeset
    28
  also explicit coercion functions between fixed record types.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    29
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    30
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    31
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    32
subsection {* Record Basics *}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    33
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    34
text {*
12586
wenzelm
parents: 12567
diff changeset
    35
  Record types are not primitive in Isabelle and have a delicate
12655
wenzelm
parents: 12634
diff changeset
    36
  internal representation \cite{NaraschewskiW-TPHOLs98}, based on
wenzelm
parents: 12634
diff changeset
    37
  nested copies of the primitive product type.  A \commdx{record}
wenzelm
parents: 12634
diff changeset
    38
  declaration introduces a new record type scheme by specifying its
wenzelm
parents: 12634
diff changeset
    39
  fields, which are packaged internally to hold up the perception of
12700
f0d09c9693d6 stylistic changes
paulson
parents: 12657
diff changeset
    40
  the record as a distinguished entity.  Here is a simple example:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    41
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    42
8db249f786ee for the records section
paulson
parents:
diff changeset
    43
record point =
8db249f786ee for the records section
paulson
parents:
diff changeset
    44
  Xcoord :: int
8db249f786ee for the records section
paulson
parents:
diff changeset
    45
  Ycoord :: int
8db249f786ee for the records section
paulson
parents:
diff changeset
    46
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    47
text {*\noindent
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
    48
  Records of type @{typ point} have two fields named @{const Xcoord}
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
    49
  and @{const Ycoord}, both of type~@{typ int}.  We now define a
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    50
  constant of type @{typ point}:
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    51
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    52
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    53
definition pt1 :: point where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    54
"pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    55
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    56
text {*\noindent
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    57
  We see above the ASCII notation for record brackets.  You can also
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    58
  use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}.  Record type
12655
wenzelm
parents: 12634
diff changeset
    59
  expressions can be also written directly with individual fields.
12700
f0d09c9693d6 stylistic changes
paulson
parents: 12657
diff changeset
    60
  The type name above is merely an abbreviation.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    61
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    62
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    63
definition pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    64
"pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    65
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    66
text {*
12586
wenzelm
parents: 12567
diff changeset
    67
  For each field, there is a \emph{selector}\index{selector!record}
wenzelm
parents: 12567
diff changeset
    68
  function of the same name.  For example, if @{text p} has type @{typ
wenzelm
parents: 12567
diff changeset
    69
  point} then @{text "Xcoord p"} denotes the value of the @{text
wenzelm
parents: 12567
diff changeset
    70
  Xcoord} field of~@{text p}.  Expressions involving field selection
wenzelm
parents: 12567
diff changeset
    71
  of explicit records are simplified automatically:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    72
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    73
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    74
lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    75
  by simp
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    76
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    77
text {*
12586
wenzelm
parents: 12567
diff changeset
    78
  The \emph{update}\index{update!record} operation is functional.  For
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
    79
  example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{const Xcoord}
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
    80
  value is zero and whose @{const Ycoord} value is copied from~@{text
12655
wenzelm
parents: 12634
diff changeset
    81
  p}.  Updates of explicit records are also simplified automatically:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    82
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    83
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    84
lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    85
         \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    86
  by simp
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    87
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    88
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    89
  \begin{warn}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    90
  Field names are declared as constants and can no longer be used as
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    91
  variables.  It would be unwise, for example, to call the fields of
12586
wenzelm
parents: 12567
diff changeset
    92
  type @{typ point} simply @{text x} and~@{text y}.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    93
  \end{warn}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    94
*}
8db249f786ee for the records section
paulson
parents:
diff changeset
    95
11428
332347b9b942 tidying the index
paulson
parents: 11389
diff changeset
    96
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
    97
subsection {* Extensible Records and Generic Operations *}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
    98
8db249f786ee for the records section
paulson
parents:
diff changeset
    99
text {*
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   100
  \index{records!extensible|(}%
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   101
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   102
  Now, let us define coloured points (type @{text cpoint}) to be
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   103
  points extended with a field @{text col} of type @{text colour}:
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   104
*}
8db249f786ee for the records section
paulson
parents:
diff changeset
   105
8db249f786ee for the records section
paulson
parents:
diff changeset
   106
datatype colour = Red | Green | Blue
8db249f786ee for the records section
paulson
parents:
diff changeset
   107
8db249f786ee for the records section
paulson
parents:
diff changeset
   108
record cpoint = point +
8db249f786ee for the records section
paulson
parents:
diff changeset
   109
  col :: colour
8db249f786ee for the records section
paulson
parents:
diff changeset
   110
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   111
text {*\noindent
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   112
  The fields of this new type are @{const Xcoord}, @{text Ycoord} and
12655
wenzelm
parents: 12634
diff changeset
   113
  @{text col}, in that order.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   114
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   115
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   116
definition cpt1 :: cpoint where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   117
"cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   118
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   119
text {*
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   120
  We can define generic operations that work on arbitrary
12657
wenzelm
parents: 12655
diff changeset
   121
  instances of a record scheme, e.g.\ covering @{typ point}, @{typ
wenzelm
parents: 12655
diff changeset
   122
  cpoint}, and any further extensions.  Every record structure has an
wenzelm
parents: 12655
diff changeset
   123
  implicit pseudo-field, \cdx{more}, that keeps the extension as an
wenzelm
parents: 12655
diff changeset
   124
  explicit value.  Its type is declared as completely
wenzelm
parents: 12655
diff changeset
   125
  polymorphic:~@{typ 'a}.  When a fixed record value is expressed
wenzelm
parents: 12655
diff changeset
   126
  using just its standard fields, the value of @{text more} is
wenzelm
parents: 12655
diff changeset
   127
  implicitly set to @{text "()"}, the empty tuple, which has type
wenzelm
parents: 12655
diff changeset
   128
  @{typ unit}.  Within the record brackets, you can refer to the
wenzelm
parents: 12655
diff changeset
   129
  @{text more} field by writing ``@{text "\<dots>"}'' (three dots):
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   130
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   131
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   132
lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   133
  by simp
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   134
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   135
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   136
  This lemma applies to any record whose first two fields are @{text
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   137
  Xcoord} and~@{const Ycoord}.  Note that @{text "\<lparr>Xcoord = a, Ycoord
12655
wenzelm
parents: 12634
diff changeset
   138
  = b, \<dots> = ()\<rparr>"} is exactly the same as @{text "\<lparr>Xcoord = a, Ycoord
wenzelm
parents: 12634
diff changeset
   139
  = b\<rparr>"}.  Selectors and updates are always polymorphic wrt.\ the
wenzelm
parents: 12634
diff changeset
   140
  @{text more} part of a record scheme, its value is just ignored (for
12586
wenzelm
parents: 12567
diff changeset
   141
  select) or copied (for update).
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   142
12586
wenzelm
parents: 12567
diff changeset
   143
  The @{text more} pseudo-field may be manipulated directly as well,
wenzelm
parents: 12567
diff changeset
   144
  but the identifier needs to be qualified:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   145
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   146
8db249f786ee for the records section
paulson
parents:
diff changeset
   147
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   148
  by (simp add: cpt1_def)
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   149
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   150
text {*\noindent
12655
wenzelm
parents: 12634
diff changeset
   151
  We see that the colour part attached to this @{typ point} is a
12700
f0d09c9693d6 stylistic changes
paulson
parents: 12657
diff changeset
   152
  rudimentary record in its own right, namely @{text "\<lparr>col =
12586
wenzelm
parents: 12567
diff changeset
   153
  Green\<rparr>"}.  In order to select or update @{text col}, this fragment
wenzelm
parents: 12567
diff changeset
   154
  needs to be put back into the context of the parent type scheme, say
wenzelm
parents: 12567
diff changeset
   155
  as @{text more} part of another @{typ point}.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   156
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   157
  To define generic operations, we need to know a bit more about
12655
wenzelm
parents: 12634
diff changeset
   158
  records.  Our definition of @{typ point} above has generated two
wenzelm
parents: 12634
diff changeset
   159
  type abbreviations:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   160
12586
wenzelm
parents: 12567
diff changeset
   161
  \medskip
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   162
  \begin{tabular}{l}
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   163
  @{typ point}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   164
  @{typ "'a point_scheme"}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   165
  \end{tabular}
12586
wenzelm
parents: 12567
diff changeset
   166
  \medskip
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   167
  
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   168
\noindent
12586
wenzelm
parents: 12567
diff changeset
   169
  Type @{typ point} is for fixed records having exactly the two fields
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   170
  @{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   171
  "'a point_scheme"} comprises all possible extensions to those two
12586
wenzelm
parents: 12567
diff changeset
   172
  fields.  Note that @{typ "unit point_scheme"} coincides with @{typ
wenzelm
parents: 12567
diff changeset
   173
  point}, and @{typ "\<lparr>col :: colour\<rparr> point_scheme"} with @{typ
wenzelm
parents: 12567
diff changeset
   174
  cpoint}.
wenzelm
parents: 12567
diff changeset
   175
wenzelm
parents: 12567
diff changeset
   176
  In the following example we define two operations --- methods, if we
wenzelm
parents: 12567
diff changeset
   177
  regard records as objects --- to get and set any point's @{text
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   178
  Xcoord} field.
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   179
*}
8db249f786ee for the records section
paulson
parents:
diff changeset
   180
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   181
definition getX :: "'a point_scheme \<Rightarrow> int" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   182
"getX r \<equiv> Xcoord r"
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   183
definition setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   184
"setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   185
8db249f786ee for the records section
paulson
parents:
diff changeset
   186
text {*
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   187
  Here is a generic method that modifies a point, incrementing its
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   188
  @{const Xcoord} field.  The @{text Ycoord} and @{text more} fields
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   189
  are copied across.  It works for any record type scheme derived from
12586
wenzelm
parents: 12567
diff changeset
   190
  @{typ point} (including @{typ cpoint} etc.):
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   191
*}
8db249f786ee for the records section
paulson
parents:
diff changeset
   192
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   193
definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   194
"incX r \<equiv>
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   195
  \<lparr>Xcoord = Xcoord r + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   196
8db249f786ee for the records section
paulson
parents:
diff changeset
   197
text {*
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   198
  Generic theorems can be proved about generic methods.  This trivial
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   199
  lemma relates @{const incX} to @{text getX} and @{text setX}:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   200
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   201
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   202
lemma "incX r = setX r (getX r + 1)"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   203
  by (simp add: getX_def setX_def incX_def)
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   204
8db249f786ee for the records section
paulson
parents:
diff changeset
   205
text {*
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   206
  \begin{warn}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   207
  If you use the symbolic record brackets @{text \<lparr>} and @{text \<rparr>},
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   208
  then you must also use the symbolic ellipsis, ``@{text \<dots>}'', rather
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   209
  than three consecutive periods, ``@{text "..."}''.  Mixing the ASCII
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   210
  and symbolic versions causes a syntax error.  (The two versions are
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   211
  more distinct on screen than they are on paper.)
12634
3baa6143a9c4 fixed \index;
wenzelm
parents: 12586
diff changeset
   212
  \end{warn}%
3baa6143a9c4 fixed \index;
wenzelm
parents: 12586
diff changeset
   213
  \index{records!extensible|)}
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   214
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   215
8db249f786ee for the records section
paulson
parents:
diff changeset
   216
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   217
subsection {* Record Equality *}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   218
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   219
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   220
  Two records are equal\index{equality!of records} if all pairs of
12655
wenzelm
parents: 12634
diff changeset
   221
  corresponding fields are equal.  Concrete record equalities are
wenzelm
parents: 12634
diff changeset
   222
  simplified automatically:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   223
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   224
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   225
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) =
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   226
    (a = a' \<and> b = b')"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   227
  by simp
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   228
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   229
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   230
  The following equality is similar, but generic, in that @{text r}
12586
wenzelm
parents: 12567
diff changeset
   231
  can be any instance of @{typ "'a point_scheme"}:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   232
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   233
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   234
lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   235
  by simp
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   236
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   237
text {*\noindent
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   238
  We see above the syntax for iterated updates.  We could equivalently
12586
wenzelm
parents: 12567
diff changeset
   239
  have written the left-hand side as @{text "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord :=
wenzelm
parents: 12567
diff changeset
   240
  b\<rparr>"}.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   241
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   242
  Record equality is \emph{extensional}:
12586
wenzelm
parents: 12567
diff changeset
   243
  \index{extensionality!for records} a record is determined entirely
wenzelm
parents: 12567
diff changeset
   244
  by the values of its fields.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   245
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   246
8db249f786ee for the records section
paulson
parents:
diff changeset
   247
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   248
  by simp
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   249
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   250
text {*\noindent
12586
wenzelm
parents: 12567
diff changeset
   251
  The generic version of this equality includes the pseudo-field
wenzelm
parents: 12567
diff changeset
   252
  @{text more}:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   253
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   254
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   255
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   256
  by simp
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   257
8db249f786ee for the records section
paulson
parents:
diff changeset
   258
text {*
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   259
  The simplifier can prove many record equalities
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   260
  automatically, but general equality reasoning can be tricky.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   261
  Consider proving this obvious fact:
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   262
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   263
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   264
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   265
  apply simp?
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   266
  oops
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   267
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   268
text {*\noindent
12586
wenzelm
parents: 12567
diff changeset
   269
  Here the simplifier can do nothing, since general record equality is
wenzelm
parents: 12567
diff changeset
   270
  not eliminated automatically.  One way to proceed is by an explicit
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   271
  forward step that applies the selector @{const Xcoord} to both sides
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   272
  of the assumed record equality:
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   273
*}
8db249f786ee for the records section
paulson
parents:
diff changeset
   274
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   275
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   276
  apply (drule_tac f = Xcoord in arg_cong)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   277
  txt {* @{subgoals [display, indent = 0, margin = 65]}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   278
    Now, @{text simp} will reduce the assumption to the desired
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   279
    conclusion. *}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   280
  apply simp
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   281
  done
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   282
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   283
text {*
12586
wenzelm
parents: 12567
diff changeset
   284
  The @{text cases} method is preferable to such a forward proof.  We
wenzelm
parents: 12567
diff changeset
   285
  state the desired lemma again:
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   286
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   287
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   288
lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
12586
wenzelm
parents: 12567
diff changeset
   289
wenzelm
parents: 12567
diff changeset
   290
  txt {* The \methdx{cases} method adds an equality to replace the
wenzelm
parents: 12567
diff changeset
   291
  named record term by an explicit record expression, listing all
wenzelm
parents: 12567
diff changeset
   292
  fields.  It even includes the pseudo-field @{text more}, since the
wenzelm
parents: 12567
diff changeset
   293
  record equality stated here is generic for all extensions. *}
wenzelm
parents: 12567
diff changeset
   294
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   295
  apply (cases r)
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   296
12586
wenzelm
parents: 12567
diff changeset
   297
  txt {* @{subgoals [display, indent = 0, margin = 65]} Again, @{text
wenzelm
parents: 12567
diff changeset
   298
  simp} finishes the proof.  Because @{text r} is now represented as
wenzelm
parents: 12567
diff changeset
   299
  an explicit record construction, the updates can be applied and the
wenzelm
parents: 12567
diff changeset
   300
  record equality can be replaced by equality of the corresponding
wenzelm
parents: 12567
diff changeset
   301
  fields (due to injectivity). *}
wenzelm
parents: 12567
diff changeset
   302
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   303
  apply simp
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   304
  done
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   305
12586
wenzelm
parents: 12567
diff changeset
   306
text {*
wenzelm
parents: 12567
diff changeset
   307
  The generic cases method does not admit references to locally bound
wenzelm
parents: 12567
diff changeset
   308
  parameters of a goal.  In longer proof scripts one might have to
wenzelm
parents: 12567
diff changeset
   309
  fall back on the primitive @{text rule_tac} used together with the
12657
wenzelm
parents: 12655
diff changeset
   310
  internal field representation rules of records.  The above use of
wenzelm
parents: 12655
diff changeset
   311
  @{text "(cases r)"} would become @{text "(rule_tac r = r in
12586
wenzelm
parents: 12567
diff changeset
   312
  point.cases_scheme)"}.
wenzelm
parents: 12567
diff changeset
   313
*}
wenzelm
parents: 12567
diff changeset
   314
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   315
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   316
subsection {* Extending and Truncating Records *}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   317
8db249f786ee for the records section
paulson
parents:
diff changeset
   318
text {*
12586
wenzelm
parents: 12567
diff changeset
   319
  Each record declaration introduces a number of derived operations to
wenzelm
parents: 12567
diff changeset
   320
  refer collectively to a record's fields and to convert between fixed
wenzelm
parents: 12567
diff changeset
   321
  record types.  They can, for instance, convert between types @{typ
wenzelm
parents: 12567
diff changeset
   322
  point} and @{typ cpoint}.  We can add a colour to a point or convert
wenzelm
parents: 12567
diff changeset
   323
  a @{typ cpoint} to a @{typ point} by forgetting its colour.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   324
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   325
  \begin{itemize}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   326
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   327
  \item Function \cdx{make} takes as arguments all of the record's
12586
wenzelm
parents: 12567
diff changeset
   328
  fields (including those inherited from ancestors).  It returns the
wenzelm
parents: 12567
diff changeset
   329
  corresponding record.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   330
12586
wenzelm
parents: 12567
diff changeset
   331
  \item Function \cdx{fields} takes the record's very own fields and
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   332
  returns a record fragment consisting of just those fields.  This may
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   333
  be filled into the @{text more} part of the parent record scheme.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   334
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   335
  \item Function \cdx{extend} takes two arguments: a record to be
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   336
  extended and a record containing the new fields.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   337
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   338
  \item Function \cdx{truncate} takes a record (possibly an extension
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   339
  of the original record type) and returns a fixed record, removing
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   340
  any additional fields.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   341
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   342
  \end{itemize}
12700
f0d09c9693d6 stylistic changes
paulson
parents: 12657
diff changeset
   343
  These functions provide useful abbreviations for standard
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   344
  record expressions involving constructors and selectors.  The
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   345
  definitions, which are \emph{not} unfolded by default, are made
12586
wenzelm
parents: 12567
diff changeset
   346
  available by the collective name of @{text defs} (@{text
wenzelm
parents: 12567
diff changeset
   347
  point.defs}, @{text cpoint.defs}, etc.).
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   348
  For example, here are the versions of those functions generated for
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   349
  record @{typ point}.  We omit @{text point.fields}, which happens to
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   350
  be the same as @{text point.make}.
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   351
12586
wenzelm
parents: 12567
diff changeset
   352
  @{thm [display, indent = 0, margin = 65] point.make_def [no_vars]
wenzelm
parents: 12567
diff changeset
   353
  point.extend_def [no_vars] point.truncate_def [no_vars]}
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   354
  Contrast those with the corresponding functions for record @{typ
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   355
  cpoint}.  Observe @{text cpoint.fields} in particular.
12586
wenzelm
parents: 12567
diff changeset
   356
  @{thm [display, indent = 0, margin = 65] cpoint.make_def [no_vars]
wenzelm
parents: 12567
diff changeset
   357
  cpoint.fields_def [no_vars] cpoint.extend_def [no_vars]
wenzelm
parents: 12567
diff changeset
   358
  cpoint.truncate_def [no_vars]}
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   359
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   360
  To demonstrate these functions, we declare a new coloured point by
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   361
  extending an ordinary point.  Function @{text point.extend} augments
12586
wenzelm
parents: 12567
diff changeset
   362
  @{text pt1} with a colour value, which is converted into an
wenzelm
parents: 12567
diff changeset
   363
  appropriate record fragment by @{text cpoint.fields}.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   364
*}
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   365
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   366
definition cpt2 :: cpoint where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
   367
"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
12407
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   368
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   369
text {*
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12700
diff changeset
   370
  The coloured points @{const cpt1} and @{text cpt2} are equal.  The
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   371
  proof is trivial, by unfolding all the definitions.  We deliberately
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   372
  omit the definition of~@{text pt1} in order to reveal the underlying
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   373
  comparison on type @{typ point}.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   374
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   375
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   376
lemma "cpt1 = cpt2"
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   377
  apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   378
  txt {* @{subgoals [display, indent = 0, margin = 65]} *}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   379
  apply (simp add: pt1_def)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   380
  done
12407
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   381
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   382
text {*
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   383
  In the example below, a coloured point is truncated to leave a
12586
wenzelm
parents: 12567
diff changeset
   384
  point.  We use the @{text truncate} function of the target record.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   385
*}
12407
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   386
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   387
lemma "point.truncate cpt2 = pt1"
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   388
  by (simp add: pt1_def cpt2_def point.defs)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   389
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   390
text {*
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   391
  \begin{exercise}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   392
  Extend record @{typ cpoint} to have a further field, @{text
12586
wenzelm
parents: 12567
diff changeset
   393
  intensity}, of type~@{typ nat}.  Experiment with generic operations
wenzelm
parents: 12567
diff changeset
   394
  (using polymorphic selectors and updates) and explicit coercions
wenzelm
parents: 12567
diff changeset
   395
  (using @{text extend}, @{text truncate} etc.) among the three record
wenzelm
parents: 12567
diff changeset
   396
  types.
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   397
  \end{exercise}
12407
70ebb59264f1 record extend and truncate
paulson
parents: 12156
diff changeset
   398
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   399
  \begin{exercise}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   400
  (For Java programmers.)
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   401
  Model a small class hierarchy using records.
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   402
  \end{exercise}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   403
  \index{records|)}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   404
*}
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   405
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   406
(*<*)
11387
8db249f786ee for the records section
paulson
parents:
diff changeset
   407
end
12567
614ef5ca41ed turned into proper Isabelle document;
wenzelm
parents: 12409
diff changeset
   408
(*>*)