# HG changeset patch # User wenzelm # Date 1008964722 -3600 # Node ID 6bf380202adb1eaffc5f62024afc17c5d36f5268 # Parent e3cb192aa6ee9055896d916c44a5032f7286021e tuned; diff -r e3cb192aa6ee -r 6bf380202adb doc-src/TutorialI/Types/Records.thy --- a/doc-src/TutorialI/Types/Records.thy Fri Dec 21 20:58:25 2001 +0100 +++ b/doc-src/TutorialI/Types/Records.thy Fri Dec 21 20:58:42 2001 +0100 @@ -12,7 +12,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 @@ -23,21 +23,20 @@ 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. *} subsection {* Record Basics *} text {* - 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. *} record point = @@ -67,21 +66,21 @@ "pt2 \ \Xcoord = -45, Ycoord = 97\" text {* - For each field, there is a \emph{selector} function of the same - name. For example, if @{text p} has type @{typ point} then @{text - "Xcoord p"} denotes the value of the @{text Xcoord} field of~@{text - 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 @{text p} has type @{typ + point} then @{text "Xcoord p"} denotes the value of the @{text + Xcoord} field of~@{text p}. Expressions involving field selection + of explicit records are simplified automatically: *} lemma "Xcoord \Xcoord = a, Ycoord = b\ = a" by simp text {* - The \emph{update} operation is functional. For example, @{term - "p\Xcoord := 0\"} is a record whose @{text Xcoord} value is zero - and whose @{text Ycoord} value is copied from~@{text p}. Updates - are also simplified automatically: + The \emph{update}\index{update!record} operation is functional. For + example, @{term "p\Xcoord := 0\"} is a record whose @{text Xcoord} + value is zero and whose @{text Ycoord} value is copied from~@{text + p}. Updates are also simplified automatically: *} lemma "\Xcoord = a, Ycoord = b\\Xcoord := 0\ = @@ -92,8 +91,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 @{typ point} simply @{text x} and~@{text y}. Each record - declaration introduces a constant \cdx{more}. + type @{typ point} simply @{text x} and~@{text y}. \end{warn} *} @@ -139,12 +137,14 @@ text {* This lemma applies to any record whose first two fields are @{text - Xcoord} and~@{text Ycoord}. Note that @{text "\Xcoord = a, Ycoord - = b, \ = ()\"} is actually the same as @{text "\Xcoord = a, - Ycoord = b\"}. + Xcoord} and~@{text Ycoord}. Note that @{text "\Xcoord = a, Ycoord = + b, \ = ()\"} is really the same as @{text "\Xcoord = a, Ycoord = + b\"}. Selectors and updates are always polymorphic wrt.\ the @{text + more} part of a record scheme, its value is just ignored (for + select) or copied (for update). - The pseudo-field @{text more} can be selected in the usual way, but - the identifier must be qualified: + The @{text more} pseudo-field may be manipulated directly as well, + but the identifier needs to be qualified: *} lemma "point.more cpt1 = \col = Green\" @@ -153,28 +153,30 @@ text {* We see that the colour attached to this @{typ point} is a (rudimentary) record in its own right, namely @{text "\col = - Green\"}. In order to select or update @{text col} in the above - fragment, @{text "\col = Green\"} needs to be put back into the - context of its parent type scheme, say as @{text more} part of a - @{typ point}. + Green\"}. In order to select or update @{text col}, this fragment + needs to be put back into the context of the parent type scheme, say + as @{text more} part of another @{typ point}. To define generic operations, we need to know a bit more about - records. Our declaration of @{typ point} above generated two type + records. Our definition of @{typ point} above generated two type abbreviations: - \smallskip + \medskip \begin{tabular}{l} @{typ point}~@{text "="}~@{typ "\Xcoord :: int, Ycoord :: int\"} \\ @{typ "'a point_scheme"}~@{text "="}~@{typ "\Xcoord :: int, Ycoord :: int, \ :: 'a\"} \\ \end{tabular} - \smallskip + \medskip - Type @{typ point} is for rigid records having exactly the two fields + Type @{typ point} is for fixed records having exactly the two fields @{text Xcoord} and~@{text Ycoord}, while the polymorphic type @{typ "'a point_scheme"} comprises all possible extensions to those two - fields, recall that @{typ "unit point_scheme"} coincides with @{typ - point}. For example, let us define two operations --- methods, if - we regard records as objects --- to get and set any point's @{text + fields. Note that @{typ "unit point_scheme"} coincides with @{typ + point}, and @{typ "\col :: colour\ point_scheme"} with @{typ + cpoint}. + + In the following example we define two operations --- methods, if we + regard records as objects --- to get and set any point's @{text Xcoord} field. *} @@ -188,7 +190,7 @@ Here is a generic method that modifies a point, incrementing its @{text Xcoord} field. The @{text Ycoord} and @{text more} fields are copied across. It works for any record type scheme derived from - @{typ point}, such as @{typ cpoint}: + @{typ point} (including @{typ cpoint} etc.): *} constdefs @@ -229,7 +231,7 @@ text {* The following equality is similar, but generic, in that @{text r} - can be any instance of @{text point_scheme}: + can be any instance of @{typ "'a point_scheme"}: *} lemma "r\Xcoord := a, Ycoord := b\ = r\Ycoord := b, Xcoord := a\" @@ -237,29 +239,26 @@ text {* We see above the syntax for iterated updates. We could equivalently - have written the left-hand side as @{term "r\Xcoord := a\\Ycoord - := b\"}. + have written the left-hand side as @{text "r\Xcoord := a\\Ycoord := + b\"}. - 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. *} lemma "r = \Xcoord = Xcoord r, Ycoord = Ycoord r\" by simp text {* - The generic version of this equality includes the field @{text - more}: + The generic version of this equality includes the pseudo-field + @{text more}: *} lemma "r = \Xcoord = Xcoord r, Ycoord = Ycoord r, \ = point.more r\" by simp text {* - Note that the @{text r} is of a different (more general) type than - the previous one. - \medskip The simplifier can prove many record equalities automatically, but general equality reasoning can be tricky. Consider proving this obvious fact: @@ -270,8 +269,8 @@ oops text {* - 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 @{text Xcoord} to both sides of the assumed record equality: *} @@ -285,42 +284,54 @@ done text {* - The @{text cases} method is preferable to such a forward proof. - State the desired lemma again: + The @{text cases} method is preferable to such a forward proof. We + state the desired lemma again: *} lemma "r\Xcoord := a\ = r\Xcoord := a'\ \ a = a'" - txt {* - 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 @{text more}, since the record - equality stated above is generic. *} + + txt {* 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 @{text more}, since the + record equality stated here is generic for all extensions. *} + apply (cases r) - txt {* @{subgoals [display, indent = 0, margin = 65]} - Again, @{text simp} finishes the proof. Because @{text 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). *} + txt {* @{subgoals [display, indent = 0, margin = 65]} Again, @{text + simp} finishes the proof. Because @{text 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). *} + apply simp done +text {* + 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 @{text rule_tac} used together with the + internal representation rules of records. E.g.\ the above use of + @{text "(cases r)"} would become @{text "(rule_tac r = r in + point.cases_scheme)"}. +*} + subsection {* Extending and Truncating Records *} text {* - 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 @{typ point} and @{typ - cpoint}. We can add a colour to a point or to convert a @{typ - cpoint} to a @{typ 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 @{typ + point} and @{typ cpoint}. We can add a colour to a point or convert + a @{typ cpoint} to a @{typ 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 @{text more} part of the parent record scheme. @@ -336,26 +347,27 @@ 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 @{text defs} (e.g.\ @{text - point.defs} or @{text cpoint.defs}). + available by the collective name of @{text defs} (@{text + point.defs}, @{text cpoint.defs}, etc.). For example, here are the versions of those functions generated for record @{typ point}. We omit @{text point.fields}, which happens to be the same as @{text point.make}. - @{thm [display, indent = 0, margin = 65] point.make_def - point.extend_def point.truncate_def} + @{thm [display, indent = 0, margin = 65] point.make_def [no_vars] + point.extend_def [no_vars] point.truncate_def [no_vars]} Contrast those with the corresponding functions for record @{typ cpoint}. Observe @{text cpoint.fields} in particular. - @{thm [display, indent = 0, margin = 65] cpoint.make_def - cpoint.extend_def cpoint.truncate_def} + @{thm [display, indent = 0, margin = 65] cpoint.make_def [no_vars] + cpoint.fields_def [no_vars] cpoint.extend_def [no_vars] + cpoint.truncate_def [no_vars]} To demonstrate these functions, we declare a new coloured point by extending an ordinary point. Function @{text point.extend} augments - @{text pt1} with a colour, which is converted into an appropriate - record fragment by @{text cpoint.fields}. + @{text pt1} with a colour value, which is converted into an + appropriate record fragment by @{text cpoint.fields}. *} constdefs @@ -377,8 +389,7 @@ text {* In the example below, a coloured point is truncated to leave a - point. We must use the @{text truncate} function of the shorter - record. + point. We use the @{text truncate} function of the target record. *} lemma "point.truncate cpt2 = pt1" @@ -387,8 +398,10 @@ text {* \begin{exercise} Extend record @{typ cpoint} to have a further field, @{text - intensity}, of type~@{typ nat}. Experiment with coercions among the - three record types. + intensity}, of type~@{typ nat}. Experiment with generic operations + (using polymorphic selectors and updates) and explicit coercions + (using @{text extend}, @{text truncate} etc.) among the three record + types. \end{exercise} \begin{exercise}