src/HOL/Record.thy
author wenzelm
Tue Jul 28 17:05:34 1998 +0200 (1998-07-28)
changeset 5210 54aaa779b6b4
parent 5198 b1adae4f8b90
child 5694 39af7b3dd1c4
permissions -rw-r--r--
removed global_names flag;
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.  See
     6 Tools/record_package.ML for the actual implementation.
     7 *)
     8 
     9 Record = Prod +
    10 
    11 
    12 (* concrete syntax *)
    13 
    14 nonterminals
    15   ident field_type field_types field fields update updates
    16 
    17 syntax
    18   (*field names*)
    19   ""                	:: "id => ident"                    		("_")
    20   ""                	:: "longid => ident"                		("_")
    21 
    22   (*record types*)
    23   "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
    24   ""               	:: "field_type => field_types"              	("_")
    25   "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
    26   "_record_type"	:: "field_types => type"                   	("('(| _ |'))")
    27   "_record_type_scheme"	:: "[field_types, type] => type"	("('(| _,/ (2... ::/ _) |'))")
    28 
    29   (*records*)
    30   "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
    31   ""                	:: "field => fields"                		("_")
    32   "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
    33   "_record"         	:: "fields => 'a"                   		("('(| _ |'))")
    34   "_record_scheme"  	:: "[fields, 'a] => 'a"             	("('(| _,/ (2... =/ _) |'))")
    35 
    36   (*record updates*)
    37   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    38   ""                	:: "update => updates"               		("_")
    39   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    40   "_record_update"  	:: "['a, updates] => 'b"               	("_/('(| _ |'))" [900,0] 900)
    41 
    42 
    43 (* type class for record extensions *)
    44 
    45 axclass more < term
    46 
    47 instance unit :: more
    48 instance "*" :: (term, more) more
    49 
    50 
    51 (* initialize the package *)
    52 
    53 setup
    54   RecordPackage.setup
    55 
    56 
    57 end