indexing
authorpaulson
Mon Jul 16 13:14:19 2001 +0200 (2001-07-16)
changeset 114273ed58bbcf4bd
parent 11426 f280d4b29a2c
child 11428 332347b9b942
indexing
doc-src/TutorialI/Types/records.tex
     1.1 --- a/doc-src/TutorialI/Types/records.tex	Sun Jul 15 14:48:36 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Types/records.tex	Mon Jul 16 13:14:19 2001 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  \section{Records} 
     1.5  \label{sec:records}
     1.6  
     1.7 +\index{records|(}%
     1.8  Records are familiar from programming languages.  A record of $n$
     1.9  fields is essentially an $n$-tuple, but the record's components have
    1.10  names, which can make expressions easier to read and reduces the risk
    1.11 @@ -14,8 +15,7 @@
    1.12  then the ambiguity is resolved in the usual way, by qualified names.
    1.13  
    1.14  Record types can also be defined by extending other record types. 
    1.15 -The effect resembles inheritance in object-oriented programming. 
    1.16 -Extensible records make use of the reserved field \isa{more}, which is
    1.17 +Extensible records make use of the reserved field \cdx{more}, which is
    1.18  present in every record type.  Generic methods, or operations that
    1.19  work on all possible extensions of a given record, can be expressed by
    1.20  definitions involving \isa{more}, but the details are complicated.
    1.21 @@ -23,7 +23,7 @@
    1.22  \subsection{Record Basics}
    1.23  
    1.24  Record types are not primitive in Isabelle and have a complex internal
    1.25 -representation.  A \isacommand{record} declaration
    1.26 +representation.  A \commdx{record} declaration
    1.27  introduces a new record type:
    1.28  \begin{isabelle}
    1.29  \isacommand{record}\ point\ =\isanewline
    1.30 @@ -71,12 +71,14 @@
    1.31  \begin{warn}
    1.32  Field names are declared as constants and can no longer be
    1.33  used as variables.  It would be unwise, for example, to call the fields
    1.34 -of type \isa{point} simply \isa{x} and~\isa{y}.
    1.35 +of type \isa{point} simply \isa{x} and~\isa{y}.  Each record
    1.36 +declaration introduces a constant \cdx{more}.
    1.37  \end{warn}
    1.38  
    1.39  
    1.40  \subsection{Extensible Records and Generic Operations}
    1.41  
    1.42 +\index{records!extensible|(}%
    1.43  Now, let us define coloured points
    1.44  (type \isa{cpoint}) to be points extended with a field \isa{col} of type
    1.45  \isa{colour}:
    1.46 @@ -104,12 +106,12 @@
    1.47  that work on type
    1.48  \isa{point} and all extensions of it.
    1.49  
    1.50 -Every record structure has an implicit field, \isa{more}, to allow
    1.51 +Every record structure has an implicit field, \cdx{more}, to allow
    1.52  extension.  Its type is completely polymorphic:~\isa{'a}.  When a
    1.53  record value is expressed using just its standard fields, the value of
    1.54  \isa{more} is implicitly set to \isa{()}, the empty tuple, which has
    1.55  type \isa{unit}.  Within the record brackets, you can refer to the
    1.56 -\isa{more} field by writing \isa{...}:
    1.57 +\isa{more} field by writing \isa{...} (three periods):
    1.58  \begin{isabelle}
    1.59  \isacommand{lemma}\ "Xcoord\ (|\ Xcoord\ =\ a,\ Ycoord\ =\ b,\ ...\ =\ p\ |)\ =\ a"
    1.60  \end{isabelle}
    1.61 @@ -137,9 +139,11 @@
    1.62  Type \isa{point} is for rigid records having the two fields
    1.63  \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{'a\ point_scheme}
    1.64  comprises all possible extensions to those two fields.  For example,
    1.65 -let us define two operations (``methods'') to get and set any point's \isa{Xcoord}
    1.66 -field.  The sort constraint in \isa{'a::more} is required, since
    1.67 -all extensions must belong to the type class \isa{more}.%
    1.68 +let us define two operations --- methods, if we regard records as
    1.69 +objects --- to get and set any point's
    1.70 +\isa{Xcoord} field.  The sort constraint in \isa{'a::more} is
    1.71 +required, since all extensions must belong to the type class
    1.72 +\isa{more}.%
    1.73  \REMARK{Why, and what does this imply in practice?}
    1.74  \begin{isabelle}
    1.75  \ \ getX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ int"\isanewline
    1.76 @@ -176,12 +180,14 @@
    1.77  \isa{...}.  Mixing the ASCII and symbolic versions
    1.78  causes a syntax error.  (The two versions are more
    1.79  distinct on screen than they are on paper.)
    1.80 -\end{warn}
    1.81 +\end{warn}%
    1.82 +\index{records!extensible|)}
    1.83  
    1.84  
    1.85  \subsection{Record Equality}
    1.86  
    1.87 -Two records are equal if all pairs of corresponding fields are equal. 
    1.88 +Two records are equal\index{equality!of records}
    1.89 +if all pairs of corresponding fields are equal. 
    1.90  Record equalities are simplified automatically:
    1.91  \begin{isabelle}
    1.92  \isacommand{lemma}\ "(\isasymlparr Xcoord\ =\ a,\ Ycoord\ =\ b\isasymrparr \ =\ \isasymlparr Xcoord\ =\ a',\ Ycoord\ =\ b'\isasymrparr )\
    1.93 @@ -203,8 +209,9 @@
    1.94  \isa{r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ \isasymlparr
    1.95  Ycoord\ :=\ b\isasymrparr}.
    1.96  
    1.97 -Record equality is \emph{extensional}: a record is determined entirely
    1.98 -by the values of its fields.
    1.99 +Record equality is \emph{extensional}:
   1.100 +\index{extensionality!for records} 
   1.101 +a record is determined entirely by the values of its fields.
   1.102  \begin{isabelle}
   1.103  \isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\
   1.104  Ycoord\ r\isasymrparr "\isanewline
   1.105 @@ -244,7 +251,7 @@
   1.106  \isacommand{lemma}\ "!!r.\ r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\
   1.107  a'"\isanewline
   1.108  \end{isabelle}
   1.109 -The \isa{record_split} method replaces the record variable by an
   1.110 +The \methdx{record_split} method replaces the record variable by an
   1.111  explicit record, listing all fields.  Even the field \isa{more} is
   1.112  included, since the record equality is generic.
   1.113  \begin{isabelle}
   1.114 @@ -263,6 +270,7 @@
   1.115  \begin{exercise}
   1.116  \REMARK{There should be some, but I can't think of any.} 
   1.117  \end{exercise}
   1.118 +\index{records|)}
   1.119  
   1.120  \endinput
   1.121