wenzelm@4870: (*  Title:      HOL/Record.thy
wenzelm@4870:     ID:         $Id$
wenzelm@4870:     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
wenzelm@4870: 
wenzelm@4870: Extensible records with structural subtyping in HOL.  See
wenzelm@4870: Tools/record_package.ML for the actual implementation.
wenzelm@4870: *)
wenzelm@4870: 
wenzelm@7357: theory Record = Datatype
wenzelm@7357: files "Tools/record_package.ML":
wenzelm@4870: 
wenzelm@4870: 
wenzelm@4870: (* concrete syntax *)
wenzelm@4870: 
wenzelm@4870: nonterminals
wenzelm@5198:   ident field_type field_types field fields update updates
wenzelm@4870: 
wenzelm@4870: syntax
wenzelm@5198:   (*field names*)
wenzelm@10093:   ""                    :: "id => ident"                                ("_")
wenzelm@10093:   ""                    :: "longid => ident"                            ("_")
wenzelm@5198: 
wenzelm@5198:   (*record types*)
wenzelm@10093:   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
wenzelm@10093:   ""                    :: "field_type => field_types"                  ("_")
wenzelm@10093:   "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")
wenzelm@10093:   "_record_type"        :: "field_types => type"                        ("(3'(| _ |'))")
wenzelm@10093:   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198: 
wenzelm@5198:   (*records*)
wenzelm@10093:   "_field"              :: "[ident, 'a] => field"                       ("(2_ =/ _)")
wenzelm@10093:   ""                    :: "field => fields"                            ("_")
wenzelm@10093:   "_fields"             :: "[field, fields] => fields"                  ("_,/ _")
wenzelm@10093:   "_record"             :: "fields => 'a"                               ("(3'(| _ |'))")
wenzelm@10093:   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198: 
wenzelm@5198:   (*record updates*)
wenzelm@10093:   "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
wenzelm@10093:   ""                    :: "update => updates"                          ("_")
wenzelm@10093:   "_updates"            :: "[update, updates] => updates"               ("_,/ _")
wenzelm@10093:   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870: 
wenzelm@10093: syntax (input)   (* FIXME (xsymbols) *)
wenzelm@10093:   "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
wenzelm@10093:   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093:   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093:   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093:   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729: 
wenzelm@4870: 
wenzelm@4870: (* type class for record extensions *)
wenzelm@4870: 
wenzelm@7357: axclass more < "term"
wenzelm@10309: instance unit :: more ..
wenzelm@4870: 
wenzelm@4870: 
wenzelm@4870: (* initialize the package *)
wenzelm@4870: 
wenzelm@4870: setup
wenzelm@4870:   RecordPackage.setup
wenzelm@4870: 
wenzelm@4870: 
wenzelm@4870: end