src/HOL/ex/Records.thy

 (*  Title:      HOL/ex/Records.thy
     ID:         $Id$
-    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
+    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
+                TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Using extensible records in HOL -- points and coloured points *}
 

 text {*
   Apart many other things, above record declaration produces the
   following theorems:
 *}
 
+
 thm "point.simps"
 thm "point.iffs"
 thm "point.defs"
 
 text {*
   The set of theorems @{thm [source] point.simps} is added
   automatically to the standard simpset, @{thm [source] point.iffs} is
   added to the Classical Reasoner and Simplifier context.
 
-  \medskip Record declarations define new type abbreviations:
+  \medskip Record declarations define new types and type abbreviations:
   @{text [display]
-"    point = (| xpos :: nat, ypos :: nat |)
-    'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"}
+"  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
+  'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
 *}
 
 consts foo1 :: point
 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
 consts foo3 :: "'a => 'a point_scheme"

 text {*
   \medskip Representation of records by cases or (degenerate)
   induction.
 *}
 
-lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
+lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
 proof (cases r)
   fix xpos ypos more
   assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
   thus ?thesis by simp
 qed

 record cpoint = point +
   colour :: colour
 
 
 text {*
-  The record declaration defines new type constructors:
+  The record declaration defines a new type constructure and abbreviations:
   @{text [display]
-"    cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |)
-    'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"}
+"  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
+     () cpoint_ext_type point_ext_type
+   'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
+     'a cpoint_ext_type point_ext_type"}
 *}
 
 consts foo6 :: cpoint
 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
 consts foo8 :: "'a cpoint_scheme"