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