src/HOL/ex/Records.thy
changeset 14700 2f885b7e5ba7
parent 12591 5a46569d2b05
child 15010 72fbe711e414
equal deleted inserted replaced
14699:2c9b463044ec 14700:2f885b7e5ba7
     1 (*  Title:      HOL/ex/Records.thy
     1 (*  Title:      HOL/ex/Records.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     3     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
       
     4                 TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 *)
     6 
     7 
     7 header {* Using extensible records in HOL -- points and coloured points *}
     8 header {* Using extensible records in HOL -- points and coloured points *}
     8 
     9 
    17 text {*
    18 text {*
    18   Apart many other things, above record declaration produces the
    19   Apart many other things, above record declaration produces the
    19   following theorems:
    20   following theorems:
    20 *}
    21 *}
    21 
    22 
       
    23 
    22 thm "point.simps"
    24 thm "point.simps"
    23 thm "point.iffs"
    25 thm "point.iffs"
    24 thm "point.defs"
    26 thm "point.defs"
    25 
    27 
    26 text {*
    28 text {*
    27   The set of theorems @{thm [source] point.simps} is added
    29   The set of theorems @{thm [source] point.simps} is added
    28   automatically to the standard simpset, @{thm [source] point.iffs} is
    30   automatically to the standard simpset, @{thm [source] point.iffs} is
    29   added to the Classical Reasoner and Simplifier context.
    31   added to the Classical Reasoner and Simplifier context.
    30 
    32 
    31   \medskip Record declarations define new type abbreviations:
    33   \medskip Record declarations define new types and type abbreviations:
    32   @{text [display]
    34   @{text [display]
    33 "    point = (| xpos :: nat, ypos :: nat |)
    35 "  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
    34     'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"}
    36   'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
    35 *}
    37 *}
    36 
    38 
    37 consts foo1 :: point
    39 consts foo1 :: point
    38 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
    40 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
    39 consts foo3 :: "'a => 'a point_scheme"
    41 consts foo3 :: "'a => 'a point_scheme"
   105 text {*
   107 text {*
   106   \medskip Representation of records by cases or (degenerate)
   108   \medskip Representation of records by cases or (degenerate)
   107   induction.
   109   induction.
   108 *}
   110 *}
   109 
   111 
   110 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   112 lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   111 proof (cases r)
   113 proof (cases r)
   112   fix xpos ypos more
   114   fix xpos ypos more
   113   assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
   115   assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
   114   thus ?thesis by simp
   116   thus ?thesis by simp
   115 qed
   117 qed
   172 record cpoint = point +
   174 record cpoint = point +
   173   colour :: colour
   175   colour :: colour
   174 
   176 
   175 
   177 
   176 text {*
   178 text {*
   177   The record declaration defines new type constructors:
   179   The record declaration defines a new type constructure and abbreviations:
   178   @{text [display]
   180   @{text [display]
   179 "    cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |)
   181 "  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
   180     'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"}
   182      () cpoint_ext_type point_ext_type
       
   183    'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
       
   184      'a cpoint_ext_type point_ext_type"}
   181 *}
   185 *}
   182 
   186 
   183 consts foo6 :: cpoint
   187 consts foo6 :: cpoint
   184 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
   188 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
   185 consts foo8 :: "'a cpoint_scheme"
   189 consts foo8 :: "'a cpoint_scheme"