src/HOL/Record.thy
author wenzelm
Thu Oct 18 21:01:18 2001 +0200 (2001-10-18)
changeset 11826 2203c7f9ec40
parent 11821 ad32c92435db
child 11833 475f772ab643
permissions -rw-r--r--
proper setup for abstract product types;
wenzelm@4870
     1
(*  Title:      HOL/Record.thy
wenzelm@4870
     2
    ID:         $Id$
wenzelm@4870
     3
    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
wenzelm@4870
     4
*)
wenzelm@4870
     5
wenzelm@11821
     6
header {* Extensible records with structural subtyping *}
wenzelm@11821
     7
wenzelm@11826
     8
theory Record = Product_Type
wenzelm@11821
     9
files ("Tools/record_package.ML"):
wenzelm@4870
    10
wenzelm@4870
    11
wenzelm@11821
    12
subsection {* Abstract product types *}
wenzelm@11821
    13
wenzelm@11821
    14
constdefs
wenzelm@11821
    15
  product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
wenzelm@11826
    16
    ('a => 'b => 'p) => ('p \<Rightarrow> 'a) => ('p => 'b) => bool"
wenzelm@11826
    17
  "product_type Rep Abs pair dest1 dest2 ==
wenzelm@11821
    18
    type_definition Rep Abs UNIV \<and>
wenzelm@11826
    19
    pair = (\<lambda>a b. Abs (a, b)) \<and>
wenzelm@11826
    20
    dest1 = (\<lambda>p. fst (Rep p)) \<and>
wenzelm@11826
    21
    dest2 = (\<lambda>p. snd (Rep p))"
wenzelm@11821
    22
wenzelm@11821
    23
lemma product_typeI:
wenzelm@11826
    24
  "type_definition Rep Abs UNIV ==>
wenzelm@11826
    25
    pair == \<lambda>a b. Abs (a, b) ==>
wenzelm@11826
    26
    dest1 == (\<lambda>p. fst (Rep p)) \<Longrightarrow>
wenzelm@11826
    27
    dest2 == (\<lambda>p. snd (Rep p)) \<Longrightarrow>
wenzelm@11826
    28
    product_type Rep Abs pair dest1 dest2"
wenzelm@11821
    29
  by (simp add: product_type_def)
wenzelm@11821
    30
wenzelm@11821
    31
lemma product_type_typedef:
wenzelm@11826
    32
    "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
wenzelm@11821
    33
  by (unfold product_type_def) blast
wenzelm@11821
    34
wenzelm@11826
    35
lemma product_type_pair:
wenzelm@11826
    36
    "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
wenzelm@11826
    37
  by (unfold product_type_def) blast
wenzelm@11826
    38
wenzelm@11826
    39
lemma product_type_dest1:
wenzelm@11826
    40
    "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
wenzelm@11821
    41
  by (unfold product_type_def) blast
wenzelm@11821
    42
wenzelm@11826
    43
lemma product_type_dest2:
wenzelm@11826
    44
    "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
wenzelm@11826
    45
  by (unfold product_type_def) blast
wenzelm@11826
    46
wenzelm@11821
    47
wenzelm@11826
    48
theorem product_type_inject:
wenzelm@11826
    49
  "product_type Rep Abs pair dest1 dest2 ==>
wenzelm@11826
    50
    (pair x y = pair x' y') = (x = x' \<and> y = y')"
wenzelm@11826
    51
proof -
wenzelm@11826
    52
  case rule_context
wenzelm@11826
    53
  show ?thesis
wenzelm@11826
    54
    by (simp add: product_type_pair [OF rule_context]
wenzelm@11826
    55
      Abs_inject [OF product_type_typedef [OF rule_context]])
wenzelm@11826
    56
qed
wenzelm@11826
    57
wenzelm@11826
    58
theorem product_type_conv1:
wenzelm@11826
    59
  "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
wenzelm@11821
    60
proof -
wenzelm@11821
    61
  case rule_context
wenzelm@11821
    62
  show ?thesis
wenzelm@11826
    63
    by (simp add: product_type_pair [OF rule_context]
wenzelm@11826
    64
      product_type_dest1 [OF rule_context]
wenzelm@11826
    65
      Abs_inverse [OF product_type_typedef [OF rule_context]])
wenzelm@11821
    66
qed
wenzelm@11821
    67
wenzelm@11826
    68
theorem product_type_conv2:
wenzelm@11826
    69
  "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
wenzelm@11821
    70
proof -
wenzelm@11821
    71
  case rule_context
wenzelm@11821
    72
  show ?thesis
wenzelm@11826
    73
    by (simp add: product_type_pair [OF rule_context]
wenzelm@11826
    74
      product_type_dest2 [OF rule_context]
wenzelm@11821
    75
      Abs_inverse [OF product_type_typedef [OF rule_context]])
wenzelm@11821
    76
qed
wenzelm@11821
    77
wenzelm@11826
    78
theorem product_type_induct [induct set: product_type]:
wenzelm@11826
    79
  "product_type Rep Abs pair dest1 dest2 ==>
wenzelm@11826
    80
    (!!x y. P (pair x y)) ==> P p"
wenzelm@11821
    81
proof -
wenzelm@11826
    82
  assume hyp: "!!x y. P (pair x y)"
wenzelm@11826
    83
  assume prod_type: "product_type Rep Abs pair dest1 dest2"
wenzelm@11821
    84
  show "P p"
wenzelm@11821
    85
  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
wenzelm@11821
    86
    fix pair show "P (Abs pair)"
wenzelm@11826
    87
    proof (rule prod_induct)
wenzelm@11821
    88
      fix x y from hyp show "P (Abs (x, y))"
wenzelm@11826
    89
        by (simp only: product_type_pair [OF prod_type])
wenzelm@11821
    90
    qed
wenzelm@11821
    91
  qed
wenzelm@11821
    92
qed
wenzelm@11821
    93
wenzelm@11826
    94
theorem product_type_cases [cases set: product_type]:
wenzelm@11826
    95
  "product_type Rep Abs pair dest1 dest2 ==>
wenzelm@11826
    96
    (!!x y. p = pair x y \<Longrightarrow> C) ==> C"
wenzelm@11826
    97
proof -
wenzelm@11826
    98
  assume prod_type: "product_type Rep Abs pair dest1 dest2"
wenzelm@11826
    99
  assume "!!x y. p = pair x y \<Longrightarrow> C"
wenzelm@11826
   100
  with prod_type show C
wenzelm@11826
   101
    by (induct p) (simp only: product_type_inject [OF prod_type], blast)
wenzelm@11826
   102
qed
wenzelm@11826
   103
wenzelm@11826
   104
theorem product_type_surjective_pairing:
wenzelm@11826
   105
  "product_type Rep Abs pair dest1 dest2 ==>
wenzelm@11826
   106
    p = pair (dest1 p) (dest2 p)"
wenzelm@11826
   107
proof -
wenzelm@11826
   108
  case rule_context
wenzelm@11826
   109
  thus ?thesis by (induct p)
wenzelm@11826
   110
    (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
wenzelm@11826
   111
qed
wenzelm@11826
   112
wenzelm@11826
   113
theorem product_type_split_paired_all:
wenzelm@11826
   114
  "product_type Rep Abs pair dest1 dest2 ==>
wenzelm@11826
   115
  (\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (pair a b))"
wenzelm@11826
   116
proof
wenzelm@11826
   117
  fix a b
wenzelm@11826
   118
  assume "!!x. PROP P x"
wenzelm@11826
   119
  thus "PROP P (pair a b)" .
wenzelm@11826
   120
next
wenzelm@11826
   121
  case rule_context
wenzelm@11826
   122
  fix x
wenzelm@11826
   123
  assume "!!a b. PROP P (pair a b)"
wenzelm@11826
   124
  hence "PROP P (pair (dest1 x) (dest2 x))" .
wenzelm@11826
   125
  thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
wenzelm@11826
   126
qed
wenzelm@11826
   127
wenzelm@11821
   128
wenzelm@11821
   129
text {* \medskip Type class for record extensions. *}
wenzelm@11821
   130
wenzelm@11821
   131
axclass more < "term"
wenzelm@11821
   132
instance unit :: more ..
wenzelm@11821
   133
wenzelm@11821
   134
wenzelm@11826
   135
subsection {* Record package setup *}
wenzelm@11826
   136
wenzelm@11826
   137
use "Tools/record_package.ML"
wenzelm@11826
   138
setup RecordPackage.setup
wenzelm@11826
   139
wenzelm@11826
   140
wenzelm@11826
   141
subsection {* Concrete syntax *}
wenzelm@4870
   142
wenzelm@4870
   143
nonterminals
wenzelm@5198
   144
  ident field_type field_types field fields update updates
wenzelm@4870
   145
wenzelm@4870
   146
syntax
wenzelm@11821
   147
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
   148
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
   149
wenzelm@11821
   150
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
   151
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
   152
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
   153
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
   154
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
   155
wenzelm@11821
   156
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
   157
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
   158
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
   159
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
   160
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
   161
wenzelm@10641
   162
  "_update_name"        :: idt
wenzelm@11821
   163
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
   164
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
   165
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
   166
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
   167
wenzelm@10331
   168
syntax (xsymbols)
wenzelm@11821
   169
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   170
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
   171
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   172
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
   173
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
   174
wenzelm@10641
   175
parse_translation {*
wenzelm@10641
   176
  let
wenzelm@10641
   177
    fun update_name_tr (Free (x, T) :: ts) =
wenzelm@10641
   178
          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
wenzelm@10641
   179
      | update_name_tr (Const (x, T) :: ts) =
wenzelm@10641
   180
          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
wenzelm@10641
   181
      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
wenzelm@10641
   182
          Term.list_comb (c $ update_name_tr [t] $
wenzelm@10641
   183
            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
wenzelm@10641
   184
      | update_name_tr ts = raise TERM ("update_name_tr", ts);
wenzelm@10641
   185
  in [("_update_name", update_name_tr)] end
wenzelm@10641
   186
*}
wenzelm@10641
   187
wenzelm@4870
   188
end