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