# HG changeset patch
# User wenzelm
# Date 1008879064 -3600
# Node ID 614ef5ca41ed31dc2878a70586c2bed171b79a6f
# Parent  fe20540bcf93d971a4c3fd786045631f8ed130d3
turned into proper Isabelle document;

diff -r fe20540bcf93 -r 614ef5ca41ed doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Thu Dec 20 18:22:44 2001 +0100
+++ b/doc-src/TutorialI/Types/Records.thy	Thu Dec 20 21:11:04 2001 +0100
@@ -1,265 +1,403 @@
-(*  Title:      HOL/ex/Records.thy
-    ID:         $Id$
-    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-    License:    GPL (GNU GENERAL PUBLIC LICENSE)
-*)
+
+header {* Records \label{sec:records} *}
+
+(*<*)
+theory Records = Main:
+(*>*)
+
+text {*
+  \index{records|(}%
+  Records are familiar from programming languages.  A record of $n$
+  fields is essentially an $n$-tuple, but the record's components have
+  names, which can make expressions easier to read and reduces the
+  risk of confusing one field for another.
 
-header {* Extensible Records  *}
+  A basic Isabelle record covers a certain set of fields, with select
+  and update operations.  Each field has a specified type, which may
+  be polymorphic.  The field names are part of the record type, and
+  the order of the fields is significant --- as it is in Pascal but
+  not in Standard ML.  If two different record types have field names
+  in common, then the ambiguity is resolved in the usual way, by
+  qualified names.
 
-theory Records = Main:
+  Record types can also be defined by extending other record types.
+  Extensible records make use of the reserved pseudo-field \cdx{more},
+  which is present in every record type.  Generic record operations
+  work on all possible extensions of a given type scheme; naive
+  polymorphism takes care of structural sub-typing behind the scenes.
+  There are also explicit coercion functions between fixed record
+  types.
+*}
+
 
-subsection {* Points *}
+subsection {* Record Basics *}
+
+text {*
+  Record types are not primitive in Isabelle and have a subtle
+  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 records as a separate concept.
+*}
 
 record point =
   Xcoord :: int
   Ycoord :: int
 
 text {*
- Apart many other things, above record declaration produces the
- following theorems:
+  Records of type @{typ point} have two fields named @{text Xcoord}
+  and @{text Ycoord}, both of type~@{typ int}.  We now define a
+  constant of type @{typ point}:
+*}
+
+constdefs
+  pt1 :: point
+  "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):
+*}
+
+constdefs
+  pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"
+  "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
+
+text {*
+  For each field, there is a \emph{selector} function of the same
+  name.  For example, if @{text p} has type @{typ point} then @{text
+  "Xcoord p"} denotes the value of the @{text Xcoord} field of~@{text
+  p}.  Expressions involving field selection of explicit records are
+  simplified automatically:
+*}
+
+lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b\<rparr> = a"
+  by simp
+
+text {*
+  The \emph{update} 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:
+*}
+
+lemma "\<lparr>Xcoord = a, Ycoord = b\<rparr>\<lparr>Xcoord := 0\<rparr> =
+    \<lparr>Xcoord = 0, Ycoord = b\<rparr>"
+  by simp
+
+text {*
+  \begin{warn}
+  Field names are declared as constants and can no longer be used as
+  variables.  It would be unwise, for example, to call the fields of
+  type @{typ point} simply @{text x} and~@{text y}.  Each record
+  declaration introduces a constant \cdx{more}.
+  \end{warn}
 *}
 
 
-thm "point.simps"
-text {*
-Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
-Updates, make, make_scheme and equality introduction (extensionality)
-*}
-
-thm "point.iffs"
-text {*
-@{thm[display] point.iffs}
-%%\rulename{point.iffs}
-Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord)
-*}
-
-thm "point.update_defs"
-text {*
-@{thm[display] point.update_defs}
-%%\rulename{point.update_defs}
-Definitions of updates to Xcoord and Ycoord, also "more"
-*}
+subsection {* Extensible Records and Generic Operations *}
 
 text {*
- The set of theorems @{thm [source] point.simps} is added
- automatically to the standard simpset, @{thm [source] point.iffs} is
- added to the Classical Reasoner and Simplifier context.
-*}
-
-text {* Exchanging Xcoord and Ycoord yields a different type: we must
-unfortunately write the fields in a canonical order.*}
-
-
-constdefs 
-  pt1 :: point
-   "pt1 == (| Xcoord = 999, Ycoord = 23 |)"
-
-  pt2 :: "(| Xcoord :: int, Ycoord :: int |)" 
-   "pt2 == (| Xcoord = -45, Ycoord = 97 |)" 
-
-
-subsubsection {* Some lemmas about records *}
+  \index{records!extensible|(}%
 
-text {* Basic simplifications. *}
-
-lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a"
-by simp -- "selection"
-
-lemma "(| Xcoord = a, Ycoord = b |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b |)"
-by simp -- "update"
-
-
-subsection {* Coloured points: record extension *}
-
-
-text {*
- Records are extensible.
- 
- The name@{text  "more"} is reserved, since it is used for extensibility.
+  Now, let us define coloured points (type @{text cpoint}) to be
+  points extended with a field @{text col} of type @{text colour}:
 *}
 
-
 datatype colour = Red | Green | Blue
 
 record cpoint = point +
   col :: colour
 
+text {*
+  The fields of this new type are @{text Xcoord}, @{text Ycoord} and
+  @{text col}, in that order:
+*}
 
-constdefs 
+constdefs
   cpt1 :: cpoint
-   "cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
-
+  "cpt1 \<equiv> \<lparr>Xcoord = 999, Ycoord = 23, col = Green\<rparr>"
 
-subsection {* Generic operations *}
-
+text {*
+  We can define generic operations that work on arbitrary instances of
+  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):
+*}
 
-text {* Record selection and record update; these are generic! *}
+lemma "Xcoord \<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = a"
+  by simp
 
-lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a"
-by simp -- "selection"
+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 actually the same as @{text "\<lparr>Xcoord = a,
+  Ycoord = b\<rparr>"}.
+
+  The pseudo-field @{text more} can be selected in the usual way, but
+  the identifier must be qualified:
+*}
 
 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
-by (simp add: cpt1_def) -- "tail of this record"
-
-
-lemma "(| Xcoord = a, Ycoord = b, ... = p |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b, ... = p |)"
-by simp -- "update"
+  by (simp add: cpt1_def)
 
 text {*
-  Record declarations define new type abbreviations:
-  @{text [display]
-"    point = (| Xcoord :: int, Ycoord :: int |)
-    'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
+  We see that the colour 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} in the above
+  fragment, @{text "\<lparr>col = Green\<rparr>"} needs to be put back into the
+  context of its parent type scheme, say as @{text more} part of a
+  @{typ point}.
+
+  To define generic operations, we need to know a bit more about
+  records.  Our declaration of @{typ point} above generated two type
+  abbreviations:
+
+  \smallskip
+  \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>"} \\
+  \end{tabular}
+  \smallskip
+
+  Type @{typ point} is for rigid records having exactly the two fields
+  @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
+  "'a point_scheme"} comprises all possible extensions to those two
+  fields, recall that @{typ "unit point_scheme"} coincides with @{typ
+  point}.  For example, let us define two operations --- methods, if
+  we regard records as objects --- to get and set any point's @{text
+  Xcoord} field.
 *}
 
 constdefs
   getX :: "'a point_scheme \<Rightarrow> int"
-   "getX r == Xcoord r"
-  setX :: "['a point_scheme, int] \<Rightarrow> 'a point_scheme"
-   "setX r a == r (| Xcoord := a |)"
-
-
+  "getX r \<equiv> Xcoord r"
+  setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme"
+  "setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
 
 text {*
- \medskip Concrete records are type instances of record schemes.
+  Here is a generic method that modifies a point, incrementing its
+  @{text Xcoord} field.  The @{text Ycoord} and @{text more} fields
+  are copied across.  It works for any record type scheme derived from
+  @{typ point}, such as @{typ cpoint}:
 *}
 
-lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64"
-by (simp add: getX_def) 
-
-
-text {* \medskip Manipulating the `...' (more) part.  beware: EACH record
-   has its OWN more field, so a compound name is required! *}
-
 constdefs
   incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
-  "incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
-
-constdefs
-  setGreen :: "[colour, 'a point_scheme] \<Rightarrow> cpoint"
-  "setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)"
-
-
-text {* works (I think) for ALL extensions of type point? *}
-
-lemma "incX r = setX r ((getX r) + 1)"
-by (simp add: getX_def setX_def incX_def)
-
-text {* An equivalent definition. *}
-lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>"
-by (simp add: incX_def)
-
-
+  "incX r \<equiv> \<lparr>Xcoord = Xcoord r + 1,
+    Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
 
 text {*
- Functions on @{text point} schemes work for type @{text cpoint} as
- well.  *}
+  Generic theorems can be proved about generic methods.  This trivial
+  lemma relates @{text incX} to @{text getX} and @{text setX}:
+*}
 
-lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23"
-by (simp add: getX_def)
-
-
-subsubsection {* Non-coercive structural subtyping *}
+lemma "incX r = setX r (getX r + 1)"
+  by (simp add: getX_def setX_def incX_def)
 
 text {*
- Function @{term setX} can be applied to type @{typ cpoint}, not just type
- @{typ point}, and returns a result of the same type!  *}
-
-lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 =  
-            \<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>"
-by (simp add: setX_def)
-
-
-subsection {* Other features *}
-
-text {* Field names (and order) contribute to record identity. *}
-
-
-text {* \medskip Polymorphic records. *}
-
-record 'a polypoint = point +
-  content :: 'a
-
-types cpolypoint = "colour polypoint"
+  \begin{warn}
+  If you use the symbolic record brackets @{text \<lparr>} and @{text \<rparr>},
+  then you must also use the symbolic ellipsis, ``@{text \<dots>}'', rather
+  than three consecutive periods, ``@{text "..."}''.  Mixing the ASCII
+  and symbolic versions causes a syntax error.  (The two versions are
+  more distinct on screen than they are on paper.)
+  \end{warn}%\index{records!extensible|)}
+*}
 
 
-subsection {* Equality of records. *}
+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:
+*}
+
+lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) =
+    (a = a' \<and> b = b')"
+  by simp
 
-lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')"
-  -- "simplification of concrete record equality"
-by simp
+text {*
+  The following equality is similar, but generic, in that @{text r}
+  can be any instance of @{text point_scheme}:
+*}
+
+lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
+  by simp
 
-text {* \medskip Surjective pairing *}
+text {*
+  We see above the syntax for iterated updates.  We could equivalently
+  have written the left-hand side as @{term "r\<lparr>Xcoord := a\<rparr>\<lparr>Ycoord
+  := b\<rparr>"}.
+
+  Record equality is \emph{extensional}: \index{extensionality!for
+  records} a record is determined entirely by the values of its
+  fields.
+*}
 
 lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
-by simp
-
+  by simp
 
+text {*
+  The generic version of this equality includes the field @{text
+  more}:
+*}
 
-lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>"
-by auto
+lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
+  by simp
 
 text {*
- A rigid record has ()::unit in its  name@{text "more"} part
+  Note that the @{text r} is of a different (more general) type than
+  the previous one.
+
+  \medskip The simplifier can prove many record equalities
+  automatically, but general equality reasoning can be tricky.
+  Consider proving this obvious fact:
+*}
+
+lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
+  apply simp?
+  oops
+
+text {*
+  The simplifier can do nothing, since general record equality is not
+  eliminated automatically.  One way to proceed is by an explicit
+  forward step that applies the selector @{text Xcoord} to both sides
+  of the assumed record equality:
 *}
 
-text {* a polymorphic record equality (covers all possible extensions) *}
-lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
-  -- "introduction of abstract record equality
-         (order of updates doesn't affect the value)"
-by simp
+lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
+  apply (drule_tac f = Xcoord in arg_cong)
+  txt {* @{subgoals [display, indent = 0, margin = 65]}
+    Now, @{text simp} will reduce the assumption to the desired
+    conclusion. *}
+  apply simp
+  done
+
+text {*
+  The @{text cases} method is preferable to such a forward proof.
+  State the desired lemma again:
+*}
 
-lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
-  -- "abstract record equality (the same with iterated updates)"
-by simp
+lemma "r\<lparr>Xcoord := a\<rparr> = r\<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
+  txt {*
+    The \methdx{cases} method adds an equality to replace the named
+    record variable by an explicit record, listing all fields.  It
+    even includes the pseudo-field @{text more}, since the record
+    equality stated above is generic. *}
+  apply (cases r)
 
-text {* Showing that repeated updates don't matter *}
-lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
-by simp
+  txt {* @{subgoals [display, indent = 0, margin = 65]}
+    Again, @{text simp} finishes the proof.  Because @{text r} has
+    become an explicit record expression, the updates can be applied
+    and the record equality can be replaced by equality of the
+    corresponding fields (due to injectivity). *}
+  apply simp
+  done
 
 
-text {* surjective *}
-
-lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
-by simp
-
+subsection {* Extending and Truncating Records *}
 
 text {*
- \medskip Splitting abstract record variables.
-*}
+  Each record declaration introduces functions to refer collectively
+  to a record's fields and to convert between related record types.
+  They can, for instance, convert between types @{typ point} and @{typ
+  cpoint}.  We can add a colour to a point or to convert a @{typ
+  cpoint} to a @{typ point} by forgetting its colour.
+
+  \begin{itemize}
+
+  \item Function \cdx{make} takes as arguments all of the record's
+  fields.  It returns the corresponding record.
+
+  \item Function \cdx{fields} takes the record's new fields and
+  returns a record fragment consisting of just those fields.  This may
+  be filled into the @{text more} part of the parent record scheme.
+
+  \item Function \cdx{extend} takes two arguments: a record to be
+  extended and a record containing the new fields.
+
+  \item Function \cdx{truncate} takes a record (possibly an extension
+  of the original record type) and returns a fixed record, removing
+  any additional fields.
+
+  \end{itemize}
 
-lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
-  -- "elimination of abstract record equality (manual proof, by selector)"
-apply (drule_tac f=Xcoord in arg_cong)
-    --{* @{subgoals[display,indent=0,margin=65]} *}
-by simp
+  These functions merely provide handsome abbreviations for standard
+  record expressions involving constructors and selectors.  The
+  definitions, which are \emph{not} unfolded by default, are made
+  available by the collective name of @{text defs} (e.g.\ @{text
+  point.defs} or @{text cpoint.defs}).
+
+  For example, here are the versions of those functions generated for
+  record @{typ point}.  We omit @{text point.fields}, which happens to
+  be the same as @{text point.make}.
 
-text {*So we replace the ugly manual proof by the "cases" method.*}
-lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
-apply (cases r)
-  --{* @{subgoals[display,indent=0,margin=65]} *}
-by simp
+  @{thm [display, indent = 0, margin = 65] point.make_def
+  point.extend_def point.truncate_def}
+
+  Contrast those with the corresponding functions for record @{typ
+  cpoint}.  Observe @{text cpoint.fields} in particular.
+
+  @{thm [display, indent = 0, margin = 65] cpoint.make_def
+  cpoint.extend_def cpoint.truncate_def}
+
+  To demonstrate these functions, we declare a new coloured point by
+  extending an ordinary point.  Function @{text point.extend} augments
+  @{text pt1} with a colour, which is converted into an appropriate
+  record fragment by @{text cpoint.fields}.
+*}
 
 constdefs
   cpt2 :: cpoint
-   "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
+  "cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
 
 text {*
-@{thm[display] point.defs}
-*};
+  The coloured points @{text cpt1} and @{text cpt2} are equal.  The
+  proof is trivial, by unfolding all the definitions.  We deliberately
+  omit the definition of~@{text pt1} in order to reveal the underlying
+  comparison on type @{typ point}.
+*}
+
+lemma "cpt1 = cpt2"
+  apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
+  txt {* @{subgoals [display, indent = 0, margin = 65]} *}
+  apply (simp add: pt1_def)
+  done
 
 text {*
-@{thm[display] cpoint.defs}
-*};
-
-text{*cpt2 is the same as cpt1, but defined by extending point pt1*}
-lemma "cpt1 = cpt2"
-apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
-	--{* @{subgoals[display,indent=0,margin=65]} *}
-by (simp add: pt1_def)
-
+  In the example below, a coloured point is truncated to leave a
+  point.  We must use the @{text truncate} function of the shorter
+  record.
+*}
 
 lemma "point.truncate cpt2 = pt1"
-by (simp add: pt1_def cpt2_def point.defs)
+  by (simp add: pt1_def cpt2_def point.defs)
+
+text {*
+  \begin{exercise}
+  Extend record @{typ cpoint} to have a further field, @{text
+  intensity}, of type~@{typ nat}.  Experiment with coercions among the
+  three record types.
+  \end{exercise}
 
+  \begin{exercise}
+  (For Java programmers.)
+  Model a small class hierarchy using records.
+  \end{exercise}
+  \index{records|)}
+*}
+
+(*<*)
 end
+(*>*)