author  haftmann 
Wed, 14 Jul 2010 16:13:14 +0200  
changeset 37826  4c0a5e35931a 
parent 34971  5c290f56ebf7 
child 38012  3ca193a6ae5a 
permissions  rwrr 
10052  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  4 
*) 
5 

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

7 

33596  8 
theory Records 
9 
imports Main Record 

10 
begin 

10052  11 

12 
subsection {* Points *} 

13 

14 
record point = 

11939  15 
xpos :: nat 
16 
ypos :: nat 

10052  17 

18 
text {* 

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

10052  21 
*} 
22 

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

23 

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

12266  26 
thm "point.defs" 
10052  27 

28 
text {* 

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

31 
added to the Classical Reasoner and Simplifier context. 

10052  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  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  37 
*} 
38 

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

10052  41 

42 

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

44 

22737  45 
definition 
46 
foo1 :: point 

47 
where 

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

49 

50 
definition 

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

52 
where 

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

10052  54 

55 

56 
subsubsection {* Record selection and record update *} 

57 

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

59 
getX :: "'a point_scheme => nat" where 
19736  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  64 
"setX r n = r ( xpos := n )" 
10052  65 

66 

67 
subsubsection {* Some lemmas about records *} 

68 

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

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

10052  73 

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

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

80 

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

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

86 

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

90 

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

94 

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

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

10052  100 
thus ?thesis by simp 
101 
qed 

102 

103 

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

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

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

112 

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

10357  116 
*} 
10052  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  119 
proof (cases r) 
120 
fix xpos ypos more 

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

122 
thus ?thesis by simp 

123 
qed 

124 

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

126 
proof (induct r) 

127 
fix xpos ypos more 

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

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

10052  130 
by simp 
131 
qed 

132 

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

135 
fix xpos ypos more 

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

137 
thus ?thesis by simp 

10052  138 
qed 
139 

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

142 
case fields 

143 
thus ?thesis by simp 

144 
qed 

145 

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

147 
by (cases r) simp 

148 

10052  149 

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

152 
*} 

10052  153 

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

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

158 

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

19736  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  163 
"incX r = ( xpos = xpos r + 1, ypos = ypos r, ... = point.more r )" 
10052  164 

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

167 

10052  168 

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

19736  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  173 
"incX' r = r ( xpos := xpos r + 1 )" 
10052  174 

175 

176 
subsection {* Coloured points: record extension *} 

177 

178 
datatype colour = Red  Green  Blue 

179 

180 
record cpoint = point + 

181 
colour :: colour 

182 

183 

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  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  191 
*} 
192 

193 
consts foo6 :: cpoint 

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

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

10052  197 

198 

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

201 
*} 

10052  202 

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

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

207 

208 
subsubsection {* Noncoercive structural subtyping *} 

209 

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

212 
Great! 

213 
*} 

10052  214 

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

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

219 

220 
subsection {* Other features *} 

221 

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

224 
record point' = 

11939  225 
xpos' :: nat 
226 
ypos' :: nat 

10052  227 

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

10357  231 
*} 
10052  232 

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

235 
record 'a point'' = point + 

236 
content :: 'a 

237 

238 
types cpoint'' = "colour point''" 

239 

25707  240 

241 

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

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

244 
by simp 

245 

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

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

248 
by simp 

249 

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

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  254 
only splits the records, whereas the tactic also simplifies the 
255 
resulting goal with the standard record simplification rules. A 

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

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

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

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

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

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  263 
equations for simplification and can also split fixed record variables. 
264 

265 
*} 

266 

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

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  270 
apply simp 
271 
done 

272 

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  275 
apply simp 
276 
done 

277 

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

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  281 
apply simp 
282 
done 

283 

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  286 
apply simp 
287 
done 

288 

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

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  292 
apply auto 
293 
done 

294 

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  297 
apply auto 
298 
done 

299 

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  302 
apply auto 
303 
done 

304 

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  307 
apply auto 
308 
done 

309 

310 

311 
lemma True 

312 
proof  

313 
{ 

26932  314 
fix P r 
25707  315 
assume pre: "P (xpos r)" 
316 
have "\<exists>x. P x" 

317 
using pre 

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  320 
apply auto 
321 
done 

322 
} 

323 
show ?thesis .. 

324 
qed 

325 

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  328 
following lemma. 
329 
*} 

330 

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

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  334 
done 
335 

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  347 
subsection {* Some code generation *} 
348 

37826  349 
export_code foo1 foo3 foo5 foo10 checking SML 
33613  350 

10052  351 
end 