src/HOL/Record.thy
author wenzelm
Wed Oct 17 20:24:37 2001 +0200 (2001-10-17)
changeset 11821 ad32c92435db
parent 11489 1fd5469c195e
child 11826 2203c7f9ec40
permissions -rw-r--r--
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@7357
     8
theory Record = Datatype
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@11821
    16
    ('a => 'b => 'p) => (('a => 'b => 'c) => 'p => 'c) => bool"
wenzelm@11821
    17
  "product_type Rep Abs intro elim ==
wenzelm@11821
    18
    type_definition Rep Abs UNIV \<and>
wenzelm@11821
    19
    intro = (\<lambda>a b. Abs (a, b)) \<and>
wenzelm@11821
    20
    elim = (\<lambda>f. prod_case f o Rep)"
wenzelm@11821
    21
wenzelm@11821
    22
lemma product_typeI:
wenzelm@11821
    23
  "type_definition Rep Abs A ==> A == UNIV ==>
wenzelm@11821
    24
    intro == \<lambda>a b. Abs (a, b) ==> elim == \<lambda>f. prod_case f o Rep ==>
wenzelm@11821
    25
    product_type Rep Abs intro elim"
wenzelm@11821
    26
  by (simp add: product_type_def)
wenzelm@11821
    27
wenzelm@11821
    28
lemma product_type_typedef:
wenzelm@11821
    29
    "product_type Rep Abs intro elim ==> type_definition Rep Abs UNIV"
wenzelm@11821
    30
  by (unfold product_type_def) blast
wenzelm@11821
    31
wenzelm@11821
    32
lemma product_type_intro:
wenzelm@11821
    33
    "product_type Rep Abs intro elim ==> intro = (\<lambda>a b. Abs (a, b))"
wenzelm@11821
    34
  by (unfold product_type_def) blast
wenzelm@11821
    35
wenzelm@11821
    36
lemma product_type_elim:
wenzelm@11821
    37
    "product_type Rep Abs intro elim ==> elim = (\<lambda>f. prod_case f o Rep)"
wenzelm@11821
    38
  by (unfold product_type_def) fast  (* FIXME blast fails!? *)
wenzelm@11821
    39
wenzelm@11821
    40
lemma product_type_inject:
wenzelm@11821
    41
  "product_type Rep Abs intro elim ==>
wenzelm@11821
    42
    (intro x y = intro x' y') = (x = x' \<and> y = y')"
wenzelm@11821
    43
proof -
wenzelm@11821
    44
  case rule_context
wenzelm@11821
    45
  show ?thesis
wenzelm@11821
    46
    by (simp add: product_type_intro [OF rule_context]
wenzelm@11821
    47
      Abs_inject [OF product_type_typedef [OF rule_context]])
wenzelm@11821
    48
qed
wenzelm@11821
    49
wenzelm@11821
    50
lemma product_type_surject:
wenzelm@11821
    51
  "product_type Rep Abs intro elim ==>
wenzelm@11821
    52
    elim f (intro x y) = f x y"
wenzelm@11821
    53
proof -
wenzelm@11821
    54
  case rule_context
wenzelm@11821
    55
  show ?thesis
wenzelm@11821
    56
    by (simp add: product_type_intro [OF rule_context]
wenzelm@11821
    57
      product_type_elim [OF rule_context]
wenzelm@11821
    58
      Abs_inverse [OF product_type_typedef [OF rule_context]])
wenzelm@11821
    59
qed
wenzelm@11821
    60
wenzelm@11821
    61
lemma product_type_induct:
wenzelm@11821
    62
  "product_type Rep Abs intro elim ==>
wenzelm@11821
    63
    (!!x y. P (intro x y)) ==> P p"
wenzelm@11821
    64
proof -
wenzelm@11821
    65
  assume hyp: "!!x y. P (intro x y)"
wenzelm@11821
    66
  assume prod_type: "product_type Rep Abs intro elim"
wenzelm@11821
    67
  show "P p"
wenzelm@11821
    68
  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
wenzelm@11821
    69
    fix pair show "P (Abs pair)"
wenzelm@11821
    70
    proof (rule prod.induct)
wenzelm@11821
    71
      fix x y from hyp show "P (Abs (x, y))"
wenzelm@11821
    72
	by (simp only: product_type_intro [OF prod_type])
wenzelm@11821
    73
    qed
wenzelm@11821
    74
  qed
wenzelm@11821
    75
qed
wenzelm@11821
    76
wenzelm@11821
    77
wenzelm@11821
    78
text {* \medskip Type class for record extensions. *}
wenzelm@11821
    79
wenzelm@11821
    80
axclass more < "term"
wenzelm@11821
    81
instance unit :: more ..
wenzelm@11821
    82
wenzelm@11821
    83
wenzelm@11821
    84
subsection {* Concrete syntax of records *}
wenzelm@4870
    85
wenzelm@4870
    86
nonterminals
wenzelm@5198
    87
  ident field_type field_types field fields update updates
wenzelm@4870
    88
wenzelm@4870
    89
syntax
wenzelm@11821
    90
  "_constify"           :: "id => ident"                        ("_")
wenzelm@11821
    91
  "_constify"           :: "longid => ident"                    ("_")
wenzelm@5198
    92
wenzelm@11821
    93
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
wenzelm@11821
    94
  ""                    :: "field_type => field_types"          ("_")
wenzelm@11821
    95
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
wenzelm@11821
    96
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
wenzelm@10093
    97
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
wenzelm@5198
    98
wenzelm@11821
    99
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
wenzelm@11821
   100
  ""                    :: "field => fields"                    ("_")
wenzelm@11821
   101
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
wenzelm@11821
   102
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
wenzelm@10093
   103
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
wenzelm@5198
   104
wenzelm@10641
   105
  "_update_name"        :: idt
wenzelm@11821
   106
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
wenzelm@11821
   107
  ""                    :: "update => updates"                  ("_")
wenzelm@11821
   108
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
wenzelm@10093
   109
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
wenzelm@4870
   110
wenzelm@10331
   111
syntax (xsymbols)
wenzelm@11821
   112
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   113
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
wenzelm@10093
   114
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
wenzelm@10093
   115
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
wenzelm@10093
   116
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
wenzelm@9729
   117
wenzelm@11821
   118
wenzelm@11821
   119
subsection {* Package setup *}
wenzelm@11821
   120
wenzelm@11821
   121
use "Tools/record_package.ML"
wenzelm@11821
   122
wenzelm@10641
   123
parse_translation {*
wenzelm@10641
   124
  let
wenzelm@10641
   125
    fun update_name_tr (Free (x, T) :: ts) =
wenzelm@10641
   126
          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
wenzelm@10641
   127
      | update_name_tr (Const (x, T) :: ts) =
wenzelm@10641
   128
          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
wenzelm@10641
   129
      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
wenzelm@10641
   130
          Term.list_comb (c $ update_name_tr [t] $
wenzelm@10641
   131
            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
wenzelm@10641
   132
      | update_name_tr ts = raise TERM ("update_name_tr", ts);
wenzelm@10641
   133
  in [("_update_name", update_name_tr)] end
wenzelm@10641
   134
*}
wenzelm@10641
   135
wenzelm@11821
   136
setup RecordPackage.setup
wenzelm@4870
   137
wenzelm@4870
   138
end