# HG changeset patch
# User wenzelm
# Date 1008879282 -3600
# Node ID 0000276024e5d4f48c639e0ccab85417e8e790fd
# Parent  3bd2372e9bed164e0e3c7a51adb9d980bf321550
supplanted by Records.thy;

diff -r 3bd2372e9bed -r 0000276024e5 doc-src/TutorialI/Types/records.tex
--- a/doc-src/TutorialI/Types/records.tex	Thu Dec 20 21:13:36 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,342 +0,0 @@
-\section{Records} 
-\label{sec:records}
-
-\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 basic Isabelle record has a fixed set of fields, with access
-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 fields 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 field \cdx{more}, which is
-present in every record type.  Generic methods, or operations that
-work on all possible extensions of a given record, can be expressed by
-definitions involving \isa{more}, but the details are complicated.
-
-\subsection{Record Basics}
-
-Record types are not primitive in Isabelle and have a complex internal
-representation.  A \commdx{record} declaration
-introduces a new record type:
-\begin{isabelle}
-\isacommand{record}\ point\ =\isanewline
-\ \ Xcoord\ ::\ int\isanewline
-\ \ Ycoord\ ::\ int
-\end{isabelle}
-
-Records of type \isa{point} have two fields named \isa{Xcoord} and \isa{Ycoord},
-both of type~\isa{int}.  We now declare a constant of type
-\isa{point}:
-\begin{isabelle}
-\isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)"
-\end{isabelle}
-We see above the ASCII notation for record brackets.  You can also use
-the symbolic brackets \isa{\isasymlparr} and  \isa{\isasymrparr}.
-Record types can be written directly, without referring to
-previously declared names: 
-\begin{isabelle}
-\isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\
-|)"\ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)"
-\end{isabelle}
-
-For each field, there is a \emph{selector} function of the same name.  For
-example, if \isa{p} has type \isa{point} then \isa{Xcoord p} denotes the
-value of the \isa{Xcoord} field of~\isa{p}.  Expressions involving field
-selection are simplified automatically:
-\begin{isabelle}
-\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ =\ a"\isanewline
-\isacommand{by}\ simp
-\end{isabelle}
-The \emph{update} operation is functional.  For example,
-\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value
-is zero and whose
-\isa{Ycoord} value is copied from~\isa{p}.  Updates are also simplified
-automatically:
-\begin{isabelle}
-\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\
-=\isanewline
-\ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline
-\isacommand{by}\ simp
-\end{isabelle}
-
-\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 \isa{point} simply \isa{x} and~\isa{y}.  Each record
-declaration introduces a constant \cdx{more}.
-\end{warn}
-
-
-\subsection{Extensible Records and Generic Operations}
-
-\index{records!extensible|(}%
-Now, let us define coloured points
-(type \isa{cpoint}) to be points extended with a field \isa{col} of type
-\isa{colour}:
-\begin{isabelle}
-\isacommand{datatype}\ colour\ =\ Red\ |\ Green\ |\
-Blue\isanewline
-\isanewline
-\isacommand{record}\ cpoint\ =\ point\ +\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ col\ ::\ colour
-\end{isabelle}
-
-The fields of this new type are \isa{Xcoord}, \isa{Ycoord} and \isa{col}, in that
-order:
-\begin{isabelle}
-\isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\
-=\ Green\ |)"
-\end{isabelle}
-
-
-We can define generic operations that work on type \isa{point} and all
-extensions of it. 
-Every record structure has an implicit field, \cdx{more}, to allow
-extension.  Its type is completely polymorphic:~\isa{'a}.  When a
-record value is expressed using just its standard fields, the value of
-\isa{more} is implicitly set to \isa{()}, the empty tuple, which has
-type \isa{unit}.  Within the record brackets, you can refer to the
-\isa{more} field by writing \isa{...} (three periods):
-\begin{isabelle}
-\isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b,\ ...\ =\ p\ |)\ =\ a"
-\end{isabelle}
-This lemma (trivially proved using \isa{simp}) applies to any
-record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}.  Field
-\isa{more} can be selected in the usual way, but as all records have
-this field, the identifier must be qualified:
-\begin{isabelle}
-\isacommand{lemma}\ "point.more\ cpt1\ =\ \isasymlparr col\ =\ Green\isasymrparr "\isanewline
-\isacommand{by}\ (simp\ add:\ cpt1_def)
-\end{isabelle}
-%
-We see that the colour attached to this \isa{point} is a record in its
-own right, namely 
-\isa{\isasymlparr col\ =\ Green\isasymrparr}.
-
-To define generic operations, we need to know a bit more about records.
-Our declaration of \isa{point} above generated two type
-abbreviations:
-\begin{isabelle}
-\ \ \ \ point\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\ |)\isanewline
-\ \ \ \ 'a\ point_scheme\ =\ (|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int,\ ...\ ::\ 'a\ |)
-\end{isabelle}
-%
-Type \isa{point} is for rigid records having the two fields
-\isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{'a\ point_scheme}
-comprises all possible extensions to those two fields.  For example,
-let us define two operations --- methods, if we regard records as
-objects --- to get and set any point's
-\isa{Xcoord} field. 
-\begin{isabelle}
-\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline
-\ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
-\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
-\ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)"
-\end{isabelle}
-
-Here is a generic method that modifies a point, incrementing its
-\isa{Xcoord} field.  The \isa{Ycoord} and \isa{more} fields
-are copied across.  It works for type \isa{point} and any of its
-extensions, such as \isa{cpoint}:
-\begin{isabelle}
-\isacommand{constdefs}\isanewline
-\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
-\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\
-r\isasymrparr"
-\end{isabelle}
-
-Generic theorems can be proved about generic methods.  This trivial
-lemma relates \isa{incX} to \isa{getX} and \isa{setX}:
-\begin{isabelle}
-\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline
-\isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def)
-\end{isabelle}
-
-\begin{warn}
-If you use the symbolic record brackets \isa{\isasymlparr} and 
-\isa{\isasymrparr}, then you must also use the symbolic ellipsis,
-\isa{\isasymdots}, rather than three consecutive periods,
-\isa{...}.  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}
-
-Two records are equal\index{equality!of records}
-if all pairs of corresponding fields are equal. 
-Record equalities are simplified automatically:
-\begin{isabelle}
-\isacommand{lemma}\ "(\isasymlparr Xcoord\ =\ a,\ Ycoord\ =\ b\isasymrparr \ =\ \isasymlparr Xcoord\ =\ a',\ Ycoord\ =\ b'\isasymrparr )\
-=\isanewline
-\ \ \ \ \ \ \ \ (a\ =\ a'\ \&\ b\ =\ b')"\isanewline
-\isacommand{by}\ simp
-\end{isabelle}
-
-The following equality is similar, but generic, in that \isa{r} can
-be any instance of \isa{point_scheme}:
-\begin{isabelle}
-\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a,\ Ycoord\ :=\
-b\isasymrparr \ =\ r\ \isasymlparr Ycoord\ :=\ b,\ Xcoord\ :=\
-a\isasymrparr "\isanewline
-\isacommand{by}\ simp
-\end{isabelle}
-We see above the syntax for iterated updates.  We could equivalently
-have written the left-hand side as
-\isa{r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ \isasymlparr
-Ycoord\ :=\ b\isasymrparr}.
-
-Record equality is \emph{extensional}:
-\index{extensionality!for records} 
-a record is determined entirely by the values of its fields.
-\begin{isabelle}
-\isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\
-Ycoord\ r\isasymrparr "\isanewline
-\isacommand{by}\ simp
-\end{isabelle}
-The generic version of this equality includes the field \isa{more}:
-\begin{isabelle}
-\ \ \ \ r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ Ycoord\ r,\ \isasymdots \ =\ point.more\
-r\isasymrparr
-\end{isabelle}
-
-\medskip
-The simplifier can prove many record equalities automatically,
-but general equality reasoning can be tricky.  Consider proving this
-obvious fact:
-\begin{isabelle}
-\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\
-a'"
-\end{isabelle}
-The simplifier can do nothing.  One way to proceed is by an explicit
-forward step that applies the selector \isa{Xcoord} to both sides
-of the assumed record equality:
-\begin{isabelle}
-\isacommand{apply}\ (drule_tac\ f=Xcoord\ \isakeyword{in}\ arg_cong)\isanewline
-\ 1.\ Xcoord\ (r\isasymlparr Xcoord\ :=\ a\isasymrparr )\ =\ Xcoord\
-(r\isasymlparr Xcoord\ :=\ a'\isasymrparr )\ \isasymLongrightarrow \
-a\ =\ a'
-\end{isabelle}
-Now, \isa{simp} will reduce the assumption to the desired
-conclusion.
-
-The \isa{cases} method is preferable to such a forward proof.  
-State the desired lemma again:
-\begin{isabelle}
-\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\ a'"
-\end{isabelle}
-The \methdx{cases} method adds an equality to replace
-the named record variable by an explicit record, listing all fields.  
-It even includes the field \isa{more}, since the record equality is generic.
-\begin{isabelle}
-\isacommand{apply}\ (cases\ r)\isanewline
-\ 1.\ \isasymAnd Xcoord\ Ycoord\ more.\isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymlbrakk r\isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\isasymlparr Xcoord\ :=\ a'\isasymrparr ;\isanewline
-\isaindent{\ 1.\ \ \ \ \ \ \ }r\ =\ \isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isasymrbrakk \isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ a\ =\ a'
-\end{isabelle}
-Again, \isa{simp} finishes the proof.  Because \isa{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.
-
-
-\subsection{Extending and Truncating Records}
-
-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 \isa{point} and \isa{cpoint}.  We can add a
-colour to a point or to convert a \isa{cpoint} to a \isa{point} by forgetting
-its colour.
-
-\begin{itemize}
-\item Function \isa{make} takes as arguments all of the record's fields.
-  It returns the corresponding record. 
-\item If the record type is an extension of another, 
-      function \isa{fields} takes the record's new fields
-      and returns a record consisting of just those fields.  
-\item Function \isa{extend} takes two arguments: a record to be extended and a
-  record containing the new fields.
-\item Function \isa{truncate} takes a record (possibly an extension of the
-  original record type) and returns a record of the original type, deleting
-  any additional fields.
-\end{itemize}
-
-For example, here are the versions of those functions generated for record
-\isa{point}.  We omit \isa{point.fields}, which is the same as 
-\isa{point.make}.
-\begin{isabelle}
-point.make\ ?Xcoord\ ?Ycoord\ \isasymequiv \isanewline\smallskip
-\ \ \isasymlparr Xcoord\ =\ ?Xcoord,\ Ycoord\ =\ ?Ycoord\isasymrparr \isanewline
-point.extend\ ?r\ ?more\ \isasymequiv \isanewline\smallskip
-\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ \isasymdots \ =\ ?more\isasymrparr \isanewline\smallskip
-point.truncate\ ?r\ \isasymequiv \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r\isasymrparr 
-\end{isabelle}
-
-Contrast those with the corresponding functions for record \isa{cpoint}.
-Observe \isa{cpoint.fields} in particular.
-\begin{isabelle}
-cpoint.make\ ?Xcoord\ ?Ycoord\ ?col\ \isasymequiv \isanewline
-\ \ \isasymlparr Xcoord\ =\ ?Xcoord,\ Ycoord\ =\ ?Ycoord,\ col\ =\ ?col\isasymrparr \par\smallskip
-cpoint.fields\ ?col\ \isasymequiv \ \isasymlparr col\ =\ ?col\isasymrparr \par\smallskip
-cpoint.extend\ ?r\ ?more\ \isasymequiv \par
-\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ col\ =\ col\ ?r,\isanewline
-\isaindent{\ \ \ }\isasymdots \ =\ ?more\isasymrparr \par\smallskip
-cpoint.truncate\ ?r\ \isasymequiv \par
-\ \ \isasymlparr Xcoord\ =\ Xcoord\ ?r,\ Ycoord\ =\ Ycoord\ ?r,\ col\ =\ col\ ?r\isasymrparr 
-\end{isabelle}
-
-To demonstrate these functions, we declare a new coloured point by extending
-an ordinary point.  Function \isa{point.extend} augments \isa{pt1} with a
-colour, which is converted into a record by \isa{cpoint.fields}.
-\begin{isabelle}
-\isacommand{constdefs}\isanewline
-\ \ cpt2\ ::\ cpoint\isanewline
-\ \ \ "cpt2\ \isasymequiv\ point.extend\ pt1\ (cpoint.fields\ Green)"\isamarkupfalse%
-\end{isabelle}
-
-The coloured points \isa{cpt1} and \isa{cpt2} are equal.  The proof is
-trivial, by unfolding all the definitions.  We deliberately omit the
-definition of~\isa{pt1} in order to reveal the underlying comparison on type
-\isa{point}. 
-\begin{isabelle}
-\isacommand{lemma}\ "cpt1\ =\ cpt2"\isanewline
-\isacommand{apply}\ (simp\ add:\ cpt1_def\ cpt2_def\ point.defs\ cpoint.defs)\isanewline
-\ 1.\ Xcoord\ pt1\ =\ 999\ \isasymand \ Ycoord\ pt1\ =\ 23
-\par\smallskip
-\isacommand{by}\ (simp\ add:\ pt1_def)
-\end{isabelle}
-
-In the example below, a coloured point is truncated to leave a point.  
-We must use the \isa{truncate} function of the shorter record.
-\begin{isabelle}
-\isacommand{lemma}\ "point.truncate\ cpt2\ =\ pt1"\isanewline
-\isacommand{by}\ (simp\ add:\ pt1_def\ cpt2_def\ point.defs)
-\end{isabelle}
-
-\begin{exercise}
-Extend record \isa{cpoint} to have a further field, \isa{intensity}, of
-type~\isa{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|)}
-
-\endinput
-