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.
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@13412
    14
locale product_type =
wenzelm@13412
    15
  fixes Rep and Abs and pair and dest1 and dest2
wenzelm@13412
    16
  assumes "typedef": "type_definition Rep Abs UNIV"
wenzelm@13412
    17
    and pair: "pair == (\<lambda>a b. Abs (a, b))"
wenzelm@13412
    18
    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
wenzelm@13412
    19
    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
wenzelm@11821
    20
wenzelm@13412
    21
lemma (in product_type)
wenzelm@13412
    22
    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
wenzelm@13412
    23
  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
wenzelm@11821
    24
wenzelm@13412
    25
lemma (in product_type) conv1: "dest1 (pair x y) = x"
wenzelm@13412
    26
  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
wenzelm@11826
    27
wenzelm@13412
    28
lemma (in product_type) conv2: "dest2 (pair x y) = y"
wenzelm@13412
    29
  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
wenzelm@11821
    30
wenzelm@13412
    31
lemma (in product_type) induct [induct type]:
wenzelm@13412
    32
  assumes hyp: "!!x y. P (pair x y)"
wenzelm@13412
    33
  shows "P p"
wenzelm@13412
    34
proof (rule type_definition.Abs_induct [OF "typedef"])
wenzelm@13412
    35
  fix q show "P (Abs q)"
wenzelm@13412
    36
  proof (induct q)
wenzelm@13412
    37
    fix x y have "P (pair x y)" by (rule hyp)
wenzelm@13412
    38
    also have "pair x y = Abs (x, y)" by (simp only: pair)
wenzelm@13412
    39
    finally show "P (Abs (x, y))" .
wenzelm@11821
    40
  qed
wenzelm@11821
    41
qed
wenzelm@11821
    42
wenzelm@13412
    43
lemma (in product_type) cases [cases type]:
wenzelm@13412
    44
    "(!!x y. p = pair x y ==> C) ==> C"
wenzelm@13412
    45
  by (induct p) (auto simp add: "inject")
wenzelm@11826
    46
wenzelm@13412
    47
lemma (in product_type) surjective_pairing:
wenzelm@13412
    48
    "p = pair (dest1 p) (dest2 p)"
wenzelm@13412
    49
  by (induct p) (simp only: conv1 conv2)
wenzelm@11826
    50
wenzelm@13412
    51
lemma (in product_type) split_paired_all:
wenzelm@13412
    52
  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
wenzelm@11826
    53
proof
wenzelm@11826
    54
  fix a b
wenzelm@11826
    55
  assume "!!x. PROP P x"
wenzelm@11826
    56
  thus "PROP P (pair a b)" .
wenzelm@11826
    57
next
wenzelm@11826
    58
  fix x
wenzelm@11826
    59
  assume "!!a b. PROP P (pair a b)"
wenzelm@11826
    60
  hence "PROP P (pair (dest1 x) (dest2 x))" .
wenzelm@13412
    61
  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
wenzelm@11826
    62
qed
wenzelm@11826
    63
berghofe@14080
    64
lemma (in product_type) split_paired_All:
berghofe@14080
    65
  "(ALL x. P x) = (ALL a b. P (pair a b))"
berghofe@14080
    66
proof
berghofe@14080
    67
  fix a b
berghofe@14080
    68
  assume "ALL x. P x"
berghofe@14080
    69
  thus "ALL a b. P (pair a b)" by rules
berghofe@14080
    70
next
berghofe@14080
    71
  assume P: "ALL a b. P (pair a b)"
berghofe@14080
    72
  show "ALL x. P x"
berghofe@14080
    73
  proof
berghofe@14080
    74
    fix x
berghofe@14080
    75
    from P have "P (pair (dest1 x) (dest2 x))" by rules
berghofe@14080
    76
    thus "P x" by (simp only: surjective_pairing [symmetric])
berghofe@14080
    77
  qed
berghofe@14080
    78
qed
berghofe@14080
    79
wenzelm@11821
    80
wenzelm@11833
    81
subsection {* Concrete record syntax *}
wenzelm@4870
    82
wenzelm@4870
    83
nonterminals
wenzelm@5198
    84
  ident field_type field_types field fields update updates
wenzelm@4870
    85
wenzelm@4870
    86
syntax
wenzelm@11821
    87
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
    88
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
    89
wenzelm@11821
    90
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
    91
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
    92
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
    93
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
    94
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
    95
wenzelm@11821
    96
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
    97
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
    98
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
    99
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
   100
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
   101
wenzelm@10641
   102
  "_update_name"        :: idt
wenzelm@11821
   103
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
   104
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
   105
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
   106
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
   107
wenzelm@10331
   108
syntax (xsymbols)
wenzelm@11821
   109
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   110
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
   111
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   112
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
   113
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
   114
wenzelm@11833
   115
wenzelm@11833
   116
subsection {* Package setup *}
wenzelm@11833
   117
wenzelm@11833
   118
use "Tools/record_package.ML"
wenzelm@11833
   119
setup RecordPackage.setup
wenzelm@10641
   120
wenzelm@4870
   121
end