doc-src/TutorialI/Types/records.tex

 \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.
 

 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. 
-The effect resembles inheritance in object-oriented programming. 
-Extensible records make use of the reserved field \isa{more}, which is
+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 \isacommand{record} declaration
+representation.  A \commdx{record} declaration
 introduces a new record type:
 \begin{isabelle}
 \isacommand{record}\ point\ =\isanewline
 \ \ Xcoord\ ::\ int\isanewline
 \ \ Ycoord\ ::\ int

 \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}.
+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\ |\

 its colour, we must define operations that copy across the other
 fields.  However,  we can define generic operations
 that work on type
 \isa{point} and all extensions of it.
 
-Every record structure has an implicit field, \isa{more}, to allow
+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{...}:
+\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

 \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'') to get and set any point's \isa{Xcoord}
-field.  The sort constraint in \isa{'a::more} is required, since
-all extensions must belong to the type class \isa{more}.%
+let us define two operations --- methods, if we regard records as
+objects --- to get and set any point's
+\isa{Xcoord} field.  The sort constraint in \isa{'a::more} is
+required, since all extensions must belong to the type class
+\isa{more}.%
 \REMARK{Why, and what does this imply in practice?}
 \begin{isabelle}
 \ \ getX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ int"\isanewline
 \ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
 \ \ setX\ ::\ "[('a::more)\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline

 \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}
+\end{warn}%
+\index{records!extensible|)}
 
 
 \subsection{Record Equality}
 
-Two records are equal if all pairs of corresponding fields are equal. 
+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

 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}: a record is determined entirely
-by the values of its fields.
+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}

 we enter the lemma again:
 \begin{isabelle}
 \isacommand{lemma}\ "!!r.\ r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\
 a'"\isanewline
 \end{isabelle}
-The \isa{record_split} method replaces the record variable by an
+The \methdx{record_split} method replaces the record variable by an
 explicit record, listing all fields.  Even the field \isa{more} is
 included, since the record equality is generic.
 \begin{isabelle}
 \isacommand{apply}\ record_split\isanewline
 \ 1.\ \isasymAnd Xcoord\ Ycoord\ more.\isanewline

 replaced by equality of the corresponding fields.
 
 \begin{exercise}
 \REMARK{There should be some, but I can't think of any.} 
 \end{exercise}
+\index{records|)}
 
 \endinput