src/HOL/Record.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21226 a607ae87ee81
child 22744 5cbe966d67a2
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 theory Record
     7 imports Product_Type
     8 uses ("Tools/record_package.ML")
     9 begin
    10 
    11 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    12   by simp
    13 
    14 lemma rec_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True"
    15   by simp
    16 
    17 lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    18   by simp
    19 
    20 constdefs K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
    21 "K_record c x \<equiv> c"
    22 
    23 lemma K_record_apply [simp]: "K_record c x = c"
    24   by (simp add: K_record_def)
    25 
    26 lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
    27   by (rule ext) (simp add: K_record_apply comp_def)
    28 
    29 lemma K_record_cong [cong]: "K_record c x = K_record c x"
    30   by (rule refl)
    31 
    32 subsection {* Concrete record syntax *}
    33 
    34 nonterminals
    35   ident field_type field_types field fields update updates
    36 syntax
    37   "_constify"           :: "id => ident"                        ("_")
    38   "_constify"           :: "longid => ident"                    ("_")
    39 
    40   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
    41   ""                    :: "field_type => field_types"          ("_")
    42   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
    43   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    44   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    45 
    46   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
    47   ""                    :: "field => fields"                    ("_")
    48   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
    49   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
    50   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    51 
    52   "_update_name"        :: idt
    53   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
    54   ""                    :: "update => updates"                  ("_")
    55   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
    56   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
    57 
    58 syntax (xsymbols)
    59   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
    60   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    61   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
    62   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    63   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    64 
    65 use "Tools/record_package.ML"
    66 setup RecordPackage.setup
    67 
    68 end
    69