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