src/HOL/ex/Records.thy
 changeset 10357 0d0cac129618 parent 10052 5fa8d8d5c852 child 11701 3d51fbf81c17
equal inserted replaced
10356:bf881f5fd82f 10357:0d0cac129618
    22 thm "point.simps"
    22 thm "point.simps"
    23 thm "point.iffs"
    23 thm "point.iffs"
    24 thm "point.update_defs"
    24 thm "point.update_defs"
    25
    25
    26 text {*
    26 text {*
    27  The set of theorems "point.simps" is added automatically to the
    27  The set of theorems @{thm [source] point.simps} is added
    28  standard simpset, "point.iffs" is added to the claset and simpset.
    28  automatically to the standard simpset, @{thm [source] point.iffs} is

    29  added to the Classical Reasoner and Simplifier context.
    29 *}
    30 *}
    30
    31
    31 text {*
    32 text {*
    32   Record declarations define new type abbreviations:
    33   Record declarations define new type abbreviations:
    33
    34   @{text [display]
    34     point = "(| x :: nat, y :: nat |)"
    35 "    point = (| x :: nat, y :: nat |)
    35     'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
    36     'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)"}
    36
    37   Extensions ...' must be in type class @{text more}.
    37   Extensions ...' must be in type class more'!
       
    38 *}
    38 *}
    39 
    39 
    40 consts foo1 :: point
    40 consts foo1 :: point
    41 consts foo2 :: "(| x :: nat, y :: nat |)"
    41 consts foo2 :: "(| x :: nat, y :: nat |)"
    42 consts foo3 :: "'a => ('a::more) point_scheme"
    42 consts foo3 :: "'a => ('a::more) point_scheme"
    59   "setX r n == r (| x := n |)"
    59   "setX r n == r (| x := n |)"
    60 
    60 
    61 
    61 
    62 subsubsection {* Some lemmas about records *}
    62 subsubsection {* Some lemmas about records *}
    63 
    63 
    64 text {* Basic simplifications *}
    64 text {* Basic simplifications. *}
    65 
    65 
    66 lemma "point.make n p = (| x = n, y = p |)"
    66 lemma "point.make n p = (| x = n, y = p |)"
    67   by simp
    67   by simp
    68 
    68 
    69 lemma "x (| x = m, y = n, ... = p |) = m"
    69 lemma "x (| x = m, y = n, ... = p |) = m"
    71 
    71 
    72 lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
    72 lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
    73   by simp
    73   by simp
    74 
    74 
    75 
    75 
    76 text {* Equality of records *}
    76 text {* \medskip Equality of records. *}
    77 
    77 
    78 lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)"
    78 lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)"
    79   -- "introduction of concrete record equality"
    79   -- "introduction of concrete record equality"
    80   by simp
    80   by simp
    81 
    81 
    94   hence "x ?lhs = x ?rhs" by simp
    94   hence "x ?lhs = x ?rhs" by simp
    95   thus ?thesis by simp
    95   thus ?thesis by simp
    96 qed
    96 qed
    97 
    97 
    98 
    98 
    99 text {* Surjective pairing *}
    99 text {* \medskip Surjective pairing *}
   100 
   100 
   101 lemma "r = (| x = x r, y = y r |)"
   101 lemma "r = (| x = x r, y = y r |)"
   102   by simp
   102   by simp
   103 
   103 
   104 lemma "r = (| x = x r, y = y r, ... = more r |)"
   104 lemma "r = (| x = x r, y = y r, ... = more r |)"
   105   by simp
   105   by simp
   106 
   106 
   107 
   107 
   108 text {* Splitting quantifiers: the !!r is NECESSARY here *}
   108 text {*
       
   109  \medskip Splitting quantifiers: the @{text "!!r"} is \emph{necessary}
       
   110  here!
       
   111 *}
   109 
   112 
   110 lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
   113 lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
   111 proof record_split
   114 proof record_split
   112   fix x y more
   115   fix x y more
   113   show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
   116   show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
   122         (| x = x, y = y, ... = more |)(| x := m |)"
   125         (| x = x, y = y, ... = more |)(| x := m |)"
   123     by simp
   126     by simp
   124 qed
   127 qed
   125 
   128 
   126 
   129 
   127 
   130 text {*
   128 text {* Concrete records are type instances of record schemes *}
   131  \medskip Concrete records are type instances of record schemes.
       
   132 *}
   129 
   133 
   130 constdefs
   134 constdefs
   131   foo5 :: nat
   135   foo5 :: nat
   132   "foo5 == getX (| x = 1, y = 0 |)"
   136   "foo5 == getX (| x = 1, y = 0 |)"
   133 
   137 
   134 
   138 
   135 text {* Manipulating the ...' (more) part *}
   139 text {* \medskip Manipulating the ...' (more) part. *}
   136 
   140 
   137 constdefs
   141 constdefs
   138   incX :: "('a::more) point_scheme => 'a point_scheme"
   142   incX :: "('a::more) point_scheme => 'a point_scheme"
   139   "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
   143   "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
   140 
   144 
   142 proof (unfold getX_def setX_def incX_def)
   146 proof (unfold getX_def setX_def incX_def)
   143   show "!!r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)"
   147   show "!!r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)"
   144     by record_split simp
   148     by record_split simp
   145 qed
   149 qed
   146 
   150 
   147 
   151 text {* An alternative definition. *}
   148 text {* alternative definition *}
       
   149 
   152 
   150 constdefs
   153 constdefs
   151   incX' :: "('a::more) point_scheme => 'a point_scheme"
   154   incX' :: "('a::more) point_scheme => 'a point_scheme"
   152   "incX' r == r (| x := Suc (x r) |)"
   155   "incX' r == r (| x := Suc (x r) |)"
   153 
   156 
   160   colour :: colour
   163   colour :: colour
   161 
   164 
   162 
   165 
   163 text {*
   166 text {*
   164   The record declaration defines new type constructors:
   167   The record declaration defines new type constructors:
   165 
   168   @{text [display]
   166     cpoint = (| x :: nat, y :: nat, colour :: colour |)
   169 "    cpoint = (| x :: nat, y :: nat, colour :: colour |)
   167     'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
   170     'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"}
   168 *}
   171 *}
   169 
   172 
   170 consts foo6 :: cpoint
   173 consts foo6 :: cpoint
   171 consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
   174 consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
   172 consts foo8 :: "('a::more) cpoint_scheme"
   175 consts foo8 :: "('a::more) cpoint_scheme"
   173 consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
   176 consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
   174 
   177 
   175 
   178 
   176 text {* Functions on point schemes work for cpoints as well *}
   179 text {*
       
   180  Functions on @{text point} schemes work for @{text cpoints} as well.
       
   181 *}
   177 
   182 
   178 constdefs
   183 constdefs
   179   foo10 :: nat
   184   foo10 :: nat
   180   "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   185   "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   181 
   186 
   182 
   187 
   183 subsubsection {* Non-coercive structural subtyping *}
   188 subsubsection {* Non-coercive structural subtyping *}
   184 
   189 
   185 text {* foo11 has type cpoint, not type point --- Great! *}
   190 text {*
       
   191  Term @{term foo11} has type @{typ cpoint}, not type @{typ point} ---
       
   192  Great!
       
   193 *}
   186 
   194 
   187 constdefs
   195 constdefs
   188   foo11 :: cpoint
   196   foo11 :: cpoint
   189   "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   197   "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   190 
   198 
   191 
   199 
   192 subsection {* Other features *}
   200 subsection {* Other features *}
   193 
   201 
   194 text {* field names contribute to record identity *}
   202 text {* Field names contribute to record identity. *}
   195 
   203 
   196 record point' =
   204 record point' =
   197   x' :: nat
   205   x' :: nat
   198   y' :: nat
   206   y' :: nat
   199 
   207 
   200 text {* May not apply @{term getX} to @{term "(| x' = 2, y' = 0 |)"} *}
   208 text {*
   201 
   209  \noindent May not apply @{term getX} to 
   202 
   210  @{term [source] "(| x' = 2, y' = 0 |)"}.
   203 text {* Polymorphic records *}
   211 *}
       
   212 
       
   213 text {* \medskip Polymorphic records. *}
   204 
   214 
   205 record 'a point'' = point +
   215 record 'a point'' = point +
   206   content :: 'a
   216   content :: 'a
   207 
   217 
   208 types cpoint'' = "colour point''"
   218 types cpoint'' = "colour point''"`