src/HOL/Record.thy
author wenzelm
Wed Aug 25 20:49:02 1999 +0200 (1999-08-25)
changeset 7357 d0e16da40ea2
parent 5732 8712391bbf3d
child 9729 40cfc3dd27da
permissions -rw-r--r--
proper bootstrap of HOL theory and packages;
     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 theory Record = Datatype
    10 files "Tools/record_package.ML":
    11 
    12 
    13 (* concrete syntax *)
    14 
    15 nonterminals
    16   ident field_type field_types field fields update updates
    17 
    18 syntax
    19   (*field names*)
    20   ""                	:: "id => ident"                    		("_")
    21   ""                	:: "longid => ident"                		("_")
    22 
    23   (*record types*)
    24   "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
    25   ""               	:: "field_type => field_types"              	("_")
    26   "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
    27   "_record_type"	:: "field_types => type"                   	("(3'(| _ |'))")
    28   "_record_type_scheme"	:: "[field_types, type] => type"	("(3'(| _,/ (2... ::/ _) |'))")
    29 
    30   (*records*)
    31   "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
    32   ""                	:: "field => fields"                		("_")
    33   "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
    34   "_record"         	:: "fields => 'a"                   		("(3'(| _ |'))")
    35   "_record_scheme"  	:: "[fields, 'a] => 'a"             	("(3'(| _,/ (2... =/ _) |'))")
    36 
    37   (*record updates*)
    38   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
    39   ""                	:: "update => updates"               		("_")
    40   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
    41   "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
    42 
    43 
    44 (* type class for record extensions *)
    45 
    46 axclass more < "term"
    47 instance unit :: more
    48   by intro_classes
    49 
    50 
    51 (* initialize the package *)
    52 
    53 setup
    54   RecordPackage.setup
    55 
    56 
    57 end