author  haftmann 
Fri, 19 Jun 2009 17:23:21 +0200  
changeset 31723  f5cafe803b55 
parent 31248  d1c65a593daf 
child 33596  27c5023ee818 
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 

16417  8 
theory Records imports Main begin 
10052  9 

10 
subsection {* Points *} 

11 

12 
record point = 

11939  13 
xpos :: nat 
14 
ypos :: nat 

10052  15 

16 
text {* 

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

10052  19 
*} 
20 

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

21 

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

12266  24 
thm "point.defs" 
10052  25 

26 
text {* 

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

29 
added to the Classical Reasoner and Simplifier context. 

10052  30 

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

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

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

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

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

10052  39 

40 

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

42 

22737  43 
definition 
44 
foo1 :: point 

45 
where 

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

47 

48 
definition 

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

50 
where 

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

10052  52 

53 

54 
subsubsection {* Record selection and record update *} 

55 

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

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

59 

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

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

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

64 

65 
subsubsection {* Some lemmas about records *} 

66 

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

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

10052  71 

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

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

78 

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

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

84 

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

88 

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

92 

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

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

10052  98 
thus ?thesis by simp 
99 
qed 

100 

101 

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

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

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

110 

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

10357  114 
*} 
10052  115 

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

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

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

120 
thus ?thesis by simp 

121 
qed 

122 

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

124 
proof (induct r) 

125 
fix xpos ypos more 

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

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

10052  128 
by simp 
129 
qed 

130 

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

133 
fix xpos ypos more 

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

135 
thus ?thesis by simp 

10052  136 
qed 
137 

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

140 
case fields 

141 
thus ?thesis by simp 

142 
qed 

143 

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

145 
by (cases r) simp 

146 

10052  147 

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

150 
*} 

10052  151 

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

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

156 

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

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

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

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

165 

10052  166 

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

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

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

173 

174 
subsection {* Coloured points: record extension *} 

175 

176 
datatype colour = Red  Green  Blue 

177 

178 
record cpoint = point + 

179 
colour :: colour 

180 

181 

182 
text {* 

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

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

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

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

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

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

191 
consts foo6 :: cpoint 

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

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

10052  195 

196 

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

199 
*} 

10052  200 

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

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

205 

206 
subsubsection {* Noncoercive structural subtyping *} 

207 

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

210 
Great! 

211 
*} 

10052  212 

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

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

217 

218 
subsection {* Other features *} 

219 

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

222 
record point' = 

11939  223 
xpos' :: nat 
224 
ypos' :: nat 

10052  225 

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

10357  229 
*} 
10052  230 

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

233 
record 'a point'' = point + 

234 
content :: 'a 

235 

236 
types cpoint'' = "colour point''" 

237 

25707  238 

239 

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

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

242 
by simp 

243 

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

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

246 
by simp 

247 

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

249 
(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

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

251 
"Record.record_split_simp_tac"}. The simplification procedure 
25707  252 
only splits the records, whereas the tactic also simplifies the 
253 
resulting goal with the standard record simplification rules. A 

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

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

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

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

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

259 
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

260 
@{ML [source] "Record.record_split_simp_tac"} additionally takes a list of 
25707  261 
equations for simplification and can also split fixed record variables. 
262 

263 
*} 

264 

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

266 
apply (tactic {* simp_tac 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31248
diff
changeset

267 
(HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) 
25707  268 
apply simp 
269 
done 

270 

271 
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

272 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  273 
apply simp 
274 
done 

275 

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

277 
apply (tactic {* simp_tac 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31248
diff
changeset

278 
(HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) 
25707  279 
apply simp 
280 
done 

281 

282 
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

283 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  284 
apply simp 
285 
done 

286 

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

288 
apply (tactic {* simp_tac 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31248
diff
changeset

289 
(HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) 
25707  290 
apply auto 
291 
done 

292 

293 
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

294 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  295 
apply auto 
296 
done 

297 

298 
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

299 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  300 
apply auto 
301 
done 

302 

303 
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

304 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  305 
apply auto 
306 
done 

307 

308 

309 
lemma True 

310 
proof  

311 
{ 

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

315 
using pre 

316 
apply  

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31248
diff
changeset

317 
apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) 
25707  318 
apply auto 
319 
done 

320 
} 

321 
show ?thesis .. 

322 
qed 

323 

324 
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

325 
"Record.record_ex_sel_eq_simproc"} is illustrated by the 
25707  326 
following lemma. 
327 
*} 

328 

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

330 
apply (tactic {*simp_tac 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31248
diff
changeset

331 
(HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*}) 
25707  332 
done 
333 

334 

10052  335 
end 