# HG changeset patch
# User paulson
# Date 995282059 -7200
# Node ID 3ed58bbcf4bd86d22c71827d49bc64bec123b3f1
# Parent  f280d4b29a2ca34c75b25ebf388eead9c9ef3a3f
indexing

diff -r f280d4b29a2c -r 3ed58bbcf4bd doc-src/TutorialI/Types/records.tex
--- a/doc-src/TutorialI/Types/records.tex	Sun Jul 15 14:48:36 2001 +0200
+++ b/doc-src/TutorialI/Types/records.tex	Mon Jul 16 13:14:19 2001 +0200
@@ -1,6 +1,7 @@
 \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
@@ -14,8 +15,7 @@
 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.
@@ -23,7 +23,7 @@
 \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
@@ -71,12 +71,14 @@
 \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}:
@@ -104,12 +106,12 @@
 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}
@@ -137,9 +139,11 @@
 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
@@ -176,12 +180,14 @@
 \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 )\
@@ -203,8 +209,9 @@
 \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
@@ -244,7 +251,7 @@
 \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}
@@ -263,6 +270,7 @@
 \begin{exercise}
 \REMARK{There should be some, but I can't think of any.} 
 \end{exercise}
+\index{records|)}
 
 \endinput