
diff -r f51d4a302962 -r 5386df44a037 doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,408 +0,0 @@
-
-header {* Records \label{sec:records} *}
-
-(*<*)
-theory Records imports Main begin
-(*>*)
-
-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.
-
-  A record of Isabelle/HOL covers a collection 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.
-
-  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; polymorphism
-  takes care of structural sub-typing behind the scenes.  There are
-  also explicit coercion functions between fixed record types.
-*}
-
-
-subsection {* Record Basics *}
-
-text {*
-  Record types are not primitive in Isabelle and have a delicate
-  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 simple example:
-*}
-
-record point =
-  Xcoord :: int
-  Ycoord :: int
-
-text {*\noindent
-  Records of type @{typ point} have two fields named @{const Xcoord}
-  and @{const Ycoord}, both of type~@{typ int}.  We now define a
-  constant of type @{typ point}:
-*}
-
-definition pt1 :: point where
-"pt1 \<equiv> (| Xcoord = 999, Ycoord = 23 |)"
-
-text {*\noindent
-  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 also written directly with individual fields.
-  The type name above is merely an abbreviation.
-*}
-
-definition pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>" where
-"pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"
-
-text {*
-  For each field, there is a \emph{selector}\index{selector!record}
-  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}\index{update!record} operation is functional.  For
-  example, @{term "p\<lparr>Xcoord := 0\<rparr>"} is a record whose @{const Xcoord}
-  value is zero and whose @{const Ycoord} value is copied from~@{text
-  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
-
-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}.
-  \end{warn}
-*}
-
-
-subsection {* Extensible Records and Generic Operations *}
-
-text {*
-  \index{records!extensible|(}%
-
-  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 {*\noindent
-  The fields of this new type are @{const Xcoord}, @{text Ycoord} and
-  @{text col}, in that order.
-*}
-
-definition cpt1 :: cpoint where
-"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 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):
-*}
-
-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~@{const 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 {*\noindent
-  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 has generated two
-  type abbreviations:
-
-  \medskip
-  \begin{tabular}{l}
-  @{typ point}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"} \\
-  @{typ "'a point_scheme"}~@{text "="}~@{text "\<lparr>Xcoord :: int, Ycoord :: int, \<dots> :: 'a\<rparr>"} \\
-  \end{tabular}
-  \medskip
-  
-\noindent
-  Type @{typ point} is for fixed records having exactly the two fields
-  @{const Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ
-  "'a point_scheme"} comprises all possible extensions to those two
-  fields.  Note that @{typ "unit point_scheme"} coincides with @{typ
-  point}, and @{typ "\<lparr>col :: colour\<rparr> point_scheme"} with @{typ
-  cpoint}.
-
-  In the following example we define two operations --- methods, if we
-  regard records as objects --- to get and set any point's @{text
-  Xcoord} field.
-*}
-
-definition getX :: "'a point_scheme \<Rightarrow> int" where
-"getX r \<equiv> Xcoord r"
-definition setX :: "'a point_scheme \<Rightarrow> int \<Rightarrow> 'a point_scheme" where
-"setX r a \<equiv> r\<lparr>Xcoord := a\<rparr>"
-
-text {*
-  Here is a generic method that modifies a point, incrementing its
-  @{const Xcoord} field.  The @{text Ycoord} and @{text more} fields
-  are copied across.  It works for any record type scheme derived from
-  @{typ point} (including @{typ cpoint} etc.):
-*}
-
-definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" where
-"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 @{const incX} to @{text getX} and @{text setX}:
-*}
-
-lemma "incX r = setX r (getX r + 1)"
-  by (simp add: getX_def setX_def incX_def)
-
-text {*
-  \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 {* Record Equality *}
-
-text {*
-  Two records are equal\index{equality!of records} if all pairs of
-  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 following equality is similar, but generic, in that @{text r}
-  can be any instance of @{typ "'a point_scheme"}:
-*}
-
-lemma "r\<lparr>Xcoord := a, Ycoord := b\<rparr> = r\<lparr>Ycoord := b, Xcoord := a\<rparr>"
-  by simp
-
-text {*\noindent
-  We see above the syntax for iterated updates.  We could equivalently
-  have written the left-hand side as @{text "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
-
-text {*\noindent
-  The generic version of this equality includes the pseudo-field
-  @{text more}:
-*}
-
-lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
-  by simp
-
-text {*
-  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 {*\noindent
-  Here 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 @{const Xcoord} to both sides
-  of the assumed record equality:
-*}
-
-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.  We
-  state the desired lemma again:
-*}
-
-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 term by an explicit record expression, listing all
-  fields.  It even includes the pseudo-field @{text more}, since the
-  record equality stated here is generic for all extensions. *}
-
-  apply (cases r)
-
-  txt {* @{subgoals [display, indent = 0, margin = 65]} Again, @{text
-  simp} finishes the proof.  Because @{text r} is now represented as
-  an explicit record construction, 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 {*
-  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 field representation rules of records.  The above use of
-  @{text "(cases r)"} would become @{text "(rule_tac r = r in
-  point.cases_scheme)"}.
-*}
-
-
-subsection {* Extending and Truncating Records *}
-
-text {*
-  Each record declaration introduces a number of derived operations to
-  refer collectively to a record's fields and to convert between fixed
-  record types.  They can, for instance, convert between types @{typ
-  point} and @{typ cpoint}.  We can add a colour to a point or 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 (including those inherited from ancestors).  It returns the
-  corresponding record.
-
-  \item Function \cdx{fields} takes the record's very own 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}
-  These functions provide useful 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} (@{text
-  point.defs}, @{text cpoint.defs}, etc.).
-  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}.
-
-  @{thm [display, indent = 0, margin = 65] point.make_def [no_vars]
-  point.extend_def [no_vars] point.truncate_def [no_vars]}
-  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 [no_vars]
-  cpoint.fields_def [no_vars] cpoint.extend_def [no_vars]
-  cpoint.truncate_def [no_vars]}
-
-  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 value, which is converted into an
-  appropriate record fragment by @{text cpoint.fields}.
-*}
-
-definition cpt2 :: cpoint where
-"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
-
-text {*
-  The coloured points @{const 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 {*
-  In the example below, a coloured point is truncated to leave a
-  point.  We use the @{text truncate} function of the target record.
-*}
-
-lemma "point.truncate cpt2 = pt1"
-  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 generic operations
-  (using polymorphic selectors and updates) and explicit coercions
-  (using @{text extend}, @{text truncate} etc.) among the three record
-  types.
-  \end{exercise}
-
-  \begin{exercise}
-  (For Java programmers.)
-  Model a small class hierarchy using records.
-  \end{exercise}
-  \index{records|)}
-*}
-
-(*<*)
-end
-(*>*)




