src/HOL/Record.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10331 7411e4659d4a
child 10641 d1533f63c738
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Record.thy
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     3
    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     4
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     5
Extensible records with structural subtyping in HOL.  See
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     6
Tools/record_package.ML for the actual implementation.
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     7
*)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     8
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 5732
diff changeset
     9
theory Record = Datatype
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 5732
diff changeset
    10
files "Tools/record_package.ML":
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    11
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    12
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    13
(* concrete syntax *)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    14
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    15
nonterminals
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    16
  ident field_type field_types field fields update updates
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    17
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    18
syntax
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    19
  (*field names*)
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    20
  ""                    :: "id => ident"                                ("_")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    21
  ""                    :: "longid => ident"                            ("_")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    22
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    23
  (*record types*)
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    24
  "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    25
  ""                    :: "field_type => field_types"                  ("_")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    26
  "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    27
  "_record_type"        :: "field_types => type"                        ("(3'(| _ |'))")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    28
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    29
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    30
  (*records*)
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    31
  "_field"              :: "[ident, 'a] => field"                       ("(2_ =/ _)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    32
  ""                    :: "field => fields"                            ("_")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    33
  "_fields"             :: "[field, fields] => fields"                  ("_,/ _")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    34
  "_record"             :: "fields => 'a"                               ("(3'(| _ |'))")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    35
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    36
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    37
  (*record updates*)
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    38
  "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    39
  ""                    :: "update => updates"                          ("_")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    40
  "_updates"            :: "[update, updates] => updates"               ("_,/ _")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    41
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    42
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10309
diff changeset
    43
syntax (xsymbols)
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    44
  "_record_type"        :: "field_types => type"                        ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    45
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    46
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    47
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    48
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729
40cfc3dd27da \<dots> syntax;
wenzelm
parents: 7357
diff changeset
    49
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    50
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    51
(* type class for record extensions *)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    52
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 5732
diff changeset
    53
axclass more < "term"
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10093
diff changeset
    54
instance unit :: more ..
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    55
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    56
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    57
(* initialize the package *)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    58
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    59
setup
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    60
  RecordPackage.setup
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    61
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    62
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    63
end