src/HOL/Record.thy
author tsewell@rubicon.NSW.bigpond.net.au
Thu Aug 27 00:40:53 2009 +1000 (2009-08-27)
changeset 32743 c4e9a48bc50e
parent 31723 f5cafe803b55
child 32744 50406c4951d9
permissions -rw-r--r--
Initial attempt at porting record update to repository Isabelle.
wenzelm@4870
     1
(*  Title:      HOL/Record.thy
tsewell@32743
     2
    ID:         $Id: Record.thy,v 1.33 2007/12/19 15:32:12 schirmer Exp $
wenzelm@16114
     3
    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
wenzelm@4870
     4
*)
wenzelm@4870
     5
wenzelm@22817
     6
header {* Extensible records with structural subtyping *}
wenzelm@22817
     7
nipkow@15131
     8
theory Record
tsewell@32743
     9
imports Product_Type IsTuple
tsewell@32743
    10
uses ("Tools/record_package.ML")
nipkow@15131
    11
begin
wenzelm@4870
    12
schirmer@14700
    13
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
schirmer@14700
    14
  by simp
wenzelm@11826
    15
schirmer@25705
    16
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" 
schirmer@25705
    17
  by (simp add: comp_def)
wenzelm@11821
    18
tsewell@32743
    19
lemma meta_iffD2:
tsewell@32743
    20
  "\<lbrakk> PROP P \<equiv> PROP Q; PROP Q \<rbrakk> \<Longrightarrow> PROP P"
tsewell@32743
    21
  by simp
tsewell@32743
    22
tsewell@32743
    23
lemma o_eq_dest_lhs:
tsewell@32743
    24
  "a o b = c \<Longrightarrow> a (b v) = c v"
tsewell@32743
    25
  by clarsimp
tsewell@32743
    26
tsewell@32743
    27
lemma id_o_refl:
tsewell@32743
    28
  "id o f = f o id"
tsewell@32743
    29
  by simp
tsewell@32743
    30
tsewell@32743
    31
lemma o_eq_id_dest:
tsewell@32743
    32
  "a o b = id o c \<Longrightarrow> a (b v) = c v"
tsewell@32743
    33
  by clarsimp
wenzelm@22817
    34
wenzelm@11833
    35
subsection {* Concrete record syntax *}
wenzelm@4870
    36
wenzelm@4870
    37
nonterminals
wenzelm@5198
    38
  ident field_type field_types field fields update updates
wenzelm@4870
    39
syntax
wenzelm@11821
    40
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
    41
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
    42
wenzelm@11821
    43
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
    44
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
    45
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
    46
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
    47
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
    48
wenzelm@11821
    49
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
    50
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
    51
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
    52
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
    53
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
    54
wenzelm@10641
    55
  "_update_name"        :: idt
wenzelm@11821
    56
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
    57
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
    58
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
    59
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
    60
wenzelm@10331
    61
syntax (xsymbols)
wenzelm@11821
    62
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
    63
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
    64
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
    65
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
    66
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
    67
tsewell@32743
    68
use "Tools/record_package.ML"
tsewell@32743
    69
setup RecordPackage.setup
wenzelm@10641
    70
wenzelm@4870
    71
end