src/HOL/Record.thy
author wenzelm
Fri, 26 Oct 2001 23:58:21 +0200
changeset 11952 b10f1e8862f4
parent 11833 475f772ab643
child 11956 b814360b0267
permissions -rw-r--r--
* Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Record.thy
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     3
    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     4
*)
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
     5
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
     6
header {* Extensible records with structural subtyping *}
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
     7
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
     8
theory Record = Product_Type
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
     9
files ("Tools/record_package.ML"):
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    10
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
    11
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    12
subsection {* Abstract product types *}
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    13
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    14
constdefs
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    15
  product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
11833
wenzelm
parents: 11826
diff changeset
    16
    ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    17
  "product_type Rep Abs pair dest1 dest2 ==
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    18
    type_definition Rep Abs UNIV \<and>
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    19
    pair = (\<lambda>a b. Abs (a, b)) \<and>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    20
    dest1 = (\<lambda>p. fst (Rep p)) \<and>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    21
    dest2 = (\<lambda>p. snd (Rep p))"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    22
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    23
lemma product_typeI:
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    24
  "type_definition Rep Abs UNIV ==>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    25
    pair == \<lambda>a b. Abs (a, b) ==>
11833
wenzelm
parents: 11826
diff changeset
    26
    dest1 == (\<lambda>p. fst (Rep p)) ==>
wenzelm
parents: 11826
diff changeset
    27
    dest2 == (\<lambda>p. snd (Rep p)) ==>
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    28
    product_type Rep Abs pair dest1 dest2"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    29
  by (simp add: product_type_def)
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    30
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    31
lemma product_type_typedef:
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    32
    "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    33
  by (unfold product_type_def) blast
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    34
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    35
lemma product_type_pair:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    36
    "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    37
  by (unfold product_type_def) blast
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    38
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    39
lemma product_type_dest1:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    40
    "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    41
  by (unfold product_type_def) blast
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    42
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    43
lemma product_type_dest2:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    44
    "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    45
  by (unfold product_type_def) blast
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    46
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    47
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    48
theorem product_type_inject:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    49
  "product_type Rep Abs pair dest1 dest2 ==>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    50
    (pair x y = pair x' y') = (x = x' \<and> y = y')"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    51
proof -
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    52
  case rule_context
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    53
  show ?thesis
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    54
    by (simp add: product_type_pair [OF rule_context]
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    55
      Abs_inject [OF product_type_typedef [OF rule_context]])
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    56
qed
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    57
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    58
theorem product_type_conv1:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    59
  "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    60
proof -
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    61
  case rule_context
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    62
  show ?thesis
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    63
    by (simp add: product_type_pair [OF rule_context]
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    64
      product_type_dest1 [OF rule_context]
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    65
      Abs_inverse [OF product_type_typedef [OF rule_context]])
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    66
qed
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    67
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    68
theorem product_type_conv2:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    69
  "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    70
proof -
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    71
  case rule_context
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    72
  show ?thesis
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    73
    by (simp add: product_type_pair [OF rule_context]
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    74
      product_type_dest2 [OF rule_context]
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    75
      Abs_inverse [OF product_type_typedef [OF rule_context]])
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    76
qed
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    77
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    78
theorem product_type_induct [induct set: product_type]:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    79
  "product_type Rep Abs pair dest1 dest2 ==>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    80
    (!!x y. P (pair x y)) ==> P p"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    81
proof -
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    82
  assume hyp: "!!x y. P (pair x y)"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    83
  assume prod_type: "product_type Rep Abs pair dest1 dest2"
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    84
  show "P p"
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    85
  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    86
    fix pair show "P (Abs pair)"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    87
    proof (rule prod_induct)
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    88
      fix x y from hyp show "P (Abs (x, y))"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    89
        by (simp only: product_type_pair [OF prod_type])
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    90
    qed
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    91
  qed
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    92
qed
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
    93
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    94
theorem product_type_cases [cases set: product_type]:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    95
  "product_type Rep Abs pair dest1 dest2 ==>
11833
wenzelm
parents: 11826
diff changeset
    96
    (!!x y. p = pair x y ==> C) ==> C"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    97
proof -
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
    98
  assume prod_type: "product_type Rep Abs pair dest1 dest2"
11833
wenzelm
parents: 11826
diff changeset
    99
  assume "!!x y. p = pair x y ==> C"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   100
  with prod_type show C
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   101
    by (induct p) (simp only: product_type_inject [OF prod_type], blast)
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   102
qed
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   103
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   104
theorem product_type_surjective_pairing:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   105
  "product_type Rep Abs pair dest1 dest2 ==>
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   106
    p = pair (dest1 p) (dest2 p)"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   107
proof -
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   108
  case rule_context
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   109
  thus ?thesis by (induct p)
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   110
    (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   111
qed
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   112
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   113
theorem product_type_split_paired_all:
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   114
  "product_type Rep Abs pair dest1 dest2 ==>
11833
wenzelm
parents: 11826
diff changeset
   115
  (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
11826
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   116
proof
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   117
  fix a b
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   118
  assume "!!x. PROP P x"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   119
  thus "PROP P (pair a b)" .
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   120
next
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   121
  case rule_context
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   122
  fix x
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   123
  assume "!!a b. PROP P (pair a b)"
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   124
  hence "PROP P (pair (dest1 x) (dest2 x))" .
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   125
  thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   126
qed
2203c7f9ec40 proper setup for abstract product types;
wenzelm
parents: 11821
diff changeset
   127
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   128
11833
wenzelm
parents: 11826
diff changeset
   129
subsection {* Type class for record extensions *}
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   130
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   131
axclass more < "term"
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   132
instance unit :: more ..
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   133
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   134
11833
wenzelm
parents: 11826
diff changeset
   135
subsection {* Concrete record syntax *}
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   136
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   137
nonterminals
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
   138
  ident field_type field_types field fields update updates
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   139
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   140
syntax
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   141
  "_constify"           :: "id => ident"                        ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   142
  "_constify"           :: "longid => ident"                    ("_")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
   143
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   144
  "_field_type"         :: "[ident, type] => field_type"        ("(2_ ::/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   145
  ""                    :: "field_type => field_types"          ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   146
  "_field_types"        :: "[field_type, field_types] => field_types"    ("_,/ _")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   147
  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   148
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3'(| _,/ (2... ::/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
   149
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   150
  "_field"              :: "[ident, 'a] => field"               ("(2_ =/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   151
  ""                    :: "field => fields"                    ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   152
  "_fields"             :: "[field, fields] => fields"          ("_,/ _")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   153
  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   154
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
5198
b1adae4f8b90 added type and update syntax;
wenzelm
parents: 5032
diff changeset
   155
10641
d1533f63c738 added "_update_name" and parse_translation;
wenzelm
parents: 10331
diff changeset
   156
  "_update_name"        :: idt
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   157
  "_update"             :: "[ident, 'a] => update"              ("(2_ :=/ _)")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   158
  ""                    :: "update => updates"                  ("_")
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   159
  "_updates"            :: "[update, updates] => updates"       ("_,/ _")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   160
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3'(| _ |'))" [900,0] 900)
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   161
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10309
diff changeset
   162
syntax (xsymbols)
11821
ad32c92435db abstract product types;
wenzelm
parents: 11489
diff changeset
   163
  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
10093
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   164
  "_record_type_scheme" :: "[field_types, type] => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   165
  "_record"             :: "fields => 'a"                               ("(3\<lparr>_\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   166
  "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
44584c2b512b more symbolic syntax (currently "input");
wenzelm
parents: 9729
diff changeset
   167
  "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
9729
40cfc3dd27da \<dots> syntax;
wenzelm
parents: 7357
diff changeset
   168
11833
wenzelm
parents: 11826
diff changeset
   169
wenzelm
parents: 11826
diff changeset
   170
subsection {* Package setup *}
wenzelm
parents: 11826
diff changeset
   171
wenzelm
parents: 11826
diff changeset
   172
use "Tools/record_package.ML"
wenzelm
parents: 11826
diff changeset
   173
setup RecordPackage.setup
10641
d1533f63c738 added "_update_name" and parse_translation;
wenzelm
parents: 10331
diff changeset
   174
4870
cc36acb5b114 Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff changeset
   175
end