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--
     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 (*>*)