src/HOL/Record.thy
author wenzelm
Wed Jul 24 00:10:52 2002 +0200 (2002-07-24)
changeset 13412 666137b488a4
parent 11956 b814360b0267
child 13421 8fcdf4a26468
permissions -rw-r--r--
predicate defs via locales;
     1 (*  Title:      HOL/Record.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Extensible records with structural subtyping *}
     7 
     8 theory Record = Product_Type
     9 files ("Tools/record_package.ML"):
    10 
    11 
    12 subsection {* Abstract product types *}
    13 
    14 locale product_type =
    15   fixes Rep and Abs and pair and dest1 and dest2
    16   assumes "typedef": "type_definition Rep Abs UNIV"
    17     and pair: "pair == (\<lambda>a b. Abs (a, b))"
    18     and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
    19     and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
    20 
    21 lemmas product_typeI =
    22   product_type.intro [OF product_type_axioms.intro]
    23 
    24 lemma (in product_type)
    25     "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    26   by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    27 
    28 lemma (in product_type) conv1: "dest1 (pair x y) = x"
    29   by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    30 
    31 lemma (in product_type) conv2: "dest2 (pair x y) = y"
    32   by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    33 
    34 lemma (in product_type) induct [induct type]:
    35   assumes hyp: "!!x y. P (pair x y)"
    36   shows "P p"
    37 proof (rule type_definition.Abs_induct [OF "typedef"])
    38   fix q show "P (Abs q)"
    39   proof (induct q)
    40     fix x y have "P (pair x y)" by (rule hyp)
    41     also have "pair x y = Abs (x, y)" by (simp only: pair)
    42     finally show "P (Abs (x, y))" .
    43   qed
    44 qed
    45 
    46 lemma (in product_type) cases [cases type]:
    47     "(!!x y. p = pair x y ==> C) ==> C"
    48   by (induct p) (auto simp add: "inject")
    49 
    50 lemma (in product_type) surjective_pairing:
    51     "p = pair (dest1 p) (dest2 p)"
    52   by (induct p) (simp only: conv1 conv2)
    53 
    54 lemma (in product_type) split_paired_all:
    55   "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
    56 proof
    57   fix a b
    58   assume "!!x. PROP P x"
    59   thus "PROP P (pair a b)" .
    60 next
    61   fix x
    62   assume "!!a b. PROP P (pair a b)"
    63   hence "PROP P (pair (dest1 x) (dest2 x))" .
    64   thus "PROP P x" by (simp only: surjective_pairing [symmetric])
    65 qed
    66 
    67 
    68 subsection {* Concrete record syntax *}
    69 
    70 nonterminals
    71   ident field_type field_types field fields update updates
    72 
    73 syntax
    74   "_constify"           :: "id => ident"                        ("_")
    75   "_constify"           :: "longid => ident"                    ("_")
    76 
    77   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
    78   ""                    :: "field_type => field_types"          ("_")
    79   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
    80   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    81   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    82 
    83   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
    84   ""                    :: "field => fields"                    ("_")
    85   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
    86   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
    87   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    88 
    89   "_update_name"        :: idt
    90   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
    91   ""                    :: "update => updates"                  ("_")
    92   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
    93   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
    94 
    95 syntax (xsymbols)
    96   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
    97   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    98   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
    99   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   100   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   101 
   102 
   103 subsection {* Package setup *}
   104 
   105 use "Tools/record_package.ML"
   106 setup RecordPackage.setup
   107 
   108 end