src/HOL/ex/Records.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 42463 f270e3e18be5
child 46231 76e32c39dd43
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
wenzelm@10052
     1
(*  Title:      HOL/ex/Records.thy
schirmer@14700
     2
    Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
schirmer@14700
     3
                TU Muenchen
wenzelm@10052
     4
*)
wenzelm@10052
     5
wenzelm@10052
     6
header {* Using extensible records in HOL -- points and coloured points *}
wenzelm@10052
     7
haftmann@33596
     8
theory Records
haftmann@33596
     9
imports Main Record
haftmann@33596
    10
begin
wenzelm@10052
    11
wenzelm@10052
    12
subsection {* Points *}
wenzelm@10052
    13
wenzelm@10052
    14
record point =
wenzelm@11939
    15
  xpos :: nat
wenzelm@11939
    16
  ypos :: nat
wenzelm@10052
    17
wenzelm@10052
    18
text {*
wenzelm@11939
    19
  Apart many other things, above record declaration produces the
wenzelm@11939
    20
  following theorems:
wenzelm@10052
    21
*}
wenzelm@10052
    22
schirmer@14700
    23
wenzelm@10052
    24
thm "point.simps"
wenzelm@10052
    25
thm "point.iffs"
wenzelm@12266
    26
thm "point.defs"
wenzelm@10052
    27
wenzelm@10052
    28
text {*
wenzelm@11939
    29
  The set of theorems @{thm [source] point.simps} is added
wenzelm@11939
    30
  automatically to the standard simpset, @{thm [source] point.iffs} is
wenzelm@11939
    31
  added to the Classical Reasoner and Simplifier context.
wenzelm@10052
    32
schirmer@14700
    33
  \medskip Record declarations define new types and type abbreviations:
wenzelm@10357
    34
  @{text [display]
schirmer@14700
    35
"  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
schirmer@14700
    36
  'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
wenzelm@10052
    37
*}
wenzelm@10052
    38
wenzelm@11939
    39
consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
wenzelm@11939
    40
consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
wenzelm@10052
    41
wenzelm@10052
    42
wenzelm@10052
    43
subsubsection {* Introducing concrete records and record schemes *}
wenzelm@10052
    44
haftmann@22737
    45
definition
haftmann@22737
    46
  foo1 :: point
haftmann@22737
    47
where
haftmann@22737
    48
  foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)"
haftmann@22737
    49
haftmann@22737
    50
definition
haftmann@22737
    51
  foo3 :: "'a => 'a point_scheme"
haftmann@22737
    52
where
haftmann@22737
    53
  foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
wenzelm@10052
    54
wenzelm@10052
    55
wenzelm@10052
    56
subsubsection {* Record selection and record update *}
wenzelm@10052
    57
wenzelm@19736
    58
definition
wenzelm@21404
    59
  getX :: "'a point_scheme => nat" where
wenzelm@19736
    60
  "getX r = xpos r"
wenzelm@21404
    61
wenzelm@21404
    62
definition
wenzelm@21404
    63
  setX :: "'a point_scheme => nat => 'a point_scheme" where
wenzelm@19736
    64
  "setX r n = r (| xpos := n |)"
wenzelm@10052
    65
wenzelm@10052
    66
wenzelm@10052
    67
subsubsection {* Some lemmas about records *}
wenzelm@10052
    68
wenzelm@10357
    69
text {* Basic simplifications. *}
wenzelm@10052
    70
wenzelm@11939
    71
lemma "point.make n p = (| xpos = n, ypos = p |)"
wenzelm@11939
    72
  by (simp only: point.make_def)
wenzelm@10052
    73
wenzelm@11939
    74
lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
wenzelm@10052
    75
  by simp
wenzelm@10052
    76
wenzelm@11939
    77
lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
wenzelm@10052
    78
  by simp
wenzelm@10052
    79
wenzelm@10052
    80
wenzelm@10357
    81
text {* \medskip Equality of records. *}
wenzelm@10052
    82
wenzelm@11939
    83
lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
wenzelm@10052
    84
  -- "introduction of concrete record equality"
wenzelm@10052
    85
  by simp
wenzelm@10052
    86
wenzelm@11939
    87
lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
wenzelm@10052
    88
  -- "elimination of concrete record equality"
wenzelm@10052
    89
  by simp
wenzelm@10052
    90
wenzelm@11939
    91
lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
wenzelm@10052
    92
  -- "introduction of abstract record equality"
wenzelm@10052
    93
  by simp
wenzelm@10052
    94
wenzelm@11939
    95
lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
wenzelm@10052
    96
  -- "elimination of abstract record equality (manual proof)"
wenzelm@10052
    97
proof -
wenzelm@11939
    98
  assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
wenzelm@11939
    99
  hence "xpos ?lhs = xpos ?rhs" by simp
wenzelm@10052
   100
  thus ?thesis by simp
wenzelm@10052
   101
qed
wenzelm@10052
   102
wenzelm@10052
   103
wenzelm@10357
   104
text {* \medskip Surjective pairing *}
wenzelm@10052
   105
wenzelm@11939
   106
lemma "r = (| xpos = xpos r, ypos = ypos r |)"
wenzelm@10052
   107
  by simp
wenzelm@10052
   108
wenzelm@12591
   109
lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
wenzelm@10052
   110
  by simp
wenzelm@10052
   111
wenzelm@10052
   112
wenzelm@10357
   113
text {*
wenzelm@11939
   114
  \medskip Representation of records by cases or (degenerate)
wenzelm@11939
   115
  induction.
wenzelm@10357
   116
*}
wenzelm@10052
   117
schirmer@14700
   118
lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
wenzelm@11939
   119
proof (cases r)
wenzelm@11939
   120
  fix xpos ypos more
wenzelm@11939
   121
  assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
wenzelm@11939
   122
  thus ?thesis by simp
wenzelm@11939
   123
qed
wenzelm@11939
   124
wenzelm@11939
   125
lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
wenzelm@11939
   126
proof (induct r)
wenzelm@11939
   127
  fix xpos ypos more
wenzelm@11939
   128
  show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
wenzelm@11939
   129
      (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
wenzelm@10052
   130
    by simp
wenzelm@10052
   131
qed
wenzelm@10052
   132
wenzelm@11939
   133
lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
wenzelm@11939
   134
proof (cases r)
wenzelm@11939
   135
  fix xpos ypos more
wenzelm@11939
   136
  assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
wenzelm@11939
   137
  thus ?thesis by simp
wenzelm@10052
   138
qed
wenzelm@10052
   139
wenzelm@11939
   140
lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
wenzelm@11939
   141
proof (cases r)
wenzelm@11939
   142
  case fields
wenzelm@11939
   143
  thus ?thesis by simp
wenzelm@11939
   144
qed
wenzelm@11939
   145
wenzelm@11939
   146
lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
wenzelm@11939
   147
  by (cases r) simp
wenzelm@11939
   148
wenzelm@10052
   149
wenzelm@10357
   150
text {*
wenzelm@10357
   151
 \medskip Concrete records are type instances of record schemes.
wenzelm@10357
   152
*}
wenzelm@10052
   153
wenzelm@19736
   154
definition
wenzelm@21404
   155
  foo5 :: nat where
wenzelm@19736
   156
  "foo5 = getX (| xpos = 1, ypos = 0 |)"
wenzelm@10052
   157
wenzelm@10052
   158
wenzelm@11939
   159
text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
wenzelm@10052
   160
wenzelm@19736
   161
definition
wenzelm@21404
   162
  incX :: "'a point_scheme => 'a point_scheme" where
wenzelm@19736
   163
  "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
wenzelm@10052
   164
wenzelm@11939
   165
lemma "incX r = setX r (Suc (getX r))"
wenzelm@11939
   166
  by (simp add: getX_def setX_def incX_def)
wenzelm@11939
   167
wenzelm@10052
   168
wenzelm@10357
   169
text {* An alternative definition. *}
wenzelm@10052
   170
wenzelm@19736
   171
definition
wenzelm@21404
   172
  incX' :: "'a point_scheme => 'a point_scheme" where
wenzelm@19736
   173
  "incX' r = r (| xpos := xpos r + 1 |)"
wenzelm@10052
   174
wenzelm@10052
   175
wenzelm@10052
   176
subsection {* Coloured points: record extension *}
wenzelm@10052
   177
wenzelm@10052
   178
datatype colour = Red | Green | Blue
wenzelm@10052
   179
wenzelm@10052
   180
record cpoint = point +
wenzelm@10052
   181
  colour :: colour
wenzelm@10052
   182
wenzelm@10052
   183
wenzelm@10052
   184
text {*
schirmer@14700
   185
  The record declaration defines a new type constructure and abbreviations:
wenzelm@10357
   186
  @{text [display]
schirmer@14700
   187
"  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
schirmer@14700
   188
     () cpoint_ext_type point_ext_type
schirmer@14700
   189
   'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
schirmer@14700
   190
     'a cpoint_ext_type point_ext_type"}
wenzelm@10052
   191
*}
wenzelm@10052
   192
wenzelm@10052
   193
consts foo6 :: cpoint
wenzelm@11939
   194
consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
wenzelm@11939
   195
consts foo8 :: "'a cpoint_scheme"
wenzelm@11939
   196
consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
wenzelm@10052
   197
wenzelm@10052
   198
wenzelm@10357
   199
text {*
wenzelm@10357
   200
 Functions on @{text point} schemes work for @{text cpoints} as well.
wenzelm@10357
   201
*}
wenzelm@10052
   202
wenzelm@19736
   203
definition
wenzelm@21404
   204
  foo10 :: nat where
wenzelm@19736
   205
  "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
wenzelm@10052
   206
wenzelm@10052
   207
wenzelm@10052
   208
subsubsection {* Non-coercive structural subtyping *}
wenzelm@10052
   209
wenzelm@10357
   210
text {*
wenzelm@10357
   211
 Term @{term foo11} has type @{typ cpoint}, not type @{typ point} ---
wenzelm@10357
   212
 Great!
wenzelm@10357
   213
*}
wenzelm@10052
   214
wenzelm@19736
   215
definition
wenzelm@21404
   216
  foo11 :: cpoint where
wenzelm@19736
   217
  "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
wenzelm@10052
   218
wenzelm@10052
   219
wenzelm@10052
   220
subsection {* Other features *}
wenzelm@10052
   221
wenzelm@10357
   222
text {* Field names contribute to record identity. *}
wenzelm@10052
   223
wenzelm@10052
   224
record point' =
wenzelm@11939
   225
  xpos' :: nat
wenzelm@11939
   226
  ypos' :: nat
wenzelm@10052
   227
wenzelm@10357
   228
text {*
wenzelm@11939
   229
  \noindent May not apply @{term getX} to @{term [source] "(| xpos' =
wenzelm@11939
   230
  2, ypos' = 0 |)"} -- type error.
wenzelm@10357
   231
*}
wenzelm@10052
   232
wenzelm@10357
   233
text {* \medskip Polymorphic records. *}
wenzelm@10052
   234
wenzelm@10052
   235
record 'a point'' = point +
wenzelm@10052
   236
  content :: 'a
wenzelm@10052
   237
wenzelm@42463
   238
type_synonym cpoint'' = "colour point''"
wenzelm@10052
   239
schirmer@25707
   240
schirmer@25707
   241
schirmer@25707
   242
text {* Updating a record field with an identical value is simplified.*}
schirmer@25707
   243
lemma "r (| xpos := xpos r |) = r"
schirmer@25707
   244
  by simp
schirmer@25707
   245
schirmer@25707
   246
text {* Only the most recent update to a component survives simplification. *}
schirmer@25707
   247
lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
schirmer@25707
   248
  by simp
schirmer@25707
   249
schirmer@25707
   250
text {* In some cases its convenient to automatically split
schirmer@25707
   251
(quantified) records. For this purpose there is the simproc @{ML [source]
haftmann@38012
   252
"Record.split_simproc"} and the tactic @{ML [source]
haftmann@38012
   253
"Record.split_simp_tac"}.  The simplification procedure
schirmer@25707
   254
only splits the records, whereas the tactic also simplifies the
schirmer@25707
   255
resulting goal with the standard record simplification rules. A
schirmer@25707
   256
(generalized) predicate on the record is passed as parameter that
schirmer@25707
   257
decides whether or how `deep' to split the record. It can peek on the
schirmer@25707
   258
subterm starting at the quantified occurrence of the record (including
schirmer@25707
   259
the quantifier). The value @{ML "0"} indicates no split, a value
schirmer@25707
   260
greater @{ML "0"} splits up to the given bound of record extension and
schirmer@25707
   261
finally the value @{ML "~1"} completely splits the record.
haftmann@38012
   262
@{ML [source] "Record.split_simp_tac"} additionally takes a list of
schirmer@25707
   263
equations for simplification and can also split fixed record variables.
schirmer@25707
   264
schirmer@25707
   265
*}
schirmer@25707
   266
schirmer@25707
   267
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
schirmer@25707
   268
  apply (tactic {* simp_tac
haftmann@38012
   269
          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
schirmer@25707
   270
  apply simp
schirmer@25707
   271
  done
schirmer@25707
   272
schirmer@25707
   273
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
haftmann@38012
   274
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   275
  apply simp
schirmer@25707
   276
  done
schirmer@25707
   277
schirmer@25707
   278
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
schirmer@25707
   279
  apply (tactic {* simp_tac
haftmann@38012
   280
          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
schirmer@25707
   281
  apply simp
schirmer@25707
   282
  done
schirmer@25707
   283
schirmer@25707
   284
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
haftmann@38012
   285
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   286
  apply simp
schirmer@25707
   287
  done
schirmer@25707
   288
schirmer@25707
   289
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
schirmer@25707
   290
  apply (tactic {* simp_tac
haftmann@38012
   291
          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
schirmer@25707
   292
  apply auto
schirmer@25707
   293
  done
schirmer@25707
   294
schirmer@25707
   295
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
haftmann@38012
   296
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   297
  apply auto
schirmer@25707
   298
  done
schirmer@25707
   299
schirmer@25707
   300
lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
haftmann@38012
   301
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   302
  apply auto
schirmer@25707
   303
  done
schirmer@25707
   304
schirmer@25707
   305
lemma fixes r shows "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
haftmann@38012
   306
  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   307
  apply auto
schirmer@25707
   308
  done
schirmer@25707
   309
schirmer@25707
   310
schirmer@25707
   311
lemma True
schirmer@25707
   312
proof -
schirmer@25707
   313
  {
wenzelm@26932
   314
    fix P r
schirmer@25707
   315
    assume pre: "P (xpos r)"
schirmer@25707
   316
    have "\<exists>x. P x"
schirmer@25707
   317
      using pre
schirmer@25707
   318
      apply -
haftmann@38012
   319
      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
schirmer@25707
   320
      apply auto 
schirmer@25707
   321
      done
schirmer@25707
   322
  }
schirmer@25707
   323
  show ?thesis ..
schirmer@25707
   324
qed
schirmer@25707
   325
schirmer@25707
   326
text {* The effect of simproc @{ML [source]
haftmann@38012
   327
"Record.ex_sel_eq_simproc"} is illustrated by the
schirmer@25707
   328
following lemma.  
schirmer@25707
   329
*}
schirmer@25707
   330
schirmer@25707
   331
lemma "\<exists>r. xpos r = x"
schirmer@25707
   332
  apply (tactic {*simp_tac 
haftmann@38012
   333
           (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
schirmer@25707
   334
  done
schirmer@25707
   335
schirmer@25707
   336
haftmann@34971
   337
subsection {* A more complex record expression *}
haftmann@34971
   338
haftmann@34971
   339
record ('a, 'b, 'c) bar = bar1 :: 'a
haftmann@34971
   340
  bar2 :: 'b
haftmann@34971
   341
  bar3 :: 'c
haftmann@34971
   342
  bar21 :: "'b \<times> 'a"
haftmann@34971
   343
  bar32 :: "'c \<times> 'b"
haftmann@34971
   344
  bar31 :: "'c \<times> 'a"
haftmann@34971
   345
haftmann@34971
   346
haftmann@33613
   347
subsection {* Some code generation *}
haftmann@33613
   348
haftmann@37826
   349
export_code foo1 foo3 foo5 foo10 checking SML
haftmann@33613
   350
wenzelm@10052
   351
end