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