src/HOL/Record.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 7357 d0e16da40ea2
child 9729 40cfc3dd27da
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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*)
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    20
  ""                	:: "id => ident"                    		("_")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    21
  ""                	:: "longid => ident"                		("_")
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*)
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    24
  "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    25
  ""               	:: "field_type => field_types"              	("_")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    26
  "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
5732
8712391bbf3d tuned block indent;
wenzelm
parents: 5694
diff changeset
    27
  "_record_type"	:: "field_types => type"                   	("(3'(| _ |'))")
8712391bbf3d tuned block indent;
wenzelm
parents: 5694
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*)
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    31
  "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    32
  ""                	:: "field => fields"                		("_")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    33
  "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
5732
8712391bbf3d tuned block indent;
wenzelm
parents: 5694
diff changeset
    34
  "_record"         	:: "fields => 'a"                   		("(3'(| _ |'))")
8712391bbf3d tuned block indent;
wenzelm
parents: 5694
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*)
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    38
  "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    39
  ""                	:: "update => updates"               		("_")
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    40
  "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
5732
8712391bbf3d tuned block indent;
wenzelm
parents: 5694
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
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    43
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    44
(* type class for record extensions *)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    45
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 5732
diff changeset
    46
axclass more < "term"
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    47
instance unit :: more
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents: 5732
diff changeset
    48
  by intro_classes
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    49
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
(* initialize the package *)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    52
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    53
setup
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    54
  RecordPackage.setup
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
end