src/HOL/ex/Records.thy
author wenzelm
Sat May 27 17:42:02 2006 +0200 (2006-05-27)
changeset 19736 d8d0f8f51d69
parent 16417 9bc16273c2d4
child 21404 eb85850d3eb7
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/ex/Records.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
     4                 TU Muenchen
     5 *)
     6 
     7 header {* Using extensible records in HOL -- points and coloured points *}
     8 
     9 theory Records imports Main begin
    10 
    11 subsection {* Points *}
    12 
    13 record point =
    14   xpos :: nat
    15   ypos :: nat
    16 
    17 text {*
    18   Apart many other things, above record declaration produces the
    19   following theorems:
    20 *}
    21 
    22 
    23 thm "point.simps"
    24 thm "point.iffs"
    25 thm "point.defs"
    26 
    27 text {*
    28   The set of theorems @{thm [source] point.simps} is added
    29   automatically to the standard simpset, @{thm [source] point.iffs} is
    30   added to the Classical Reasoner and Simplifier context.
    31 
    32   \medskip Record declarations define new types and type abbreviations:
    33   @{text [display]
    34 "  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
    35   'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
    36 *}
    37 
    38 consts foo1 :: point
    39 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
    40 consts foo3 :: "'a => 'a point_scheme"
    41 consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
    42 
    43 
    44 subsubsection {* Introducing concrete records and record schemes *}
    45 
    46 defs
    47   foo1_def: "foo1 == (| xpos = 1, ypos = 0 |)"
    48   foo3_def: "foo3 ext == (| xpos = 1, ypos = 0, ... = ext |)"
    49 
    50 
    51 subsubsection {* Record selection and record update *}
    52 
    53 definition
    54   getX :: "'a point_scheme => nat"
    55   "getX r = xpos r"
    56   setX :: "'a point_scheme => nat => 'a point_scheme"
    57   "setX r n = r (| xpos := n |)"
    58 
    59 
    60 subsubsection {* Some lemmas about records *}
    61 
    62 text {* Basic simplifications. *}
    63 
    64 lemma "point.make n p = (| xpos = n, ypos = p |)"
    65   by (simp only: point.make_def)
    66 
    67 lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
    68   by simp
    69 
    70 lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
    71   by simp
    72 
    73 
    74 text {* \medskip Equality of records. *}
    75 
    76 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
    77   -- "introduction of concrete record equality"
    78   by simp
    79 
    80 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
    81   -- "elimination of concrete record equality"
    82   by simp
    83 
    84 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    85   -- "introduction of abstract record equality"
    86   by simp
    87 
    88 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
    89   -- "elimination of abstract record equality (manual proof)"
    90 proof -
    91   assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
    92   hence "xpos ?lhs = xpos ?rhs" by simp
    93   thus ?thesis by simp
    94 qed
    95 
    96 
    97 text {* \medskip Surjective pairing *}
    98 
    99 lemma "r = (| xpos = xpos r, ypos = ypos r |)"
   100   by simp
   101 
   102 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
   103   by simp
   104 
   105 
   106 text {*
   107   \medskip Representation of records by cases or (degenerate)
   108   induction.
   109 *}
   110 
   111 lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   112 proof (cases r)
   113   fix xpos ypos more
   114   assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
   115   thus ?thesis by simp
   116 qed
   117 
   118 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   119 proof (induct r)
   120   fix xpos ypos more
   121   show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
   122       (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
   123     by simp
   124 qed
   125 
   126 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   127 proof (cases r)
   128   fix xpos ypos more
   129   assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
   130   thus ?thesis by simp
   131 qed
   132 
   133 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   134 proof (cases r)
   135   case fields
   136   thus ?thesis by simp
   137 qed
   138 
   139 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   140   by (cases r) simp
   141 
   142 
   143 text {*
   144  \medskip Concrete records are type instances of record schemes.
   145 *}
   146 
   147 definition
   148   foo5 :: nat
   149   "foo5 = getX (| xpos = 1, ypos = 0 |)"
   150 
   151 
   152 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
   153 
   154 definition
   155   incX :: "'a point_scheme => 'a point_scheme"
   156   "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
   157 
   158 lemma "incX r = setX r (Suc (getX r))"
   159   by (simp add: getX_def setX_def incX_def)
   160 
   161 
   162 text {* An alternative definition. *}
   163 
   164 definition
   165   incX' :: "'a point_scheme => 'a point_scheme"
   166   "incX' r = r (| xpos := xpos r + 1 |)"
   167 
   168 
   169 subsection {* Coloured points: record extension *}
   170 
   171 datatype colour = Red | Green | Blue
   172 
   173 record cpoint = point +
   174   colour :: colour
   175 
   176 
   177 text {*
   178   The record declaration defines a new type constructure and abbreviations:
   179   @{text [display]
   180 "  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
   181      () cpoint_ext_type point_ext_type
   182    'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
   183      'a cpoint_ext_type point_ext_type"}
   184 *}
   185 
   186 consts foo6 :: cpoint
   187 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
   188 consts foo8 :: "'a cpoint_scheme"
   189 consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
   190 
   191 
   192 text {*
   193  Functions on @{text point} schemes work for @{text cpoints} as well.
   194 *}
   195 
   196 definition
   197   foo10 :: nat
   198   "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
   199 
   200 
   201 subsubsection {* Non-coercive structural subtyping *}
   202 
   203 text {*
   204  Term @{term foo11} has type @{typ cpoint}, not type @{typ point} ---
   205  Great!
   206 *}
   207 
   208 definition
   209   foo11 :: cpoint
   210   "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
   211 
   212 
   213 subsection {* Other features *}
   214 
   215 text {* Field names contribute to record identity. *}
   216 
   217 record point' =
   218   xpos' :: nat
   219   ypos' :: nat
   220 
   221 text {*
   222   \noindent May not apply @{term getX} to @{term [source] "(| xpos' =
   223   2, ypos' = 0 |)"} -- type error.
   224 *}
   225 
   226 text {* \medskip Polymorphic records. *}
   227 
   228 record 'a point'' = point +
   229   content :: 'a
   230 
   231 types cpoint'' = "colour point''"
   232 
   233 end