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