src/HOL/Record.thy
author schirmer
Mon May 03 23:22:17 2004 +0200 (2004-05-03)
changeset 14700 2f885b7e5ba7
parent 14080 9a50427d7165
child 14701 62a724ce51c7
permissions -rw-r--r--
reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.
wenzelm@4870
     1
(*  Title:      HOL/Record.thy
wenzelm@4870
     2
    ID:         $Id$
schirmer@14700
     3
    Author:     Wolfgang Naraschewski, Norbert Schirmer  and Markus Wenzel, TU Muenchen
wenzelm@4870
     4
*)
wenzelm@4870
     5
wenzelm@11826
     6
theory Record = Product_Type
wenzelm@11821
     7
files ("Tools/record_package.ML"):
wenzelm@4870
     8
schirmer@14700
     9
ML {*
schirmer@14700
    10
val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
schirmer@14700
    11
by (rtac h2 1);
schirmer@14700
    12
by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
schirmer@14700
    13
qed "meta_allE";
schirmer@14700
    14
*}
wenzelm@11821
    15
schirmer@14700
    16
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
schirmer@14700
    17
  by simp
wenzelm@11826
    18
schirmer@14700
    19
lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
schirmer@14700
    20
  by simp
wenzelm@11826
    21
schirmer@14700
    22
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
schirmer@14700
    23
  by simp
berghofe@14080
    24
wenzelm@11821
    25
wenzelm@11833
    26
subsection {* Concrete record syntax *}
wenzelm@4870
    27
wenzelm@4870
    28
nonterminals
wenzelm@5198
    29
  ident field_type field_types field fields update updates
wenzelm@4870
    30
syntax
wenzelm@11821
    31
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
    32
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
    33
wenzelm@11821
    34
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
    35
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
    36
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
    37
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
    38
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
    39
wenzelm@11821
    40
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
    41
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
    42
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
    43
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
    44
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
    45
wenzelm@10641
    46
  "_update_name"        :: idt
wenzelm@11821
    47
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
    48
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
    49
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
    50
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
    51
wenzelm@10331
    52
syntax (xsymbols)
wenzelm@11821
    53
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
    54
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
    55
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
    56
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
    57
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
    58
schirmer@14700
    59
(* 
wenzelm@11833
    60
schirmer@14700
    61
  "_structure"             :: "fields => 'a"          ("(3{| _ |})")
schirmer@14700
    62
  "_structure_scheme"      :: "[fields, 'a] => 'a"    ("(3{| _,/ (2... =/ _) |})")
schirmer@14700
    63
  
schirmer@14700
    64
  "_structure_update_name":: idt
schirmer@14700
    65
  "_structure_update"  :: "['a, updates] \<Rightarrow> 'b"    ("_/(3{| _ |})" [900,0] 900)
wenzelm@11833
    66
schirmer@14700
    67
  "_structure_type"        :: "field_types => type"    ("(3{| _ |})")
schirmer@14700
    68
  "_structure_type_scheme" :: "[field_types, type] => type" 
schirmer@14700
    69
                                      ("(3{| _,/ (2... ::/ _) |})")
schirmer@14700
    70
syntax (xsymbols)
schirmer@14700
    71
schirmer@14700
    72
 "_structure_scheme"   :: "[fields, 'a] => 'a"       ("(3{|_,/ (2\<dots> =/ _)|})")
schirmer@14700
    73
schirmer@14700
    74
  "_structure_type_scheme" :: "[field_types, type] => type"        
schirmer@14700
    75
                                      ("(3{|_,/ (2\<dots> ::/ _)|})")
schirmer@14700
    76
schirmer@14700
    77
*)
schirmer@14700
    78
use "Tools/record_package.ML";
schirmer@14700
    79
setup RecordPackage.setup;
wenzelm@10641
    80
wenzelm@4870
    81
end
schirmer@14700
    82