# HG changeset patch # User wenzelm # Date 1008964705 -3600 # Node ID e3cb192aa6ee9055896d916c44a5032f7286021e # Parent cf5a342ce69831f648538a1b080edac946c7186d updated; diff -r cf5a342ce698 -r e3cb192aa6ee doc-src/TutorialI/Types/document/Records.tex --- a/doc-src/TutorialI/Types/document/Records.tex Fri Dec 21 19:56:42 2001 +0100 +++ b/doc-src/TutorialI/Types/document/Records.tex Fri Dec 21 20:58:25 2001 +0100 @@ -14,7 +14,7 @@ names, which can make expressions easier to read and reduces the risk of confusing one field for another. - A basic Isabelle record covers a certain set of fields, with select + 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 @@ -25,10 +25,9 @@ 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; naive - polymorphism takes care of structural sub-typing behind the scenes. - There are also explicit coercion functions between fixed record - types.% + 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.% \end{isamarkuptext}% \isamarkuptrue% % @@ -37,11 +36,11 @@ \isamarkuptrue% % \begin{isamarkuptext}% -Record types are not primitive in Isabelle and have a subtle +Record types are not primitive in Isabelle and have a delicate internal representation 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 records as a separate concept.% + to hold up the perception of the record as a distinguished entity.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{record}\ point\ {\isacharequal}\isanewline @@ -71,9 +70,9 @@ \ \ {\isachardoublequote}pt{\isadigit{2}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharminus}{\isadigit{4}}{\isadigit{5}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{7}}{\isasymrparr}{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptext}% -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 of explicit records are - simplified automatically:% +For each field, there is a \emph{selector}\index{selector!record} + 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 + of explicit records are simplified automatically:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline @@ -81,9 +80,9 @@ \isacommand{by}\ simp\isamarkupfalse% % \begin{isamarkuptext}% -The \emph{update} operation is functional. For example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{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:% +The \emph{update}\index{update!record} operation is functional. For + example, \isa{p{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{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:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline @@ -95,8 +94,7 @@ \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}. + type \isa{point} simply \isa{x} and~\isa{y}. \end{warn}% \end{isamarkuptext}% \isamarkuptrue% @@ -144,10 +142,11 @@ \isacommand{by}\ simp\isamarkupfalse% % \begin{isamarkuptext}% -This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Note that \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}} is actually the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}. +This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}. Note that \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}} is really the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}. Selectors and updates are always polymorphic wrt.\ the \isa{more} part of a record scheme, its value is just ignored (for + select) or copied (for update). - The pseudo-field \isa{more} can be selected in the usual way, but - the identifier must be qualified:% + The \isa{more} pseudo-field may be manipulated directly as well, + but the identifier needs to be qualified:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline @@ -156,26 +155,27 @@ % \begin{isamarkuptext}% We see that the colour attached to this \isa{point} is a - (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col} in the above - fragment, \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}} needs to be put back into the - context of its parent type scheme, say as \isa{more} part of a - \isa{point}. + (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}. In order to select or update \isa{col}, this fragment + needs to be put back into the context of the parent type scheme, say + as \isa{more} part of another \isa{point}. To define generic operations, we need to know a bit more about - records. Our declaration of \isa{point} above generated two type + records. Our definition of \isa{point} above generated two type abbreviations: - \smallskip + \medskip \begin{tabular}{l} \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\ \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\ \end{tabular} - \smallskip + \medskip - Type \isa{point} is for rigid records having exactly the two fields + Type \isa{point} is for fixed records having exactly the two fields \isa{Xcoord} and~\isa{Ycoord}, while the polymorphic type \isa{{\isacharprime}a\ point{\isacharunderscore}scheme} comprises all possible extensions to those two - fields, recall that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}. For example, let us define two operations --- methods, if - we regard records as objects --- to get and set any point's \isa{Xcoord} field.% + fields. Note that \isa{unit\ point{\isacharunderscore}scheme} coincides with \isa{point}, and \isa{{\isasymlparr}col\ {\isacharcolon}{\isacharcolon}\ colour{\isasymrparr}\ point{\isacharunderscore}scheme} with \isa{cpoint}. + + In the following example we define two operations --- methods, if we + regard records as objects --- to get and set any point's \isa{Xcoord} field.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{constdefs}\isanewline @@ -188,7 +188,7 @@ 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 any record type scheme derived from - \isa{point}, such as \isa{cpoint}:% + \isa{point} (including \isa{cpoint} etc.):% \end{isamarkuptext}% \isamarkuptrue% \isacommand{constdefs}\isanewline @@ -233,7 +233,7 @@ % \begin{isamarkuptext}% The following equality is similar, but generic, in that \isa{r} - can be any instance of \isa{point{\isacharunderscore}scheme}:% + can be any instance of \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isanewline @@ -242,11 +242,11 @@ % \begin{isamarkuptext}% We see above the syntax for iterated updates. We could equivalently - have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}. + have written the left-hand side as \isa{r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}}. - Record equality is \emph{extensional}: \index{extensionality!for - records} a record is determined entirely by the values of its - fields.% + \medskip Record equality is \emph{extensional}: + \index{extensionality!for records} a record is determined entirely + by the values of its fields.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline @@ -254,7 +254,8 @@ \isacommand{by}\ simp\isamarkupfalse% % \begin{isamarkuptext}% -The generic version of this equality includes the field \isa{more}:% +The generic version of this equality includes the pseudo-field + \isa{more}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline @@ -262,10 +263,7 @@ \isacommand{by}\ simp\isamarkupfalse% % \begin{isamarkuptext}% -Note that the \isa{r} is of a different (more general) type than - the previous one. - - \medskip The simplifier can prove many record equalities +\medskip The simplifier can prove many record equalities automatically, but general equality reasoning can be tricky. Consider proving this obvious fact:% \end{isamarkuptext}% @@ -277,8 +275,8 @@ \isacommand{oops}\isamarkupfalse% % \begin{isamarkuptext}% -The simplifier can do nothing, since general record equality is not - eliminated automatically. One way to proceed is by an explicit +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 \isa{Xcoord} to both sides of the assumed record equality:% \end{isamarkuptext}% @@ -300,17 +298,17 @@ \isacommand{done}\isamarkupfalse% % \begin{isamarkuptext}% -The \isa{cases} method is preferable to such a forward proof. - State the desired lemma again:% +The \isa{cases} method is preferable to such a forward proof. We + state the desired lemma again:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptxt}% -The \methdx{cases} method adds an equality to replace the named - record variable by an explicit record, listing all fields. It - even includes the pseudo-field \isa{more}, since the record - equality stated above is generic.% +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 \isa{more}, since the + record equality stated here is generic for all extensions.% \end{isamarkuptxt}% \ \ \isamarkuptrue% \isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse% @@ -321,32 +319,42 @@ \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}% -\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 (due to injectivity).% +\end{isabelle} Again, \isa{simp} finishes the proof. Because \isa{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).% \end{isamarkuptxt}% \ \ \isamarkuptrue% \isacommand{apply}\ simp\isanewline \ \ \isamarkupfalse% \isacommand{done}\isamarkupfalse% % +\begin{isamarkuptext}% +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 \isa{rule{\isacharunderscore}tac} used together with the + internal representation rules of records. E.g.\ the above use of + \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Extending and Truncating Records% } \isamarkuptrue% % \begin{isamarkuptext}% -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. +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 \isa{point} and \isa{cpoint}. We can add a colour to a point or convert + a \isa{cpoint} to a \isa{point} by forgetting its colour. \begin{itemize} \item Function \cdx{make} takes as arguments all of the record's - fields. It returns the corresponding record. + fields (including those inherited from ancestors). It returns the + corresponding record. - \item Function \cdx{fields} takes the record's new fields and + \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 \isa{more} part of the parent record scheme. @@ -362,34 +370,35 @@ These functions merely provide handsome 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 \isa{defs} (e.g.\ \isa{point{\isachardot}defs} or \isa{cpoint{\isachardot}defs}). + available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.). For example, here are the versions of those functions generated for record \isa{point}. We omit \isa{point{\isachardot}fields}, which happens to be the same as \isa{point{\isachardot}make}. \begin{isabelle}% -point{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isasymrparr}\isanewline -point{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline -point{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isasymrparr}% +point{\isachardot}make\ Xcoord\ Ycoord\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isasymrparr}\isanewline +point{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline +point{\isachardot}truncate\ r\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}% \end{isabelle} Contrast those with the corresponding functions for record \isa{cpoint}. Observe \isa{cpoint{\isachardot}fields} in particular. \begin{isabelle}% -cpoint{\isachardot}make\ {\isacharquery}Xcoord\ {\isacharquery}Ycoord\ {\isacharquery}col\ {\isasymequiv}\isanewline -{\isasymlparr}Xcoord\ {\isacharequal}\ {\isacharquery}Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isacharquery}Ycoord{\isacharcomma}\ col\ {\isacharequal}\ {\isacharquery}col{\isasymrparr}\isanewline -cpoint{\isachardot}extend\ {\isacharquery}r\ {\isacharquery}more\ {\isasymequiv}\isanewline -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharquery}more{\isasymrparr}\isanewline -cpoint{\isachardot}truncate\ {\isacharquery}r\ {\isasymequiv}\isanewline -{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ {\isacharquery}r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ {\isacharquery}r{\isacharcomma}\ col\ {\isacharequal}\ col\ {\isacharquery}r{\isasymrparr}% +cpoint{\isachardot}make\ Xcoord\ Ycoord\ col\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ col\ {\isacharequal}\ col{\isasymrparr}\isanewline +cpoint{\isachardot}fields\ col\ {\isasymequiv}\ {\isasymlparr}col\ {\isacharequal}\ col{\isasymrparr}\isanewline +cpoint{\isachardot}extend\ r\ more\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}\isanewline +cpoint{\isachardot}truncate\ r\ {\isasymequiv}\isanewline +{\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ col\ {\isacharequal}\ col\ r{\isasymrparr}% \end{isabelle} To demonstrate these functions, we declare a new coloured point by extending an ordinary point. Function \isa{point{\isachardot}extend} augments - \isa{pt{\isadigit{1}}} with a colour, which is converted into an appropriate - record fragment by \isa{cpoint{\isachardot}fields}.% + \isa{pt{\isadigit{1}}} with a colour value, which is converted into an + appropriate record fragment by \isa{cpoint{\isachardot}fields}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{constdefs}\isanewline @@ -419,8 +428,7 @@ % \begin{isamarkuptext}% In the example below, a coloured point is truncated to leave a - point. We must use the \isa{truncate} function of the shorter - record.% + point. We use the \isa{truncate} function of the target record.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline @@ -429,8 +437,10 @@ % \begin{isamarkuptext}% \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. + Extend record \isa{cpoint} to have a further field, \isa{intensity}, of type~\isa{nat}. Experiment with generic operations + (using polymorphic selectors and updates) and explicit coercions + (using \isa{extend}, \isa{truncate} etc.) among the three record + types. \end{exercise} \begin{exercise} diff -r cf5a342ce698 -r e3cb192aa6ee doc-src/TutorialI/tutorial.ind --- a/doc-src/TutorialI/tutorial.ind Fri Dec 21 19:56:42 2001 +0100 +++ b/doc-src/TutorialI/tutorial.ind Fri Dec 21 20:58:25 2001 +0100 @@ -1,139 +1,139 @@ \begin{theindex} - \item \ttall, \bold{199} - \item \texttt{?}, \bold{199} - \item \isasymuniqex, \bold{199} - \item \ttuniquex, \bold{199} - \item {\texttt {\&}}, \bold{199} - \item \verb$~$, \bold{199} - \item \verb$~=$, \bold{199} - \item \ttor, \bold{199} + \item \ttall, \bold{201} + \item \texttt{?}, \bold{201} + \item \isasymuniqex, \bold{201} + \item \ttuniquex, \bold{201} + \item {\texttt {\&}}, \bold{201} + \item \verb$~$, \bold{201} + \item \verb$~=$, \bold{201} + \item \ttor, \bold{201} \item \texttt{[]}, \bold{9} \item \texttt{\#}, \bold{9} - \item \texttt{\at}, \bold{10}, 199 - \item \isasymnotin, \bold{199} - \item \verb$~:$, \bold{199} - \item \isasymInter, \bold{199} - \item \isasymUnion, \bold{199} - \item \isasyminverse, \bold{199} - \item \verb$^-1$, \bold{199} - \item \isactrlsup{\isacharasterisk}, \bold{199} - \item \verb$^$\texttt{*}, \bold{199} - \item \isasymAnd, \bold{12}, \bold{199} - \item \ttAnd, \bold{199} - \item \isasymrightleftharpoons, 26 - \item \isasymrightharpoonup, 26 - \item \isasymleftharpoondown, 26 + \item \texttt{\at}, \bold{10}, 201 + \item \isasymnotin, \bold{201} + \item \verb$~:$, \bold{201} + \item \isasymInter, \bold{201} + \item \isasymUnion, \bold{201} + \item \isasyminverse, \bold{201} + \item \verb$^-1$, \bold{201} + \item \isactrlsup{\isacharasterisk}, \bold{201} + \item \verb$^$\texttt{*}, \bold{201} + \item \isasymAnd, \bold{12}, \bold{201} + \item \ttAnd, \bold{201} + \item \isasymrightleftharpoons, 55 + \item \isasymrightharpoonup, 55 + \item \isasymleftharpoondown, 55 \item \emph {$\Rightarrow $}, \bold{5} - \item \ttlbr, \bold{199} - \item \ttrbr, \bold{199} - \item \texttt {\%}, \bold{199} + \item \ttlbr, \bold{201} + \item \ttrbr, \bold{201} + \item \texttt {\%}, \bold{201} \item \texttt {;}, \bold{7} \item \isa {()} (constant), 24 - \item \isa {+} (tactical), 89 + \item \isa {+} (tactical), 91 \item \isa {<*lex*>}, \see{lexicographic product}{1} - \item \isa {?} (tactical), 89 - \item \texttt{|} (tactical), 89 + \item \isa {?} (tactical), 91 + \item \texttt{|} (tactical), 91 \indexspace - \item \isa {0} (constant), 22, 23, 140 - \item \isa {1} (constant), 23, 140, 141 + \item \isa {0} (constant), 22, 23, 142 + \item \isa {1} (constant), 23, 142, 143 \indexspace \item abandoning a proof, \bold{13} \item abandoning a theory, \bold{16} - \item \isa {abs} (constant), 143 - \item \texttt {abs}, \bold{199} - \item absolute value, 143 + \item \isa {abs} (constant), 145 + \item \texttt {abs}, \bold{201} + \item absolute value, 145 \item \isa {add} (modifier), 29 - \item \isa {add_ac} (theorems), 142 - \item \isa {add_assoc} (theorem), \bold{142} - \item \isa {add_commute} (theorem), \bold{142} - \item \isa {add_mult_distrib} (theorem), \bold{141} - \item \texttt {ALL}, \bold{199} - \item \isa {All} (constant), 99 - \item \isa {allE} (theorem), \bold{71} - \item \isa {allI} (theorem), \bold{70} + \item \isa {add_ac} (theorems), 144 + \item \isa {add_assoc} (theorem), \bold{144} + \item \isa {add_commute} (theorem), \bold{144} + \item \isa {add_mult_distrib} (theorem), \bold{143} + \item \texttt {ALL}, \bold{201} + \item \isa {All} (constant), 101 + \item \isa {allE} (theorem), \bold{73} + \item \isa {allI} (theorem), \bold{72} \item append function, 10--14 \item \isacommand {apply} (command), 15 - \item \isa {arg_cong} (theorem), \bold{86} - \item \isa {arith} (method), 23, 139 + \item \isa {arg_cong} (theorem), \bold{88} + \item \isa {arith} (method), 23, 141 \item arithmetic operations \subitem for \protect\isa{nat}, 23 - \item \textsc {ascii} symbols, \bold{199} - \item associative-commutative function, 166 - \item \isa {assumption} (method), 59 + \item \textsc {ascii} symbols, \bold{201} + \item associative-commutative function, 168 + \item \isa {assumption} (method), 61 \item assumptions \subitem of subgoal, 12 - \subitem renaming, 72--73 - \subitem reusing, 73 - \item \isa {auto} (method), 38, 82 - \item \isa {axclass}, 154--160 - \item axiom of choice, 76 - \item axiomatic type classes, 154--160 + \subitem renaming, 74--75 + \subitem reusing, 75 + \item \isa {auto} (method), 38, 84 + \item \isa {axclass}, 156--162 + \item axiom of choice, 78 + \item axiomatic type classes, 156--162 \indexspace - \item \isacommand {back} (command), 68 - \item \isa {Ball} (constant), 99 - \item \isa {ballI} (theorem), \bold{98} - \item \isa {best} (method), 82 - \item \isa {Bex} (constant), 99 - \item \isa {bexE} (theorem), \bold{98} - \item \isa {bexI} (theorem), \bold{98} - \item \isa {bij_def} (theorem), \bold{100} - \item bijections, 100 + \item \isacommand {back} (command), 70 + \item \isa {Ball} (constant), 101 + \item \isa {ballI} (theorem), \bold{100} + \item \isa {best} (method), 84 + \item \isa {Bex} (constant), 101 + \item \isa {bexE} (theorem), \bold{100} + \item \isa {bexI} (theorem), \bold{100} + \item \isa {bij_def} (theorem), \bold{102} + \item bijections, 102 \item binary trees, 18 - \item binomial coefficients, 99 - \item bisimulations, 106 - \item \isa {blast} (method), 79--80, 82 + \item binomial coefficients, 101 + \item bisimulations, 108 + \item \isa {blast} (method), 81--82, 84 \item \isa {bool} (type), 4, 5 \item boolean expressions example, 20--22 - \item \isa {bspec} (theorem), \bold{98} - \item \isacommand{by} (command), 63 + \item \isa {bspec} (theorem), \bold{100} + \item \isacommand{by} (command), 65 \indexspace - \item \isa {card} (constant), 99 - \item \isa {card_Pow} (theorem), \bold{99} - \item \isa {card_Un_Int} (theorem), \bold{99} - \item cardinality, 99 + \item \isa {card} (constant), 101 + \item \isa {card_Pow} (theorem), \bold{101} + \item \isa {card_Un_Int} (theorem), \bold{101} + \item cardinality, 101 \item \isa {case} (symbol), 32, 33 \item \isa {case} expressions, 5, 6, 18 \item case distinctions, 19 \item case splits, \bold{31} - \item \isa {case_tac} (method), 19, 91, 147 - \item \isa {cases} (method), 152 - \item \isa {clarify} (method), 81, 82 - \item \isa {clarsimp} (method), 81, 82 - \item \isa {classical} (theorem), \bold{63} - \item coinduction, \bold{106} - \item \isa {Collect} (constant), 99 + \item \isa {case_tac} (method), 19, 93, 149 + \item \isa {cases} (method), 154 + \item \isa {clarify} (method), 83, 84 + \item \isa {clarsimp} (method), 83, 84 + \item \isa {classical} (theorem), \bold{65} + \item coinduction, \bold{108} + \item \isa {Collect} (constant), 101 \item compiling expressions example, 36--38 - \item \isa {Compl_iff} (theorem), \bold{96} + \item \isa {Compl_iff} (theorem), \bold{98} \item complement - \subitem of a set, 95 + \subitem of a set, 97 \item composition - \subitem of functions, \bold{100} - \subitem of relations, \bold{102} + \subitem of functions, \bold{102} + \subitem of relations, \bold{104} \item conclusion \subitem of subgoal, 12 \item conditional expressions, \see{\isa{if} expressions}{1} \item conditional simplification rules, 31 - \item \isa {cong} (attribute), 166 - \item congruence rules, \bold{165} - \item \isa {conjE} (theorem), \bold{61} - \item \isa {conjI} (theorem), \bold{58} + \item \isa {cong} (attribute), 168 + \item congruence rules, \bold{167} + \item \isa {conjE} (theorem), \bold{63} + \item \isa {conjI} (theorem), \bold{60} \item \isa {Cons} (constant), 9 \item \isacommand {constdefs} (command), 25 \item \isacommand {consts} (command), 10 - \item contrapositives, 63 + \item contrapositives, 65 \item converse - \subitem of a relation, \bold{102} - \item \isa {converse_iff} (theorem), \bold{102} - \item CTL, 111--116, 181--183 + \subitem of a relation, \bold{104} + \item \isa {converse_iff} (theorem), \bold{104} + \item CTL, 113--118, 183--185 \indexspace @@ -141,179 +141,179 @@ \item datatypes, 17--22 \subitem and nested recursion, 40, 44 \subitem mutually recursive, 38 - \subitem nested, 170 - \item \isacommand {defer} (command), 16, 90 + \subitem nested, 172 + \item \isacommand {defer} (command), 16, 92 \item Definitional Approach, 26 \item definitions, \bold{25} \subitem unfolding, \bold{30} \item \isacommand {defs} (command), 25 \item \isa {del} (modifier), 29 - \item description operators, 75--77 + \item description operators, 77--79 \item descriptions - \subitem definite, 75 - \subitem indefinite, 76 - \item \isa {dest} (attribute), 92 - \item destruction rules, 61 - \item \isa {diff_mult_distrib} (theorem), \bold{141} + \subitem definite, 77 + \subitem indefinite, 78 + \item \isa {dest} (attribute), 94 + \item destruction rules, 63 + \item \isa {diff_mult_distrib} (theorem), \bold{143} \item difference - \subitem of sets, \bold{96} - \item \isa {disjCI} (theorem), \bold{64} - \item \isa {disjE} (theorem), \bold{60} + \subitem of sets, \bold{98} + \item \isa {disjCI} (theorem), \bold{66} + \item \isa {disjE} (theorem), \bold{62} \item \isa {div} (symbol), 23 - \item divides relation, 74, 85, 91--94, 142 + \item divides relation, 76, 87, 93--96, 144 \item division - \subitem by negative numbers, 143 - \subitem by zero, 142 - \subitem for type \protect\isa{nat}, 141 + \subitem by negative numbers, 145 + \subitem by zero, 144 + \subitem for type \protect\isa{nat}, 143 \item domain - \subitem of a relation, 102 - \item \isa {Domain_iff} (theorem), \bold{102} + \subitem of a relation, 104 + \item \isa {Domain_iff} (theorem), \bold{104} \item \isacommand {done} (command), 13 - \item \isa {drule_tac} (method), 66, 86 - \item \isa {dvd_add} (theorem), \bold{142} - \item \isa {dvd_anti_sym} (theorem), \bold{142} - \item \isa {dvd_def} (theorem), \bold{142} + \item \isa {drule_tac} (method), 68, 88 + \item \isa {dvd_add} (theorem), \bold{144} + \item \isa {dvd_anti_sym} (theorem), \bold{144} + \item \isa {dvd_def} (theorem), \bold{144} \indexspace - \item \isa {elim!} (attribute), 121 - \item elimination rules, 59--60 + \item \isa {elim!} (attribute), 123 + \item elimination rules, 61--62 \item \isacommand {end} (command), 14 - \item \isa {Eps} (constant), 99 + \item \isa {Eps} (constant), 101 \item equality, 5 - \subitem of functions, \bold{99} - \subitem of records, 151 - \subitem of sets, \bold{96} - \item \isa {equalityE} (theorem), \bold{96} - \item \isa {equalityI} (theorem), \bold{96} - \item \isa {erule} (method), 60 - \item \isa {erule_tac} (method), 66 - \item Euclid's algorithm, 91--94 + \subitem of functions, \bold{101} + \subitem of records, 153 + \subitem of sets, \bold{98} + \item \isa {equalityE} (theorem), \bold{98} + \item \isa {equalityI} (theorem), \bold{98} + \item \isa {erule} (method), 62 + \item \isa {erule_tac} (method), 68 + \item Euclid's algorithm, 93--96 \item even numbers - \subitem defining inductively, 117--121 - \item \texttt {EX}, \bold{199} - \item \isa {Ex} (constant), 99 - \item \isa {exE} (theorem), \bold{72} - \item \isa {exI} (theorem), \bold{72} - \item \isa {ext} (theorem), \bold{99} - \item \isa {extend} (constant), 153 + \subitem defining inductively, 119--123 + \item \texttt {EX}, \bold{201} + \item \isa {Ex} (constant), 101 + \item \isa {exE} (theorem), \bold{74} + \item \isa {exI} (theorem), \bold{74} + \item \isa {ext} (theorem), \bold{101} + \item \isa {extend} (constant), 155 \item extensionality - \subitem for functions, \bold{99, 100} - \subitem for records, 151 - \subitem for sets, \bold{96} - \item \ttEXU, \bold{199} + \subitem for functions, \bold{101, 102} + \subitem for records, 153 + \subitem for sets, \bold{98} + \item \ttEXU, \bold{201} \indexspace \item \isa {False} (constant), 5 - \item \isa {fast} (method), 82, 114 + \item \isa {fast} (method), 84, 116 \item Fibonacci function, 47 - \item \isa {fields} (constant), 153 - \item \isa {finite} (symbol), 99 - \item \isa {Finites} (constant), 99 - \item fixed points, 106 + \item \isa {fields} (constant), 155 + \item \isa {finite} (symbol), 101 + \item \isa {Finites} (constant), 101 + \item fixed points, 108 \item flags, 5, 6, 33 \subitem setting and resetting, 5 - \item \isa {force} (method), 81, 82 + \item \isa {force} (method), 83, 84 \item formulae, 5--6 - \item forward proof, 82--88 - \item \isa {frule} (method), 73 - \item \isa {frule_tac} (method), 66 + \item forward proof, 84--90 + \item \isa {frule} (method), 75 + \item \isa {frule_tac} (method), 68 \item \isa {fst} (constant), 24 \item function types, 5 - \item functions, 99--101 - \subitem partial, 172 + \item functions, 101--103 + \subitem partial, 174 \subitem total, 11, 46--52 - \subitem underdefined, 173 + \subitem underdefined, 175 \indexspace - \item \isa {gcd} (constant), 83--84, 91--94 - \item generalizing for induction, 119 + \item \isa {gcd} (constant), 85--86, 93--96 + \item generalizing for induction, 121 \item generalizing induction formulae, 35 - \item Girard, Jean-Yves, \fnote{61} + \item Girard, Jean-Yves, \fnote{63} \item Gordon, Mike, 3 \item grammars - \subitem defining inductively, 130--135 - \item ground terms example, 125--130 + \subitem defining inductively, 132--137 + \item ground terms example, 127--132 \indexspace \item \isa {hd} (constant), 17, 37 - \item Hilbert's $\varepsilon$-operator, 76 + \item Hilbert's $\varepsilon$-operator, 78 \item HOLCF, 43 - \item Hopcroft, J. E., 135 - \item \isa {hypreal} (type), 145 + \item Hopcroft, J. E., 137 + \item \isa {hypreal} (type), 147 \indexspace - \item \isa {Id_def} (theorem), \bold{102} - \item \isa {id_def} (theorem), \bold{100} + \item \isa {Id_def} (theorem), \bold{104} + \item \isa {id_def} (theorem), \bold{102} \item identifiers, \bold{6} \subitem qualified, \bold{4} - \item identity function, \bold{100} - \item identity relation, \bold{102} + \item identity function, \bold{102} + \item identity relation, \bold{104} \item \isa {if} expressions, 5, 6 \subitem simplification of, 33 \subitem splitting of, 31, 49 \item if-and-only-if, 6 - \item \isa {iff} (attribute), 80, 92, 120 - \item \isa {iffD1} (theorem), \bold{84} - \item \isa {iffD2} (theorem), \bold{84} + \item \isa {iff} (attribute), 82, 94, 122 + \item \isa {iffD1} (theorem), \bold{86} + \item \isa {iffD2} (theorem), \bold{86} \item image - \subitem under a function, \bold{101} - \subitem under a relation, \bold{102} - \item \isa {image_def} (theorem), \bold{101} - \item \isa {Image_iff} (theorem), \bold{102} - \item \isa {impI} (theorem), \bold{62} - \item implication, 62--63 - \item \isa {ind_cases} (method), 121 - \item \isa {induct_tac} (method), 12, 19, 52, 180 - \item induction, 176--183 - \subitem complete, 178 - \subitem deriving new schemas, 180 - \subitem on a term, 177 + \subitem under a function, \bold{103} + \subitem under a relation, \bold{104} + \item \isa {image_def} (theorem), \bold{103} + \item \isa {Image_iff} (theorem), \bold{104} + \item \isa {impI} (theorem), \bold{64} + \item implication, 64--65 + \item \isa {ind_cases} (method), 123 + \item \isa {induct_tac} (method), 12, 19, 52, 182 + \item induction, 178--185 + \subitem complete, 180 + \subitem deriving new schemas, 182 + \subitem on a term, 179 \subitem recursion, 51--52 \subitem structural, 19 - \subitem well-founded, 105 + \subitem well-founded, 107 \item induction heuristics, 34--36 - \item \isacommand {inductive} (command), 117 + \item \isacommand {inductive} (command), 119 \item inductive definition - \subitem simultaneous, 131 - \item inductive definitions, 117--135 - \item \isacommand {inductive\_cases} (command), 121, 129 + \subitem simultaneous, 133 + \item inductive definitions, 119--137 + \item \isacommand {inductive\_cases} (command), 123, 131 \item infinitely branching trees, 43 \item \isacommand{infixr} (annotation), 10 - \item \isa {inj_on_def} (theorem), \bold{100} - \item injections, 100 - \item \isa {insert} (constant), 97 - \item \isa {insert} (method), 87--88 - \item instance, \bold{155} - \item \texttt {INT}, \bold{199} - \item \texttt {Int}, \bold{199} - \item \isa {int} (type), 143--144 - \item \isa {INT_iff} (theorem), \bold{98} - \item \isa {IntD1} (theorem), \bold{95} - \item \isa {IntD2} (theorem), \bold{95} - \item integers, 143--144 - \item \isa {INTER} (constant), 99 - \item \texttt {Inter}, \bold{199} - \item \isa {Inter_iff} (theorem), \bold{98} - \item intersection, 95 - \subitem indexed, 98 - \item \isa {IntI} (theorem), \bold{95} - \item \isa {intro} (method), 64 - \item \isa {intro!} (attribute), 118 - \item \isa {intro_classes} (method), 155 - \item introduction rules, 58--59 - \item \isa {inv} (constant), 76 - \item \isa {inv_image_def} (theorem), \bold{105} + \item \isa {inj_on_def} (theorem), \bold{102} + \item injections, 102 + \item \isa {insert} (constant), 99 + \item \isa {insert} (method), 89--90 + \item instance, \bold{158} + \item \texttt {INT}, \bold{201} + \item \texttt {Int}, \bold{201} + \item \isa {int} (type), 145--146 + \item \isa {INT_iff} (theorem), \bold{100} + \item \isa {IntD1} (theorem), \bold{97} + \item \isa {IntD2} (theorem), \bold{97} + \item integers, 145--146 + \item \isa {INTER} (constant), 101 + \item \texttt {Inter}, \bold{201} + \item \isa {Inter_iff} (theorem), \bold{100} + \item intersection, 97 + \subitem indexed, 100 + \item \isa {IntI} (theorem), \bold{97} + \item \isa {intro} (method), 66 + \item \isa {intro!} (attribute), 120 + \item \isa {intro_classes} (method), 158 + \item introduction rules, 60--61 + \item \isa {inv} (constant), 78 + \item \isa {inv_image_def} (theorem), \bold{107} \item inverse - \subitem of a function, \bold{100} - \subitem of a relation, \bold{102} + \subitem of a function, \bold{102} + \subitem of a relation, \bold{104} \item inverse image - \subitem of a function, 101 - \subitem of a relation, 104 + \subitem of a function, 103 + \subitem of a relation, 106 \item \isa {itrev} (constant), 34 \indexspace @@ -324,99 +324,99 @@ \item $\lambda$ expressions, 5 \item LCF, 43 - \item \isa {LEAST} (symbol), 23, 75 - \item least number operator, \see{\protect\isa{LEAST}}{75} + \item \isa {LEAST} (symbol), 23, 77 + \item least number operator, \see{\protect\isa{LEAST}}{77} \item \isacommand {lemma} (command), 13 - \item \isacommand {lemmas} (command), 83, 92 + \item \isacommand {lemmas} (command), 85, 94 \item \isa {length} (symbol), 18 - \item \isa {length_induct}, \bold{180} - \item \isa {less_than} (constant), 104 - \item \isa {less_than_iff} (theorem), \bold{104} + \item \isa {length_induct}, \bold{182} + \item \isa {less_than} (constant), 106 + \item \isa {less_than_iff} (theorem), \bold{106} \item \isa {let} expressions, 5, 6, 31 \item \isa {Let_def} (theorem), 31 - \item \isa {lex_prod_def} (theorem), \bold{105} - \item lexicographic product, \bold{105}, 168 + \item \isa {lex_prod_def} (theorem), \bold{107} + \item lexicographic product, \bold{107}, 170 \item {\texttt{lfp}} - \subitem applications of, \see{CTL}{106} + \subitem applications of, \see{CTL}{108} \item Library, 4 - \item linear arithmetic, 22--24, 139 + \item linear arithmetic, 22--24, 141 \item \isa {List} (theory), 17 \item \isa {list} (type), 5, 9, 17 \item \isa {list.split} (theorem), 32 - \item \isa {lists_mono} (theorem), \bold{127} - \item Lowe, Gavin, 186--187 + \item \isa {lists_mono} (theorem), \bold{129} + \item Lowe, Gavin, 188--189 \indexspace \item \isa {Main} (theory), 4 - \item major premise, \bold{65} - \item \isa {make} (constant), 153 + \item major premise, \bold{67} + \item \isa {make} (constant), 155 \item \isa {max} (constant), 23, 24 - \item measure functions, 47, 104 - \item \isa {measure_def} (theorem), \bold{105} - \item meta-logic, \bold{70} + \item measure functions, 47, 106 + \item \isa {measure_def} (theorem), \bold{107} + \item meta-logic, \bold{72} \item methods, \bold{16} \item \isa {min} (constant), 23, 24 \item \isa {mod} (symbol), 23 - \item \isa {mod_div_equality} (theorem), \bold{141} - \item \isa {mod_mult_distrib} (theorem), \bold{141} - \item model checking example, 106--116 - \item \emph{modus ponens}, 57, 62 - \item \isa {mono_def} (theorem), \bold{106} - \item monotone functions, \bold{106}, 129 - \subitem and inductive definitions, 127--128 - \item \isa {more} (constant), 148--150 - \item \isa {mp} (theorem), \bold{62} - \item \isa {mult_ac} (theorems), 142 - \item multiple inheritance, \bold{159} - \item multiset ordering, \bold{105} + \item \isa {mod_div_equality} (theorem), \bold{143} + \item \isa {mod_mult_distrib} (theorem), \bold{143} + \item model checking example, 108--118 + \item \emph{modus ponens}, 59, 64 + \item \isa {mono_def} (theorem), \bold{108} + \item monotone functions, \bold{108}, 131 + \subitem and inductive definitions, 129--130 + \item \isa {more} (constant), 150, 152 + \item \isa {mp} (theorem), \bold{64} + \item \isa {mult_ac} (theorems), 144 + \item multiple inheritance, \bold{161} + \item multiset ordering, \bold{107} \indexspace - \item \isa {nat} (type), 4, 22, 141--143 - \item \isa {nat_less_induct} (theorem), 178 - \item natural deduction, 57--58 - \item natural numbers, 22, 141--143 - \item Needham-Schroeder protocol, 185--187 - \item negation, 63--65 + \item \isa {nat} (type), 4, 22, 143--145 + \item \isa {nat_less_induct} (theorem), 180 + \item natural deduction, 59--60 + \item natural numbers, 22, 143--145 + \item Needham-Schroeder protocol, 187--189 + \item negation, 65--67 \item \isa {Nil} (constant), 9 \item \isa {no_asm} (modifier), 29 \item \isa {no_asm_simp} (modifier), 30 \item \isa {no_asm_use} (modifier), 30 - \item non-standard reals, 145 + \item non-standard reals, 147 \item \isa {None} (constant), \bold{24} - \item \isa {notE} (theorem), \bold{63} - \item \isa {notI} (theorem), \bold{63} - \item numbers, 139--145 - \item numeric literals, 140 - \subitem for type \protect\isa{nat}, 141 - \subitem for type \protect\isa{real}, 145 + \item \isa {notE} (theorem), \bold{65} + \item \isa {notI} (theorem), \bold{65} + \item numbers, 141--147 + \item numeric literals, 142 + \subitem for type \protect\isa{nat}, 143 + \subitem for type \protect\isa{real}, 147 \indexspace - \item \isa {O} (symbol), 102 - \item \texttt {o}, \bold{199} - \item \isa {o_def} (theorem), \bold{100} - \item \isa {OF} (attribute), 85--86 - \item \isa {of} (attribute), 83, 86 + \item \isa {O} (symbol), 104 + \item \texttt {o}, \bold{201} + \item \isa {o_def} (theorem), \bold{102} + \item \isa {OF} (attribute), 87--88 + \item \isa {of} (attribute), 85, 88 \item \isa {only} (modifier), 29 \item \isacommand {oops} (command), 13 \item \isa {option} (type), \bold{24} - \item ordered rewriting, \bold{166} - \item overloading, 23, 154--157 - \subitem and arithmetic, 140 + \item ordered rewriting, \bold{168} + \item overloading, 23, 157--159 + \subitem and arithmetic, 142 \indexspace - \item pairs and tuples, 24, 145--148 + \item pairs and tuples, 24, 147--150 \item parent theories, \bold{4} \item pattern matching \subitem and \isacommand{recdef}, 47 \item patterns - \subitem higher-order, \bold{167} - \item PDL, 108--110 - \item \isacommand {pr} (command), 16, 90 - \item \isacommand {prefer} (command), 16, 90 + \subitem higher-order, \bold{169} + \item PDL, 110--112 + \item \isacommand {pr} (command), 16, 92 + \item \isacommand {prefer} (command), 16, 92 \item primitive recursion, \see{recursion, primitive}{1} \item \isacommand {primrec} (command), 10, 18, 38--43 \item product type, \see{pairs and tuples}{1} @@ -424,75 +424,77 @@ \item proof state, 12 \item proofs \subitem abandoning, \bold{13} - \subitem examples of failing, 77--79 + \subitem examples of failing, 79--81 \item protocols - \subitem security, 185--195 + \subitem security, 187--197 \indexspace \item quantifiers, 6 - \subitem and inductive definitions, 125--127 - \subitem existential, 72 - \subitem for sets, 98 - \subitem instantiating, 74 - \subitem universal, 69--72 + \subitem and inductive definitions, 127--129 + \subitem existential, 74 + \subitem for sets, 100 + \subitem instantiating, 76 + \subitem universal, 71--74 \indexspace - \item \isa {r_into_rtrancl} (theorem), \bold{102} - \item \isa {r_into_trancl} (theorem), \bold{103} + \item \isa {r_into_rtrancl} (theorem), \bold{104} + \item \isa {r_into_trancl} (theorem), \bold{105} \item range - \subitem of a function, 101 - \subitem of a relation, 102 - \item \isa {range} (symbol), 101 - \item \isa {Range_iff} (theorem), \bold{102} - \item \isa {Real} (theory), 145 - \item \isa {real} (type), 144--145 - \item real numbers, 144--145 - \item \isacommand {recdef} (command), 46--52, 104, 168--176 - \subitem and numeric literals, 140 - \item \isa {recdef_cong} (attribute), 172 + \subitem of a function, 103 + \subitem of a relation, 104 + \item \isa {range} (symbol), 103 + \item \isa {Range_iff} (theorem), \bold{104} + \item \isa {Real} (theory), 147 + \item \isa {real} (type), 146--147 + \item real numbers, 146--147 + \item \isacommand {recdef} (command), 46--52, 106, 170--178 + \subitem and numeric literals, 142 + \item \isa {recdef_cong} (attribute), 174 \item \isa {recdef_simp} (attribute), 49 - \item \isa {recdef_wf} (attribute), 170 - \item \isacommand {record} (command), 149 - \item records, 148--154 - \subitem extensible, 150 + \item \isa {recdef_wf} (attribute), 172 + \item \isacommand {record} (command), 151 + \item records, 150--156 + \subitem extensible, 152 \item recursion - \subitem guarded, 173 + \subitem guarded, 175 \subitem primitive, 18 - \subitem well-founded, \bold{169} + \subitem well-founded, \bold{171} \item recursion induction, 51--52 \item \isacommand {redo} (command), 16 - \item reflexive and transitive closure, 102--104 + \item reflexive and transitive closure, 104--106 \item reflexive transitive closure - \subitem defining inductively, 122--125 - \item \isa {rel_comp_def} (theorem), \bold{102} - \item relations, 101--104 - \subitem well-founded, 104--105 - \item \isa {rename_tac} (method), 72--73 + \subitem defining inductively, 124--127 + \item \isa {rel_comp_def} (theorem), \bold{104} + \item relations, 103--106 + \subitem well-founded, 106--107 + \item \isa {rename_tac} (method), 74--75 \item \isa {rev} (constant), 10--14, 34 \item rewrite rules, \bold{27} - \subitem permutative, \bold{166} + \subitem permutative, \bold{168} \item rewriting, \bold{27} \item \isa {rotate_tac} (method), 30 - \item \isa {rtrancl_refl} (theorem), \bold{102} - \item \isa {rtrancl_trans} (theorem), \bold{102} - \item rule induction, 118--120 - \item rule inversion, 120--121, 129--130 - \item \isa {rule_format} (attribute), 177 - \item \isa {rule_tac} (method), 66 - \subitem and renaming, 73 + \item \isa {rtrancl_refl} (theorem), \bold{104} + \item \isa {rtrancl_trans} (theorem), \bold{104} + \item rule induction, 120--122 + \item rule inversion, 122--123, 131--132 + \item \isa {rule_format} (attribute), 179 + \item \isa {rule_tac} (method), 68 + \subitem and renaming, 75 \indexspace - \item \isa {safe} (method), 81, 82 - \item safe rules, \bold{80} - \item \isa {set} (type), 5, 95 - \item set comprehensions, 97--98 - \item \isa {set_ext} (theorem), \bold{96} - \item sets, 95--99 - \subitem finite, 99 - \subitem notation for finite, \bold{97} + \item \isa {safe} (method), 83, 84 + \item safe rules, \bold{82} + \item selector + \subitem record, 151 + \item \isa {set} (type), 5, 97 + \item set comprehensions, 99--100 + \item \isa {set_ext} (theorem), \bold{98} + \item sets, 97--101 + \subitem finite, 101 + \subitem notation for finite, \bold{99} \item settings, \see{flags}{1} \item \isa {show_brackets} (flag), 6 \item \isa {show_types} (flag), 5, 16 @@ -500,61 +502,61 @@ \item \isa {simp} (method), \bold{28} \item \isa {simp} del (attribute), 28 \item \isa {simp_all} (method), 29, 38 - \item simplification, 27--33, 165--168 + \item simplification, 27--33, 167--170 \subitem of \isa{let}-expressions, 31 \subitem with definitions, 30 \subitem with/of assumptions, 29 - \item simplification rule, 167--168 + \item simplification rule, 169--170 \item simplification rules, 28 \subitem adding and deleting, 29 - \item \isa {simplified} (attribute), 83, 86 + \item \isa {simplified} (attribute), 85, 88 \item \isa {size} (constant), 17 \item \isa {snd} (constant), 24 - \item \isa {SOME} (symbol), 76 - \item \texttt {SOME}, \bold{199} + \item \isa {SOME} (symbol), 78 + \item \texttt {SOME}, \bold{201} \item \isa {Some} (constant), \bold{24} - \item \isa {some_equality} (theorem), \bold{76} - \item \isa {someI} (theorem), \bold{76} - \item \isa {someI2} (theorem), \bold{76} - \item \isa {someI_ex} (theorem), \bold{77} - \item sorts, 159 - \item \isa {spec} (theorem), \bold{70} + \item \isa {some_equality} (theorem), \bold{78} + \item \isa {someI} (theorem), \bold{78} + \item \isa {someI2} (theorem), \bold{78} + \item \isa {someI_ex} (theorem), \bold{79} + \item sorts, 162 + \item \isa {spec} (theorem), \bold{72} \item \isa {split} (attribute), 32 - \item \isa {split} (constant), 146 - \item \isa {split} (method), 31, 146 + \item \isa {split} (constant), 148 + \item \isa {split} (method), 31, 148 \item \isa {split} (modifier), 32 \item split rule, \bold{32} \item \isa {split_if} (theorem), 32 \item \isa {split_if_asm} (theorem), 32 - \item \isa {ssubst} (theorem), \bold{67} + \item \isa {ssubst} (theorem), \bold{69} \item structural induction, \see{induction, structural}{1} - \item subclasses, 154, 158 + \item subclasses, 156, 161 \item subgoal numbering, 46 - \item \isa {subgoal_tac} (method), 88 + \item \isa {subgoal_tac} (method), 90 \item subgoals, 12 - \item subset relation, \bold{96} - \item \isa {subsetD} (theorem), \bold{96} - \item \isa {subsetI} (theorem), \bold{96} - \item \isa {subst} (method), 67 - \item substitution, 67--69 + \item subset relation, \bold{98} + \item \isa {subsetD} (theorem), \bold{98} + \item \isa {subsetI} (theorem), \bold{98} + \item \isa {subst} (method), 69 + \item substitution, 69--71 \item \isa {Suc} (constant), 22 - \item \isa {surj_def} (theorem), \bold{100} - \item surjections, 100 - \item \isa {sym} (theorem), \bold{84} + \item \isa {surj_def} (theorem), \bold{102} + \item surjections, 102 + \item \isa {sym} (theorem), \bold{86} \item syntax, 6, 11 - \item syntax translations, 26 + \item syntax translations, 55--56 \indexspace - \item tacticals, 89 + \item tacticals, 91 \item tactics, 12 \item \isacommand {term} (command), 16 \item term rewriting, \bold{27} \item termination, \see{functions, total}{1} \item terms, 5 - \item \isa {THE} (symbol), 75 - \item \isa {the_equality} (theorem), \bold{75} - \item \isa {THEN} (attribute), \bold{84}, 86, 92 + \item \isa {THE} (symbol), 77 + \item \isa {the_equality} (theorem), \bold{77} + \item \isa {THEN} (attribute), \bold{86}, 88, 94 \item \isacommand {theorem} (command), \bold{11}, 13 \item theories, 4 \subitem abandoning, \bold{16} @@ -565,12 +567,12 @@ \item \isa {ToyList} example, 9--14 \item \isa {trace_simp} (flag), 33 \item tracing the simplifier, \bold{33} - \item \isa {trancl_trans} (theorem), \bold{103} - \item transition systems, 107 - \item \isacommand {translations} (command), 26 + \item \isa {trancl_trans} (theorem), \bold{105} + \item transition systems, 109 + \item \isacommand {translations} (command), 55--56 \item tries, 44--46 \item \isa {True} (constant), 5 - \item \isa {truncate} (constant), 153 + \item \isa {truncate} (constant), 155 \item tuples, \see{pairs and tuples}{1} \item \isacommand {typ} (command), 16 \item type constraints, \bold{6} @@ -578,58 +580,60 @@ \item type inference, \bold{5} \item type synonyms, 25 \item type variables, 5 - \item \isacommand {typedecl} (command), 107, 161 - \item \isacommand {typedef} (command), 161--164 + \item \isacommand {typedecl} (command), 109, 163 + \item \isacommand {typedef} (command), 163--166 \item types, 4--5 - \subitem declaring, 161 - \subitem defining, 161--164 + \subitem declaring, 163 + \subitem defining, 163--166 \item \isacommand {types} (command), 25 \indexspace - \item Ullman, J. D., 135 - \item \texttt {UN}, \bold{199} - \item \texttt {Un}, \bold{199} - \item \isa {UN_E} (theorem), \bold{98} - \item \isa {UN_I} (theorem), \bold{98} - \item \isa {UN_iff} (theorem), \bold{98} - \item \isa {Un_subset_iff} (theorem), \bold{96} + \item Ullman, J. D., 137 + \item \texttt {UN}, \bold{201} + \item \texttt {Un}, \bold{201} + \item \isa {UN_E} (theorem), \bold{100} + \item \isa {UN_I} (theorem), \bold{100} + \item \isa {UN_iff} (theorem), \bold{100} + \item \isa {Un_subset_iff} (theorem), \bold{98} \item \isacommand {undo} (command), 16 \item \isa {unfold} (method), \bold{31} - \item unification, 66--69 - \item \isa {UNION} (constant), 99 - \item \texttt {Union}, \bold{199} + \item unification, 68--71 + \item \isa {UNION} (constant), 101 + \item \texttt {Union}, \bold{201} \item union - \subitem indexed, 98 - \item \isa {Union_iff} (theorem), \bold{98} + \subitem indexed, 100 + \item \isa {Union_iff} (theorem), \bold{100} \item \isa {unit} (type), 24 - \item unknowns, 7, \bold{58} - \item unsafe rules, \bold{80} - \item updating a function, \bold{99} + \item unknowns, 7, \bold{60} + \item unsafe rules, \bold{82} + \item update + \subitem record, 151 + \item updating a function, \bold{101} \indexspace \item variables, 7 \subitem schematic, 7 \subitem type, 5 - \item \isa {vimage_def} (theorem), \bold{101} + \item \isa {vimage_def} (theorem), \bold{103} \indexspace \item Wenzel, Markus, vii - \item \isa {wf_induct} (theorem), \bold{105} - \item \isa {wf_inv_image} (theorem), \bold{105} - \item \isa {wf_less_than} (theorem), \bold{104} - \item \isa {wf_lex_prod} (theorem), \bold{105} - \item \isa {wf_measure} (theorem), \bold{105} - \item \isa {wf_subset} (theorem), 170 - \item \isa {while} (constant), 175 - \item \isa {While_Combinator} (theory), 175 - \item \isa {while_rule} (theorem), 175 + \item \isa {wf_induct} (theorem), \bold{107} + \item \isa {wf_inv_image} (theorem), \bold{107} + \item \isa {wf_less_than} (theorem), \bold{106} + \item \isa {wf_lex_prod} (theorem), \bold{107} + \item \isa {wf_measure} (theorem), \bold{107} + \item \isa {wf_subset} (theorem), 172 + \item \isa {while} (constant), 177 + \item \isa {While_Combinator} (theory), 177 + \item \isa {while_rule} (theorem), 177 \indexspace - \item \isa {zadd_ac} (theorems), 143 - \item \isa {zmult_ac} (theorems), 143 + \item \isa {zadd_ac} (theorems), 145 + \item \isa {zmult_ac} (theorems), 145 \end{theindex}