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