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 |
|
|
22 |
thm "point.simps"
|
|
23 |
text {*
|
|
24 |
Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
|
|
25 |
Updates, make, make_scheme and equality introduction (extensionality)
|
|
26 |
*}
|
|
27 |
|
|
28 |
thm "point.iffs"
|
|
29 |
text {*
|
|
30 |
@{thm[display] point.iffs}
|
|
31 |
%%\rulename{point.iffs}
|
|
32 |
Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord)
|
|
33 |
*}
|
|
34 |
|
|
35 |
thm "point.update_defs"
|
|
36 |
text {*
|
|
37 |
@{thm[display] point.update_defs}
|
|
38 |
%%\rulename{point.update_defs}
|
|
39 |
Definitions of updates to Xcoord and Ycoord, also "more"
|
|
40 |
*}
|
|
41 |
|
|
42 |
text {*
|
|
43 |
The set of theorems @{thm [source] point.simps} is added
|
|
44 |
automatically to the standard simpset, @{thm [source] point.iffs} is
|
|
45 |
added to the Classical Reasoner and Simplifier context.
|
|
46 |
*}
|
|
47 |
|
|
48 |
text {* Exchanging Xcoord and Ycoord yields a different type: we must
|
|
49 |
unfortunately write the fields in a canonical order.*}
|
|
50 |
|
|
51 |
|
|
52 |
constdefs
|
|
53 |
pt1 :: point
|
|
54 |
"pt1 == (| Xcoord = #999, Ycoord = #23 |)"
|
|
55 |
|
|
56 |
pt2 :: "(| Xcoord :: int, Ycoord :: int |)"
|
|
57 |
"pt2 == (| Xcoord = #-45, Ycoord = #97 |)"
|
|
58 |
|
|
59 |
|
|
60 |
subsubsection {* Some lemmas about records *}
|
|
61 |
|
|
62 |
text {* Basic simplifications. *}
|
|
63 |
|
|
64 |
lemma "point.make a b = (| Xcoord = a, Ycoord = b |)"
|
|
65 |
by simp -- "needed?? forget it"
|
|
66 |
|
|
67 |
lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a"
|
|
68 |
by simp -- "selection"
|
|
69 |
|
|
70 |
lemma "(| Xcoord = a, Ycoord = b |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b |)"
|
|
71 |
by simp -- "update"
|
|
72 |
|
|
73 |
subsection {* Coloured points: record extension *}
|
|
74 |
|
|
75 |
|
|
76 |
text {*
|
|
77 |
Records are extensible.
|
|
78 |
|
|
79 |
The name@{text "more"} is reserved, since it is used for extensibility.
|
|
80 |
*}
|
|
81 |
|
|
82 |
|
|
83 |
datatype colour = Red | Green | Blue
|
|
84 |
|
|
85 |
record cpoint = point +
|
|
86 |
col :: colour
|
|
87 |
|
|
88 |
|
|
89 |
constdefs
|
|
90 |
cpt1 :: cpoint
|
|
91 |
"cpt1 == (| Xcoord = #999, Ycoord = #23, col = Green |)"
|
|
92 |
|
|
93 |
|
|
94 |
subsection {* Generic operations *}
|
|
95 |
|
|
96 |
|
|
97 |
text {* Record selection and record update; these are generic! *}
|
|
98 |
|
|
99 |
lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a"
|
|
100 |
by simp -- "selection"
|
|
101 |
|
|
102 |
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
|
|
103 |
by (simp add: cpt1_def) -- "tail of this record"
|
|
104 |
|
|
105 |
|
|
106 |
lemma "(| Xcoord = a, Ycoord = b, ... = p |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b, ... = p |)"
|
|
107 |
by simp -- "update"
|
|
108 |
|
|
109 |
text {*
|
|
110 |
Record declarations define new type abbreviations:
|
|
111 |
@{text [display]
|
|
112 |
" point = (| Xcoord :: int, Ycoord :: int |)
|
|
113 |
'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
|
|
114 |
Extensions `...' must be in type class @{text more}.
|
|
115 |
*}
|
|
116 |
|
|
117 |
constdefs
|
|
118 |
getX :: "('a::more) point_scheme \<Rightarrow> int"
|
|
119 |
"getX r == Xcoord r"
|
|
120 |
setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"
|
|
121 |
"setX r a == r (| Xcoord := a |)"
|
|
122 |
extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"
|
|
123 |
"extendpt ext == (| Xcoord = #15, Ycoord = 0, ... = ext |)"
|
|
124 |
text{*not sure what this is for!*}
|
|
125 |
|
|
126 |
|
|
127 |
text {*
|
|
128 |
\medskip Concrete records are type instances of record schemes.
|
|
129 |
*}
|
|
130 |
|
|
131 |
lemma "getX (| Xcoord = #64, Ycoord = #36 |) = #64"
|
|
132 |
by (simp add: getX_def)
|
|
133 |
|
|
134 |
|
|
135 |
text {* \medskip Manipulating the `...' (more) part. beware: EACH record
|
|
136 |
has its OWN more field, so a compound name is required! *}
|
|
137 |
|
|
138 |
constdefs
|
|
139 |
incX :: "('a::more) point_scheme \<Rightarrow> 'a point_scheme"
|
|
140 |
"incX r == \<lparr>Xcoord = (Xcoord r) + #1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
|
|
141 |
|
|
142 |
constdefs
|
|
143 |
setGreen :: "[colour, ('a::more) point_scheme] \<Rightarrow> cpoint"
|
|
144 |
"setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)"
|
|
145 |
|
|
146 |
|
|
147 |
text {* works (I think) for ALL extensions of type point? *}
|
|
148 |
|
|
149 |
lemma "incX r = setX r ((getX r) + #1)"
|
|
150 |
by (simp add: getX_def setX_def incX_def)
|
|
151 |
|
|
152 |
text {* An equivalent definition. *}
|
|
153 |
lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + #1\<rparr>"
|
|
154 |
by (simp add: incX_def)
|
|
155 |
|
|
156 |
|
|
157 |
|
|
158 |
text {*
|
|
159 |
Functions on @{text point} schemes work for type @{text cpoint} as
|
|
160 |
well. *}
|
|
161 |
|
|
162 |
lemma "getX \<lparr>Xcoord = #23, Ycoord = #10, col = Blue\<rparr> = #23"
|
|
163 |
by (simp add: getX_def)
|
|
164 |
|
|
165 |
|
|
166 |
subsubsection {* Non-coercive structural subtyping *}
|
|
167 |
|
|
168 |
text {*
|
|
169 |
Function @{term setX} can be applied to type @{typ cpoint}, not just type
|
|
170 |
@{typ point}, and returns a result of the same type! *}
|
|
171 |
|
|
172 |
lemma "setX \<lparr>Xcoord = #12, Ycoord = 0, col = Blue\<rparr> #23 =
|
|
173 |
\<lparr>Xcoord = #23, Ycoord = 0, col = Blue\<rparr>"
|
|
174 |
by (simp add: setX_def)
|
|
175 |
|
|
176 |
|
|
177 |
subsection {* Other features *}
|
|
178 |
|
|
179 |
text {* Field names (and order) contribute to record identity. *}
|
|
180 |
|
|
181 |
|
|
182 |
text {* \medskip Polymorphic records. *}
|
|
183 |
|
|
184 |
record 'a polypoint = point +
|
|
185 |
content :: 'a
|
|
186 |
|
|
187 |
types cpolypoint = "colour polypoint"
|
|
188 |
|
|
189 |
|
|
190 |
subsection {* Equality of records. *}
|
|
191 |
|
|
192 |
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')"
|
|
193 |
-- "simplification of concrete record equality"
|
|
194 |
by simp
|
|
195 |
|
|
196 |
text {* \medskip Surjective pairing *}
|
|
197 |
|
|
198 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
|
|
199 |
by simp
|
|
200 |
|
|
201 |
|
|
202 |
|
|
203 |
lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>"
|
|
204 |
by auto
|
|
205 |
|
|
206 |
text {*
|
|
207 |
A rigid record has ()::unit in its name@{text "more"} part
|
|
208 |
*}
|
|
209 |
|
|
210 |
text {* a polymorphic record equality (covers all possible extensions) *}
|
|
211 |
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
|
|
212 |
-- "introduction of abstract record equality
|
11389
|
213 |
(order of updates doesn't affect the value)"
|
11387
|
214 |
by simp
|
|
215 |
|
|
216 |
lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
|
|
217 |
-- "abstract record equality (the same with iterated updates)"
|
|
218 |
by simp
|
|
219 |
|
|
220 |
text {* Showing that repeated updates don't matter *}
|
|
221 |
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
|
11389
|
222 |
by simp
|
11387
|
223 |
|
|
224 |
|
|
225 |
text {* surjective *}
|
|
226 |
|
|
227 |
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
|
|
228 |
by simp
|
|
229 |
|
|
230 |
|
|
231 |
text {*
|
|
232 |
\medskip Splitting abstract record variables.
|
|
233 |
*}
|
|
234 |
|
|
235 |
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
|
|
236 |
-- "elimination of abstract record equality (manual proof, by selector)"
|
|
237 |
apply (drule_tac f=Xcoord in arg_cong)
|
|
238 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
239 |
by simp
|
|
240 |
|
|
241 |
text {*
|
|
242 |
So we replace the ugly manual proof by splitting. These must be quantified:
|
|
243 |
the @{text "!!r"} is \emph{necessary}! Note the occurrence of more, since
|
|
244 |
r is polymorphic.
|
|
245 |
*}
|
|
246 |
lemma "!!r. r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
|
|
247 |
apply record_split --{* @{subgoals[display,indent=0,margin=65]} *}
|
|
248 |
by simp
|
|
249 |
|
|
250 |
|
|
251 |
end
|