doc-src/TutorialI/Types/Records.thy

 
 subsection {* Record Basics *}
 
 text {*
   Record types are not primitive in Isabelle and have a delicate
-  internal representation based on nested copies of the primitive
-  product type.  A \commdx{record} declaration introduces a new record
-  type scheme by specifying its fields, which are packaged internally
-  to hold up the perception of the record as a distinguished entity.
+  internal representation \cite{NaraschewskiW-TPHOLs98}, based on
+  nested copies of the primitive product type.  A \commdx{record}
+  declaration introduces a new record type scheme by specifying its
+  fields, which are packaged internally to hold up the perception of
+  the record as a distinguished entity.  Here is a simply example.
 *}
 
 record point =
   Xcoord :: int
   Ycoord :: int

   "pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
 
 text {*
   We see above the ASCII notation for record brackets.  You can also
   use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}.  Record type
-  expressions can be written directly as well, without referring to
-  previously declared names (which happen to be mere type
-  abbreviations):
+  expressions can be also written directly with individual fields.
+  The type name above is merely an abbreviations.
 *}
 
 constdefs
   pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"
   "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"

 
 text {*
   The \emph{update}\index{update!record} operation is functional.  For
   example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{text Xcoord}
   value is zero and whose @{text Ycoord} value is copied from~@{text
-  p}.  Updates are also simplified automatically:
+  p}.  Updates of explicit records are also simplified automatically:
 *}
 
 lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
     \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
   by simp

 record cpoint = point +
   col :: colour
 
 text {*
   The fields of this new type are @{text Xcoord}, @{text Ycoord} and
-  @{text col}, in that order:
+  @{text col}, in that order.
 *}
 
 constdefs
   cpt1 :: cpoint
   "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
 
 text {*
   We can define generic operations that work on arbitrary instances of
-  a record scheme, e.g.\ covering @{typ point}, @{typ cpoint} and any
+  a record scheme, e.g.\ covering @{typ point}, @{typ cpoint}, and any
   further extensions.  Every record structure has an implicit
   pseudo-field, \cdx{more}, that keeps the extension as an explicit
   value.  Its type is declared as completely polymorphic:~@{typ 'a}.
   When a fixed record value is expressed using just its standard
   fields, the value of @{text more} is implicitly set to @{text "()"},
   the empty tuple, which has type @{typ unit}.  Within the record
-  brackets, you can refer to the @{text more} field by writing @{text
-  "\<dots>"} (three dots):
+  brackets, you can refer to the @{text more} field by writing
+  ``@{text "\<dots>"}'' (three dots):
 *}
 
 lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a"
   by simp
 
 text {*
   This lemma applies to any record whose first two fields are @{text
-  Xcoord} and~@{text Ycoord}.  Note that @{text "\<lparr>Xcoord = a, Ycoord =
-  b, \<dots> = ()\<rparr>"} is really the same as @{text "\<lparr>Xcoord = a, Ycoord =
-  b\<rparr>"}.  Selectors and updates are always polymorphic wrt.\ the @{text
-  more} part of a record scheme, its value is just ignored (for
+  Xcoord} and~@{text Ycoord}.  Note that @{text "\<lparr>Xcoord = a, Ycoord
+  = b, \<dots> = ()\<rparr>"} is exactly the same as @{text "\<lparr>Xcoord = a, Ycoord
+  = b\<rparr>"}.  Selectors and updates are always polymorphic wrt.\ the
+  @{text more} part of a record scheme, its value is just ignored (for
   select) or copied (for update).
 
   The @{text more} pseudo-field may be manipulated directly as well,
   but the identifier needs to be qualified:
 *}
 
 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
   by (simp add: cpt1_def)
 
 text {*
-  We see that the colour attached to this @{typ point} is a
+  We see that the colour part attached to this @{typ point} is a
   (rudimentary) record in its own right, namely @{text "\<lparr>col =
   Green\<rparr>"}.  In order to select or update @{text col}, this fragment
   needs to be put back into the context of the parent type scheme, say
   as @{text more} part of another @{typ point}.
 
   To define generic operations, we need to know a bit more about
-  records.  Our definition of @{typ point} above generated two type
-  abbreviations:
+  records.  Our definition of @{typ point} above has generated two
+  type abbreviations:
 
   \medskip
   \begin{tabular}{l}
   @{typ point}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
   @{typ "'a point_scheme"}~@{text "="}~@{typ "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\

   @{typ point} (including @{typ cpoint} etc.):
 *}
 
 constdefs
   incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
-  "incX r \<equiv> \<lparr>Xcoord = Xcoord r + 1,
-    Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
+  "incX r \<equiv>
+    \<lparr>Xcoord = Xcoord r + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
 
 text {*
   Generic theorems can be proved about generic methods.  This trivial
   lemma relates @{text incX} to @{text getX} and @{text setX}:
 *}

 
 subsection {* Record Equality *}
 
 text {*
   Two records are equal\index{equality!of records} if all pairs of
-  corresponding fields are equal.  Record equalities are simplified
-  automatically:
+  corresponding fields are equal.  Concrete record equalities are
+  simplified automatically:
 *}
 
 lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) =
     (a = a' \<and> b = b')"
   by simp

 
 text {*
   The generic cases method does not admit references to locally bound
   parameters of a goal.  In longer proof scripts one might have to
   fall back on the primitive @{text rule_tac} used together with the
-  internal representation rules of records.  E.g.\ the above use of
-  @{text "(cases r)"} would become @{text "(rule_tac r = r in
+  internal field representation rules of records.  E.g.\ the above use
+  of @{text "(cases r)"} would become @{text "(rule_tac r = r in
   point.cases_scheme)"}.
 *}
 
 
 subsection {* Extending and Truncating Records *}