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