src/HOL/Record.thy
author wenzelm
Thu Oct 18 21:22:40 2001 +0200 (2001-10-18)
changeset 11833 475f772ab643
parent 11826 2203c7f9ec40
child 11956 b814360b0267
permissions -rw-r--r--
tuned;
     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 constdefs
    15   product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
    16     ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
    17   "product_type Rep Abs pair dest1 dest2 ==
    18     type_definition Rep Abs UNIV \<and>
    19     pair = (\<lambda>a b. Abs (a, b)) \<and>
    20     dest1 = (\<lambda>p. fst (Rep p)) \<and>
    21     dest2 = (\<lambda>p. snd (Rep p))"
    22 
    23 lemma product_typeI:
    24   "type_definition Rep Abs UNIV ==>
    25     pair == \<lambda>a b. Abs (a, b) ==>
    26     dest1 == (\<lambda>p. fst (Rep p)) ==>
    27     dest2 == (\<lambda>p. snd (Rep p)) ==>
    28     product_type Rep Abs pair dest1 dest2"
    29   by (simp add: product_type_def)
    30 
    31 lemma product_type_typedef:
    32     "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
    33   by (unfold product_type_def) blast
    34 
    35 lemma product_type_pair:
    36     "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
    37   by (unfold product_type_def) blast
    38 
    39 lemma product_type_dest1:
    40     "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
    41   by (unfold product_type_def) blast
    42 
    43 lemma product_type_dest2:
    44     "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
    45   by (unfold product_type_def) blast
    46 
    47 
    48 theorem product_type_inject:
    49   "product_type Rep Abs pair dest1 dest2 ==>
    50     (pair x y = pair x' y') = (x = x' \<and> y = y')"
    51 proof -
    52   case rule_context
    53   show ?thesis
    54     by (simp add: product_type_pair [OF rule_context]
    55       Abs_inject [OF product_type_typedef [OF rule_context]])
    56 qed
    57 
    58 theorem product_type_conv1:
    59   "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
    60 proof -
    61   case rule_context
    62   show ?thesis
    63     by (simp add: product_type_pair [OF rule_context]
    64       product_type_dest1 [OF rule_context]
    65       Abs_inverse [OF product_type_typedef [OF rule_context]])
    66 qed
    67 
    68 theorem product_type_conv2:
    69   "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
    70 proof -
    71   case rule_context
    72   show ?thesis
    73     by (simp add: product_type_pair [OF rule_context]
    74       product_type_dest2 [OF rule_context]
    75       Abs_inverse [OF product_type_typedef [OF rule_context]])
    76 qed
    77 
    78 theorem product_type_induct [induct set: product_type]:
    79   "product_type Rep Abs pair dest1 dest2 ==>
    80     (!!x y. P (pair x y)) ==> P p"
    81 proof -
    82   assume hyp: "!!x y. P (pair x y)"
    83   assume prod_type: "product_type Rep Abs pair dest1 dest2"
    84   show "P p"
    85   proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
    86     fix pair show "P (Abs pair)"
    87     proof (rule prod_induct)
    88       fix x y from hyp show "P (Abs (x, y))"
    89         by (simp only: product_type_pair [OF prod_type])
    90     qed
    91   qed
    92 qed
    93 
    94 theorem product_type_cases [cases set: product_type]:
    95   "product_type Rep Abs pair dest1 dest2 ==>
    96     (!!x y. p = pair x y ==> C) ==> C"
    97 proof -
    98   assume prod_type: "product_type Rep Abs pair dest1 dest2"
    99   assume "!!x y. p = pair x y ==> C"
   100   with prod_type show C
   101     by (induct p) (simp only: product_type_inject [OF prod_type], blast)
   102 qed
   103 
   104 theorem product_type_surjective_pairing:
   105   "product_type Rep Abs pair dest1 dest2 ==>
   106     p = pair (dest1 p) (dest2 p)"
   107 proof -
   108   case rule_context
   109   thus ?thesis by (induct p)
   110     (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
   111 qed
   112 
   113 theorem product_type_split_paired_all:
   114   "product_type Rep Abs pair dest1 dest2 ==>
   115   (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
   116 proof
   117   fix a b
   118   assume "!!x. PROP P x"
   119   thus "PROP P (pair a b)" .
   120 next
   121   case rule_context
   122   fix x
   123   assume "!!a b. PROP P (pair a b)"
   124   hence "PROP P (pair (dest1 x) (dest2 x))" .
   125   thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
   126 qed
   127 
   128 
   129 subsection {* Type class for record extensions *}
   130 
   131 axclass more < "term"
   132 instance unit :: more ..
   133 
   134 
   135 subsection {* Concrete record syntax *}
   136 
   137 nonterminals
   138   ident field_type field_types field fields update updates
   139 
   140 syntax
   141   "_constify"           :: "id => ident"                        ("_")
   142   "_constify"           :: "longid => ident"                    ("_")
   143 
   144   "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
   145   ""                    :: "field_type => field_types"          ("_")
   146   "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
   147   "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   148   "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   149 
   150   "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
   151   ""                    :: "field => fields"                    ("_")
   152   "_fields"             :: "[field, fields] => fields"          ("_,/ _")
   153   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   154   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   155 
   156   "_update_name"        :: idt
   157   "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
   158   ""                    :: "update => updates"                  ("_")
   159   "_updates"            :: "[update, updates] => updates"       ("_,/ _")
   160   "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
   161 
   162 syntax (xsymbols)
   163   "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   164   "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   165   "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
   166   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   167   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   168 
   169 
   170 subsection {* Package setup *}
   171 
   172 use "Tools/record_package.ML"
   173 setup RecordPackage.setup
   174 
   175 end