author | paulson |
Tue, 18 Dec 2001 17:15:41 +0100 | |
changeset 12541 | c6e454ec501c |
parent 12409 | 25bf458af885 |
child 12567 | 614ef5ca41ed |
permissions | -rw-r--r-- |
11387 | 1 |
(* Title: HOL/ex/Records.thy |
2 |
ID: $Id$ |
|
3 |
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
*) |
|
6 |
||
7 |
header {* Extensible Records *} |
|
8 |
||
9 |
theory Records = Main: |
|
10 |
||
11 |
subsection {* Points *} |
|
12 |
||
13 |
record point = |
|
14 |
Xcoord :: int |
|
15 |
Ycoord :: int |
|
16 |
||
17 |
text {* |
|
18 |
Apart many other things, above record declaration produces the |
|
19 |
following theorems: |
|
20 |
*} |
|
21 |
||
11428 | 22 |
|
11387 | 23 |
thm "point.simps" |
24 |
text {* |
|
25 |
Incomprehensible equations: the selectors Xcoord and Ycoord, also "more"; |
|
26 |
Updates, make, make_scheme and equality introduction (extensionality) |
|
27 |
*} |
|
28 |
||
29 |
thm "point.iffs" |
|
30 |
text {* |
|
31 |
@{thm[display] point.iffs} |
|
32 |
%%\rulename{point.iffs} |
|
33 |
Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord) |
|
34 |
*} |
|
35 |
||
36 |
thm "point.update_defs" |
|
37 |
text {* |
|
38 |
@{thm[display] point.update_defs} |
|
39 |
%%\rulename{point.update_defs} |
|
40 |
Definitions of updates to Xcoord and Ycoord, also "more" |
|
41 |
*} |
|
42 |
||
43 |
text {* |
|
44 |
The set of theorems @{thm [source] point.simps} is added |
|
45 |
automatically to the standard simpset, @{thm [source] point.iffs} is |
|
46 |
added to the Classical Reasoner and Simplifier context. |
|
47 |
*} |
|
48 |
||
49 |
text {* Exchanging Xcoord and Ycoord yields a different type: we must |
|
50 |
unfortunately write the fields in a canonical order.*} |
|
51 |
||
52 |
||
53 |
constdefs |
|
54 |
pt1 :: point |
|
11711 | 55 |
"pt1 == (| Xcoord = 999, Ycoord = 23 |)" |
11387 | 56 |
|
57 |
pt2 :: "(| Xcoord :: int, Ycoord :: int |)" |
|
11711 | 58 |
"pt2 == (| Xcoord = -45, Ycoord = 97 |)" |
11387 | 59 |
|
60 |
||
61 |
subsubsection {* Some lemmas about records *} |
|
62 |
||
63 |
text {* Basic simplifications. *} |
|
64 |
||
65 |
lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a" |
|
66 |
by simp -- "selection" |
|
67 |
||
68 |
lemma "(| Xcoord = a, Ycoord = b |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b |)" |
|
69 |
by simp -- "update" |
|
70 |
||
12407 | 71 |
|
11387 | 72 |
subsection {* Coloured points: record extension *} |
73 |
||
74 |
||
75 |
text {* |
|
76 |
Records are extensible. |
|
77 |
||
78 |
The name@{text "more"} is reserved, since it is used for extensibility. |
|
79 |
*} |
|
80 |
||
81 |
||
82 |
datatype colour = Red | Green | Blue |
|
83 |
||
84 |
record cpoint = point + |
|
85 |
col :: colour |
|
86 |
||
87 |
||
88 |
constdefs |
|
89 |
cpt1 :: cpoint |
|
11711 | 90 |
"cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)" |
11387 | 91 |
|
92 |
||
93 |
subsection {* Generic operations *} |
|
94 |
||
95 |
||
96 |
text {* Record selection and record update; these are generic! *} |
|
97 |
||
98 |
lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a" |
|
99 |
by simp -- "selection" |
|
100 |
||
101 |
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>" |
|
102 |
by (simp add: cpt1_def) -- "tail of this record" |
|
103 |
||
104 |
||
105 |
lemma "(| Xcoord = a, Ycoord = b, ... = p |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b, ... = p |)" |
|
106 |
by simp -- "update" |
|
107 |
||
108 |
text {* |
|
109 |
Record declarations define new type abbreviations: |
|
110 |
@{text [display] |
|
111 |
" point = (| Xcoord :: int, Ycoord :: int |) |
|
112 |
'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"} |
|
113 |
*} |
|
114 |
||
115 |
constdefs |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
116 |
getX :: "'a point_scheme \<Rightarrow> int" |
11387 | 117 |
"getX r == Xcoord r" |
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
118 |
setX :: "['a point_scheme, int] \<Rightarrow> 'a point_scheme" |
11387 | 119 |
"setX r a == r (| Xcoord := a |)" |
12407 | 120 |
|
11387 | 121 |
|
122 |
||
123 |
text {* |
|
124 |
\medskip Concrete records are type instances of record schemes. |
|
125 |
*} |
|
126 |
||
11711 | 127 |
lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64" |
11387 | 128 |
by (simp add: getX_def) |
129 |
||
130 |
||
131 |
text {* \medskip Manipulating the `...' (more) part. beware: EACH record |
|
132 |
has its OWN more field, so a compound name is required! *} |
|
133 |
||
134 |
constdefs |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
135 |
incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" |
11711 | 136 |
"incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>" |
11387 | 137 |
|
138 |
constdefs |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
139 |
setGreen :: "[colour, 'a point_scheme] \<Rightarrow> cpoint" |
11387 | 140 |
"setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)" |
141 |
||
142 |
||
143 |
text {* works (I think) for ALL extensions of type point? *} |
|
144 |
||
11711 | 145 |
lemma "incX r = setX r ((getX r) + 1)" |
11387 | 146 |
by (simp add: getX_def setX_def incX_def) |
147 |
||
148 |
text {* An equivalent definition. *} |
|
11711 | 149 |
lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>" |
11387 | 150 |
by (simp add: incX_def) |
151 |
||
152 |
||
153 |
||
154 |
text {* |
|
155 |
Functions on @{text point} schemes work for type @{text cpoint} as |
|
156 |
well. *} |
|
157 |
||
11711 | 158 |
lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23" |
11387 | 159 |
by (simp add: getX_def) |
160 |
||
161 |
||
162 |
subsubsection {* Non-coercive structural subtyping *} |
|
163 |
||
164 |
text {* |
|
165 |
Function @{term setX} can be applied to type @{typ cpoint}, not just type |
|
166 |
@{typ point}, and returns a result of the same type! *} |
|
167 |
||
11711 | 168 |
lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 = |
169 |
\<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>" |
|
11387 | 170 |
by (simp add: setX_def) |
171 |
||
172 |
||
173 |
subsection {* Other features *} |
|
174 |
||
175 |
text {* Field names (and order) contribute to record identity. *} |
|
176 |
||
177 |
||
178 |
text {* \medskip Polymorphic records. *} |
|
179 |
||
180 |
record 'a polypoint = point + |
|
181 |
content :: 'a |
|
182 |
||
183 |
types cpolypoint = "colour polypoint" |
|
184 |
||
185 |
||
186 |
subsection {* Equality of records. *} |
|
187 |
||
188 |
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')" |
|
189 |
-- "simplification of concrete record equality" |
|
190 |
by simp |
|
191 |
||
192 |
text {* \medskip Surjective pairing *} |
|
193 |
||
194 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>" |
|
195 |
by simp |
|
196 |
||
197 |
||
198 |
||
199 |
lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>" |
|
200 |
by auto |
|
201 |
||
202 |
text {* |
|
203 |
A rigid record has ()::unit in its name@{text "more"} part |
|
204 |
*} |
|
205 |
||
206 |
text {* a polymorphic record equality (covers all possible extensions) *} |
|
207 |
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>" |
|
208 |
-- "introduction of abstract record equality |
|
11389 | 209 |
(order of updates doesn't affect the value)" |
11387 | 210 |
by simp |
211 |
||
212 |
lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>" |
|
213 |
-- "abstract record equality (the same with iterated updates)" |
|
214 |
by simp |
|
215 |
||
216 |
text {* Showing that repeated updates don't matter *} |
|
217 |
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>" |
|
11389 | 218 |
by simp |
11387 | 219 |
|
220 |
||
221 |
text {* surjective *} |
|
222 |
||
223 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>" |
|
224 |
by simp |
|
225 |
||
226 |
||
227 |
text {* |
|
228 |
\medskip Splitting abstract record variables. |
|
229 |
*} |
|
230 |
||
231 |
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'" |
|
232 |
-- "elimination of abstract record equality (manual proof, by selector)" |
|
233 |
apply (drule_tac f=Xcoord in arg_cong) |
|
234 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
|
235 |
by simp |
|
236 |
||
12409 | 237 |
text {*So we replace the ugly manual proof by the "cases" method.*} |
238 |
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'" |
|
239 |
apply (cases r) |
|
240 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
|
11942
06fac365248d
accomodate some recent changes of record package;
wenzelm
parents:
11711
diff
changeset
|
241 |
by simp |
11387 | 242 |
|
12407 | 243 |
constdefs |
244 |
cpt2 :: cpoint |
|
245 |
"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)" |
|
246 |
||
247 |
text {* |
|
248 |
@{thm[display] point.defs} |
|
249 |
*}; |
|
250 |
||
251 |
text {* |
|
252 |
@{thm[display] cpoint.defs} |
|
253 |
*}; |
|
254 |
||
255 |
text{*cpt2 is the same as cpt1, but defined by extending point pt1*} |
|
256 |
lemma "cpt1 = cpt2" |
|
257 |
apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs) |
|
258 |
--{* @{subgoals[display,indent=0,margin=65]} *} |
|
259 |
by (simp add: pt1_def) |
|
260 |
||
261 |
||
262 |
lemma "point.truncate cpt2 = pt1" |
|
263 |
by (simp add: pt1_def cpt2_def point.defs) |
|
264 |
||
11387 | 265 |
end |