src/HOL/Record.thy
author berghofe
Sun Jun 29 21:27:28 2003 +0200 (2003-06-29)
changeset 14080 9a50427d7165
parent 13421 8fcdf4a26468
child 14700 2f885b7e5ba7
permissions -rw-r--r--
Added split_paired_All rule for splitting variables bound by
object-level universal quantifiers.
     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 lemma (in product_type)
    22     "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    23   by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    24 
    25 lemma (in product_type) conv1: "dest1 (pair x y) = x"
    26   by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    27 
    28 lemma (in product_type) conv2: "dest2 (pair x y) = y"
    29   by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    30 
    31 lemma (in product_type) induct [induct type]:
    32   assumes hyp: "!!x y. P (pair x y)"
    33   shows "P p"
    34 proof (rule type_definition.Abs_induct [OF "typedef"])
    35   fix q show "P (Abs q)"
    36   proof (induct q)
    37     fix x y have "P (pair x y)" by (rule hyp)
    38     also have "pair x y = Abs (x, y)" by (simp only: pair)
    39     finally show "P (Abs (x, y))" .
    40   qed
    41 qed
    42 
    43 lemma (in product_type) cases [cases type]:
    44     "(!!x y. p = pair x y ==> C) ==> C"
    45   by (induct p) (auto simp add: "inject")
    46 
    47 lemma (in product_type) surjective_pairing:
    48     "p = pair (dest1 p) (dest2 p)"
    49   by (induct p) (simp only: conv1 conv2)
    50 
    51 lemma (in product_type) split_paired_all:
    52   "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
    53 proof
    54   fix a b
    55   assume "!!x. PROP P x"
    56   thus "PROP P (pair a b)" .
    57 next
    58   fix x
    59   assume "!!a b. PROP P (pair a b)"
    60   hence "PROP P (pair (dest1 x) (dest2 x))" .
    61   thus "PROP P x" by (simp only: surjective_pairing [symmetric])
    62 qed
    63 
    64 lemma (in product_type) split_paired_All:
    65   "(ALL x. P x) = (ALL a b. P (pair a b))"
    66 proof
    67   fix a b
    68   assume "ALL x. P x"
    69   thus "ALL a b. P (pair a b)" by rules
    70 next
    71   assume P: "ALL a b. P (pair a b)"
    72   show "ALL x. P x"
    73   proof
    74     fix x
    75     from P have "P (pair (dest1 x) (dest2 x))" by rules
    76     thus "P x" by (simp only: surjective_pairing [symmetric])
    77   qed
    78 qed
    79 
    80 
    81 subsection {* Concrete record syntax *}
    82 
    83 nonterminals
    84   ident field_type field_types field fields update updates
    85 
    86 syntax
    87   "_constify"           :: "id => ident"                        ("_")
    88   "_constify"           :: "longid => ident"                    ("_")
    89 
    90   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
    91   ""                    :: "field_type => field_types"          ("_")
    92   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
    93   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    94   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    95 
    96   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
    97   ""                    :: "field => fields"                    ("_")
    98   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
    99   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   100   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   101 
   102   "_update_name"        :: idt
   103   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   104   ""                    :: "update => updates"                  ("_")
   105   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   106   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   107 
   108 syntax (xsymbols)
   109   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   110   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   111   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   112   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   113   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   114 
   115 
   116 subsection {* Package setup *}
   117 
   118 use "Tools/record_package.ML"
   119 setup RecordPackage.setup
   120 
   121 end