src/HOL/Record.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 16114 8d453f906e43
child 17957 d31acb64aa9a
permissions -rw-r--r--
migrated theory headers to new format
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$
16114
wenzelm
parents: 15140
diff changeset
     3
    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
4870
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
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14701
diff changeset
     6
theory Record
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     7
imports Product_Type
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16114
diff changeset
     8
uses ("Tools/record_package.ML")
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14701
diff changeset
     9
begin
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    10
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    11
ML {*
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    12
val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    13
by (rtac h2 1);
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    14
by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    15
qed "meta_allE";
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    16
*}
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    17
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    18
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    19
  by simp
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    20
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    21
lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    22
  by simp
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    23
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    24
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    25
  by simp
14080
9a50427d7165 Added split_paired_All rule for splitting variables bound by
berghofe
parents: 13421
diff changeset
    26
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    27
11833
wenzelm
parents: 11826
diff changeset
    28
subsection {* Concrete record syntax *}
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    29
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    30
nonterminals
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    31
  ident field_type field_types field fields update updates
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    32
syntax
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    33
  "_constify"           :: "id => ident"                        ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    34
  "_constify"           :: "longid => ident"                    ("_")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    35
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    36
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    37
  ""                    :: "field_type => field_types"          ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    38
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    39
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    40
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    41
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    42
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    43
  ""                    :: "field => fields"                    ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    44
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    45
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    46
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
    47
10641
d1533f63c738 added "_update_name" and parse_translation;
wenzelm
parents: 10331
diff changeset
    48
  "_update_name"        :: idt
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    49
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    50
  ""                    :: "update => updates"                  ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    51
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    52
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    53
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10309
diff changeset
    54
syntax (xsymbols)
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    55
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    56
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    57
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    58
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
    59
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729
40cfc3dd27da \<dots> syntax;
wenzelm
parents: 7357
diff changeset
    60
16114
wenzelm
parents: 15140
diff changeset
    61
use "Tools/record_package.ML"
wenzelm
parents: 15140
diff changeset
    62
setup RecordPackage.setup
10641
d1533f63c738 added "_update_name" and parse_translation;
wenzelm
parents: 10331
diff changeset
    63
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    64
end
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14080
diff changeset
    65