author  schirmer 
Wed, 19 Dec 2007 16:32:16 +0100  
changeset 25707  0a599404f5a1 
parent 22737  d87ccbcc2702 
child 26932  c398a3866082 
permissions  rwrr 
10052  1 
(* Title: HOL/ex/Records.thy 
2 
ID: $Id$ 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

3 
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

4 
TU Muenchen 
10052  5 
*) 
6 

7 
header {* Using extensible records in HOL  points and coloured points *} 

8 

16417  9 
theory Records imports Main begin 
10052  10 

11 
subsection {* Points *} 

12 

13 
record point = 

11939  14 
xpos :: nat 
15 
ypos :: nat 

10052  16 

17 
text {* 

11939  18 
Apart many other things, above record declaration produces the 
19 
following theorems: 

10052  20 
*} 
21 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

22 

10052  23 
thm "point.simps" 
24 
thm "point.iffs" 

12266  25 
thm "point.defs" 
10052  26 

27 
text {* 

11939  28 
The set of theorems @{thm [source] point.simps} is added 
29 
automatically to the standard simpset, @{thm [source] point.iffs} is 

30 
added to the Classical Reasoner and Simplifier context. 

10052  31 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

32 
\medskip Record declarations define new types and type abbreviations: 
10357  33 
@{text [display] 
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

34 
" 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

35 
'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type"} 
10052  36 
*} 
37 

11939  38 
consts foo2 :: "( xpos :: nat, ypos :: nat )" 
39 
consts foo4 :: "'a => ( xpos :: nat, ypos :: nat, ... :: 'a )" 

10052  40 

41 

42 
subsubsection {* Introducing concrete records and record schemes *} 

43 

22737  44 
definition 
45 
foo1 :: point 

46 
where 

47 
foo1_def: "foo1 = ( xpos = 1, ypos = 0 )" 

48 

49 
definition 

50 
foo3 :: "'a => 'a point_scheme" 

51 
where 

52 
foo3_def: "foo3 ext = ( xpos = 1, ypos = 0, ... = ext )" 

10052  53 

54 

55 
subsubsection {* Record selection and record update *} 

56 

19736  57 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

58 
getX :: "'a point_scheme => nat" where 
19736  59 
"getX r = xpos r" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

60 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

61 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

62 
setX :: "'a point_scheme => nat => 'a point_scheme" where 
19736  63 
"setX r n = r ( xpos := n )" 
10052  64 

65 

66 
subsubsection {* Some lemmas about records *} 

67 

10357  68 
text {* Basic simplifications. *} 
10052  69 

11939  70 
lemma "point.make n p = ( xpos = n, ypos = p )" 
71 
by (simp only: point.make_def) 

10052  72 

11939  73 
lemma "xpos ( xpos = m, ypos = n, ... = p ) = m" 
10052  74 
by simp 
75 

11939  76 
lemma "( xpos = m, ypos = n, ... = p ) ( xpos:= 0 ) = ( xpos = 0, ypos = n, ... = p )" 
10052  77 
by simp 
78 

79 

10357  80 
text {* \medskip Equality of records. *} 
10052  81 

11939  82 
lemma "n = n' ==> p = p' ==> ( xpos = n, ypos = p ) = ( xpos = n', ypos = p' )" 
10052  83 
 "introduction of concrete record equality" 
84 
by simp 

85 

11939  86 
lemma "( xpos = n, ypos = p ) = ( xpos = n', ypos = p' ) ==> n = n'" 
10052  87 
 "elimination of concrete record equality" 
88 
by simp 

89 

11939  90 
lemma "r ( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
10052  91 
 "introduction of abstract record equality" 
92 
by simp 

93 

11939  94 
lemma "r ( xpos := n ) = r ( xpos := n' ) ==> n = n'" 
10052  95 
 "elimination of abstract record equality (manual proof)" 
96 
proof  

11939  97 
assume "r ( xpos := n ) = r ( xpos := n' )" (is "?lhs = ?rhs") 
98 
hence "xpos ?lhs = xpos ?rhs" by simp 

10052  99 
thus ?thesis by simp 
100 
qed 

101 

102 

10357  103 
text {* \medskip Surjective pairing *} 
10052  104 

11939  105 
lemma "r = ( xpos = xpos r, ypos = ypos r )" 
10052  106 
by simp 
107 

12591  108 
lemma "r = ( xpos = xpos r, ypos = ypos r, ... = point.more r )" 
10052  109 
by simp 
110 

111 

10357  112 
text {* 
11939  113 
\medskip Representation of records by cases or (degenerate) 
114 
induction. 

10357  115 
*} 
10052  116 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

117 
lemma "r( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
11939  118 
proof (cases r) 
119 
fix xpos ypos more 

120 
assume "r = ( xpos = xpos, ypos = ypos, ... = more )" 

121 
thus ?thesis by simp 

122 
qed 

123 

124 
lemma "r ( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 

125 
proof (induct r) 

126 
fix xpos ypos more 

127 
show "( xpos = xpos, ypos = ypos, ... = more ) ( xpos := n, ypos := m ) = 

128 
( xpos = xpos, ypos = ypos, ... = more ) ( ypos := m, xpos := n )" 

10052  129 
by simp 
130 
qed 

131 

11939  132 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 
133 
proof (cases r) 

134 
fix xpos ypos more 

135 
assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" 

136 
thus ?thesis by simp 

10052  137 
qed 
138 

11939  139 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 
140 
proof (cases r) 

141 
case fields 

142 
thus ?thesis by simp 

143 
qed 

144 

145 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 

146 
by (cases r) simp 

147 

10052  148 

10357  149 
text {* 
150 
\medskip Concrete records are type instances of record schemes. 

151 
*} 

10052  152 

19736  153 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

154 
foo5 :: nat where 
19736  155 
"foo5 = getX ( xpos = 1, ypos = 0 )" 
10052  156 

157 

11939  158 
text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *} 
10052  159 

19736  160 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

161 
incX :: "'a point_scheme => 'a point_scheme" where 
19736  162 
"incX r = ( xpos = xpos r + 1, ypos = ypos r, ... = point.more r )" 
10052  163 

11939  164 
lemma "incX r = setX r (Suc (getX r))" 
165 
by (simp add: getX_def setX_def incX_def) 

166 

10052  167 

10357  168 
text {* An alternative definition. *} 
10052  169 

19736  170 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

171 
incX' :: "'a point_scheme => 'a point_scheme" where 
19736  172 
"incX' r = r ( xpos := xpos r + 1 )" 
10052  173 

174 

175 
subsection {* Coloured points: record extension *} 

176 

177 
datatype colour = Red  Green  Blue 

178 

179 
record cpoint = point + 

180 
colour :: colour 

181 

182 

183 
text {* 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

184 
The record declaration defines a new type constructure and abbreviations: 
10357  185 
@{text [display] 
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

186 
" cpoint = ( xpos :: nat, ypos :: nat, colour :: colour ) = 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

187 
() cpoint_ext_type point_ext_type 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

188 
'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

189 
'a cpoint_ext_type point_ext_type"} 
10052  190 
*} 
191 

192 
consts foo6 :: cpoint 

11939  193 
consts foo7 :: "( xpos :: nat, ypos :: nat, colour :: colour )" 
194 
consts foo8 :: "'a cpoint_scheme" 

195 
consts foo9 :: "( xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a )" 

10052  196 

197 

10357  198 
text {* 
199 
Functions on @{text point} schemes work for @{text cpoints} as well. 

200 
*} 

10052  201 

19736  202 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

203 
foo10 :: nat where 
19736  204 
"foo10 = getX ( xpos = 2, ypos = 0, colour = Blue )" 
10052  205 

206 

207 
subsubsection {* Noncoercive structural subtyping *} 

208 

10357  209 
text {* 
210 
Term @{term foo11} has type @{typ cpoint}, not type @{typ point}  

211 
Great! 

212 
*} 

10052  213 

19736  214 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset

215 
foo11 :: cpoint where 
19736  216 
"foo11 = setX ( xpos = 2, ypos = 0, colour = Blue ) 0" 
10052  217 

218 

219 
subsection {* Other features *} 

220 

10357  221 
text {* Field names contribute to record identity. *} 
10052  222 

223 
record point' = 

11939  224 
xpos' :: nat 
225 
ypos' :: nat 

10052  226 

10357  227 
text {* 
11939  228 
\noindent May not apply @{term getX} to @{term [source] "( xpos' = 
229 
2, ypos' = 0 )"}  type error. 

10357  230 
*} 
10052  231 

10357  232 
text {* \medskip Polymorphic records. *} 
10052  233 

234 
record 'a point'' = point + 

235 
content :: 'a 

236 

237 
types cpoint'' = "colour point''" 

238 

25707  239 

240 

241 
text {* Updating a record field with an identical value is simplified.*} 

242 
lemma "r ( xpos := xpos r ) = r" 

243 
by simp 

244 

245 
text {* Only the most recent update to a component survives simplification. *} 

246 
lemma "r ( xpos := x, ypos := y, xpos := x' ) = r ( ypos := y, xpos := x' )" 

247 
by simp 

248 

249 
text {* In some cases its convenient to automatically split 

250 
(quantified) records. For this purpose there is the simproc @{ML [source] 

251 
"RecordPackage.record_split_simproc"} and the tactic @{ML [source] 

252 
"RecordPackage.record_split_simp_tac"}. The simplification procedure 

253 
only splits the records, whereas the tactic also simplifies the 

254 
resulting goal with the standard record simplification rules. A 

255 
(generalized) predicate on the record is passed as parameter that 

256 
decides whether or how `deep' to split the record. It can peek on the 

257 
subterm starting at the quantified occurrence of the record (including 

258 
the quantifier). The value @{ML "0"} indicates no split, a value 

259 
greater @{ML "0"} splits up to the given bound of record extension and 

260 
finally the value @{ML "~1"} completely splits the record. 

261 
@{ML [source] "RecordPackage.record_split_simp_tac"} additionally takes a list of 

262 
equations for simplification and can also split fixed record variables. 

263 

264 
*} 

265 

266 
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)" 

267 
apply (tactic {* simp_tac 

268 
(HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*}) 

269 
apply simp 

270 
done 

271 

272 
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)" 

273 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

274 
apply simp 

275 
done 

276 

277 
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)" 

278 
apply (tactic {* simp_tac 

279 
(HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*}) 

280 
apply simp 

281 
done 

282 

283 
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)" 

284 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

285 
apply simp 

286 
done 

287 

288 
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)" 

289 
apply (tactic {* simp_tac 

290 
(HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*}) 

291 
apply auto 

292 
done 

293 

294 
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)" 

295 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

296 
apply auto 

297 
done 

298 

299 
lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)" 

300 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

301 
apply auto 

302 
done 

303 

304 
lemma fixes r shows "P (xpos r) \<Longrightarrow> (\<exists>x. P x)" 

305 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

306 
apply auto 

307 
done 

308 

309 

310 
lemma True 

311 
proof  

312 
{ 

313 
fix r 

314 
assume pre: "P (xpos r)" 

315 
have "\<exists>x. P x" 

316 
using pre 

317 
apply  

318 
apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*}) 

319 
apply auto 

320 
done 

321 
} 

322 
show ?thesis .. 

323 
qed 

324 

325 
text {* The effect of simproc @{ML [source] 

326 
"RecordPackage.record_ex_sel_eq_simproc"} is illustrated by the 

327 
following lemma. 

328 
*} 

329 

330 
lemma "\<exists>r. xpos r = x" 

331 
apply (tactic {*simp_tac 

332 
(HOL_basic_ss addsimprocs [RecordPackage.record_ex_sel_eq_simproc]) 1*}) 

333 
done 

334 

335 

10052  336 
end 