author  kleing 
Sun, 10 Jan 2016 20:13:29 0800  
changeset 62119  b8c973d90ae7 
parent 61933  cf58b5b794b2 
child 67443  3abf6a722518 
permissions  rwrr 
10052  1 
(* Title: HOL/ex/Records.thy 
46231  2 
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

3 
TU Muenchen 
10052  4 
*) 
5 

61343  6 
section \<open>Using extensible records in HOL  points and coloured points\<close> 
10052  7 

33596  8 
theory Records 
46231  9 
imports Main 
33596  10 
begin 
10052  11 

61343  12 
subsection \<open>Points\<close> 
10052  13 

14 
record point = 

11939  15 
xpos :: nat 
16 
ypos :: nat 

10052  17 

61343  18 
text \<open> 
11939  19 
Apart many other things, above record declaration produces the 
20 
following theorems: 

61343  21 
\<close> 
10052  22 

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

23 

46231  24 
thm point.simps 
25 
thm point.iffs 

26 
thm point.defs 

10052  27 

61343  28 
text \<open> 
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] 
61499  35 
\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type 
36 
'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type\<close>} 

61343  37 
\<close> 
10052  38 

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

10052  41 

42 

61343  43 
subsubsection \<open>Introducing concrete records and record schemes\<close> 
10052  44 

46231  45 
definition foo1 :: point 
46 
where "foo1 = ( xpos = 1, ypos = 0 )" 

22737  47 

46231  48 
definition foo3 :: "'a => 'a point_scheme" 
49 
where "foo3 ext = ( xpos = 1, ypos = 0, ... = ext )" 

10052  50 

51 

61343  52 
subsubsection \<open>Record selection and record update\<close> 
10052  53 

46231  54 
definition getX :: "'a point_scheme => nat" 
55 
where "getX r = xpos r" 

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

56 

46231  57 
definition setX :: "'a point_scheme => nat => 'a point_scheme" 
58 
where "setX r n = r ( xpos := n )" 

10052  59 

60 

61343  61 
subsubsection \<open>Some lemmas about records\<close> 
10052  62 

61343  63 
text \<open>Basic simplifications.\<close> 
10052  64 

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

10052  67 

11939  68 
lemma "xpos ( xpos = m, ypos = n, ... = p ) = m" 
10052  69 
by simp 
70 

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

74 

61343  75 
text \<open>\medskip Equality of records.\<close> 
10052  76 

11939  77 
lemma "n = n' ==> p = p' ==> ( xpos = n, ypos = p ) = ( xpos = n', ypos = p' )" 
61933  78 
\<comment> "introduction of concrete record equality" 
10052  79 
by simp 
80 

11939  81 
lemma "( xpos = n, ypos = p ) = ( xpos = n', ypos = p' ) ==> n = n'" 
61933  82 
\<comment> "elimination of concrete record equality" 
10052  83 
by simp 
84 

11939  85 
lemma "r ( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
61933  86 
\<comment> "introduction of abstract record equality" 
10052  87 
by simp 
88 

11939  89 
lemma "r ( xpos := n ) = r ( xpos := n' ) ==> n = n'" 
61933  90 
\<comment> "elimination of abstract record equality (manual proof)" 
10052  91 
proof  
11939  92 
assume "r ( xpos := n ) = r ( xpos := n' )" (is "?lhs = ?rhs") 
46231  93 
then have "xpos ?lhs = xpos ?rhs" by simp 
94 
then show ?thesis by simp 

10052  95 
qed 
96 

97 

61343  98 
text \<open>\medskip Surjective pairing\<close> 
10052  99 

11939  100 
lemma "r = ( xpos = xpos r, ypos = ypos r )" 
10052  101 
by simp 
102 

12591  103 
lemma "r = ( xpos = xpos r, ypos = ypos r, ... = point.more r )" 
10052  104 
by simp 
105 

106 

61343  107 
text \<open> 
11939  108 
\medskip Representation of records by cases or (degenerate) 
109 
induction. 

61343  110 
\<close> 
10052  111 

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

112 
lemma "r( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
11939  113 
proof (cases r) 
114 
fix xpos ypos more 

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

46231  116 
then show ?thesis by simp 
11939  117 
qed 
118 

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

120 
proof (induct r) 

121 
fix xpos ypos more 

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

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

10052  124 
by simp 
125 
qed 

126 

11939  127 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 
128 
proof (cases r) 

129 
fix xpos ypos more 

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

46231  131 
then show ?thesis by simp 
10052  132 
qed 
133 

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

136 
case fields 

46231  137 
then show ?thesis by simp 
11939  138 
qed 
139 

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

141 
by (cases r) simp 

142 

10052  143 

61343  144 
text \<open> 
10357  145 
\medskip Concrete records are type instances of record schemes. 
61343  146 
\<close> 
10052  147 

46231  148 
definition foo5 :: nat 
149 
where "foo5 = getX ( xpos = 1, ypos = 0 )" 

10052  150 

151 

61933  152 
text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close> 
10052  153 

46231  154 
definition incX :: "'a point_scheme => 'a point_scheme" 
155 
where "incX r = ( xpos = xpos r + 1, ypos = ypos r, ... = point.more r )" 

10052  156 

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

159 

10052  160 

61343  161 
text \<open>An alternative definition.\<close> 
10052  162 

46231  163 
definition incX' :: "'a point_scheme => 'a point_scheme" 
164 
where "incX' r = r ( xpos := xpos r + 1 )" 

10052  165 

166 

61343  167 
subsection \<open>Coloured points: record extension\<close> 
10052  168 

58310  169 
datatype colour = Red  Green  Blue 
10052  170 

171 
record cpoint = point + 

172 
colour :: colour 

173 

174 

61343  175 
text \<open> 
61499  176 
The record declaration defines a new type constructor and abbreviations: 
10357  177 
@{text [display] 
61499  178 
\<open>cpoint = ( xpos :: nat, ypos :: nat, colour :: colour ) = 
179 
() cpoint_ext_type point_ext_type 

180 
'a cpoint_scheme = ( xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a ) = 

181 
'a cpoint_ext_type point_ext_type\<close>} 

61343  182 
\<close> 
10052  183 

184 
consts foo6 :: cpoint 

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

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

10052  188 

189 

61343  190 
text \<open> 
61933  191 
Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well. 
61343  192 
\<close> 
10052  193 

46231  194 
definition foo10 :: nat 
195 
where "foo10 = getX ( xpos = 2, ypos = 0, colour = Blue )" 

10052  196 

197 

61343  198 
subsubsection \<open>Noncoercive structural subtyping\<close> 
10052  199 

61343  200 
text \<open> 
10357  201 
Term @{term foo11} has type @{typ cpoint}, not type @{typ point}  
202 
Great! 

61343  203 
\<close> 
10052  204 

46231  205 
definition foo11 :: cpoint 
206 
where "foo11 = setX ( xpos = 2, ypos = 0, colour = Blue ) 0" 

10052  207 

208 

61343  209 
subsection \<open>Other features\<close> 
10052  210 

61343  211 
text \<open>Field names contribute to record identity.\<close> 
10052  212 

213 
record point' = 

11939  214 
xpos' :: nat 
215 
ypos' :: nat 

10052  216 

61343  217 
text \<open> 
11939  218 
\noindent May not apply @{term getX} to @{term [source] "( xpos' = 
219 
2, ypos' = 0 )"}  type error. 

61343  220 
\<close> 
10052  221 

61343  222 
text \<open>\medskip Polymorphic records.\<close> 
10052  223 

224 
record 'a point'' = point + 

225 
content :: 'a 

226 

42463  227 
type_synonym cpoint'' = "colour point''" 
10052  228 

25707  229 

230 

61343  231 
text \<open>Updating a record field with an identical value is simplified.\<close> 
25707  232 
lemma "r ( xpos := xpos r ) = r" 
233 
by simp 

234 

61343  235 
text \<open>Only the most recent update to a component survives simplification.\<close> 
25707  236 
lemma "r ( xpos := x, ypos := y, xpos := x' ) = r ( ypos := y, xpos := x' )" 
237 
by simp 

238 

61343  239 
text \<open>In some cases its convenient to automatically split 
25707  240 
(quantified) records. For this purpose there is the simproc @{ML [source] 
38012
3ca193a6ae5a
delete structure Basic_Record; avoid `record` in names in structure Record
haftmann
parents:
37826
diff
changeset

241 
"Record.split_simproc"} and the tactic @{ML [source] 
3ca193a6ae5a
delete structure Basic_Record; avoid `record` in names in structure Record
haftmann
parents:
37826
diff
changeset

242 
"Record.split_simp_tac"}. The simplification procedure 
25707  243 
only splits the records, whereas the tactic also simplifies the 
244 
resulting goal with the standard record simplification rules. A 

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

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

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

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

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

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

38012
3ca193a6ae5a
delete structure Basic_Record; avoid `record` in names in structure Record
haftmann
parents:
37826
diff
changeset

251 
@{ML [source] "Record.split_simp_tac"} additionally takes a list of 
25707  252 
equations for simplification and can also split fixed record variables. 
253 

61343  254 
\<close> 
25707  255 

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

61343  257 
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} 
258 
addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) 

25707  259 
apply simp 
260 
done 

261 

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

61343  263 
apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) 
25707  264 
apply simp 
265 
done 

266 

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

61343  268 
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} 
269 
addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) 

25707  270 
apply simp 
271 
done 

272 

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

61343  274 
apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) 
25707  275 
apply simp 
276 
done 

277 

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

61343  279 
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} 
280 
addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) 

25707  281 
apply auto 
282 
done 

283 

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

61343  285 
apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) 
25707  286 
apply auto 
287 
done 

288 

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

61343  290 
apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) 
25707  291 
apply auto 
292 
done 

293 

294 
lemma True 

295 
proof  

296 
{ 

26932  297 
fix P r 
25707  298 
assume pre: "P (xpos r)" 
46231  299 
then have "\<exists>x. P x" 
25707  300 
apply  
61343  301 
apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>) 
46231  302 
apply auto 
25707  303 
done 
304 
} 

305 
show ?thesis .. 

306 
qed 

307 

61343  308 
text \<open>The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is 
309 
illustrated by the following lemma.\<close> 

25707  310 

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

61343  312 
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss @{context} 
313 
addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>) 

25707  314 
done 
315 

316 

61343  317 
subsection \<open>A more complex record expression\<close> 
34971
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

318 

5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

319 
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

320 
bar2 :: 'b 
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

321 
bar3 :: 'c 
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

322 
bar21 :: "'b \<times> 'a" 
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

323 
bar32 :: "'c \<times> 'b" 
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

324 
bar31 :: "'c \<times> 'a" 
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

325 

62119  326 
print_record "('a,'b,'c) bar" 
34971
5c290f56ebf7
a more complex record expression  cf. src/HOL/Tools/quickcheck_generators.ML
haftmann
parents:
33613
diff
changeset

327 

61343  328 
subsection \<open>Some code generation\<close> 
33613  329 

37826  330 
export_code foo1 foo3 foo5 foo10 checking SML 
33613  331 

61343  332 
text \<open> 
47842
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

333 
Code generation can also be switched off, for instance for very large records 
61343  334 
\<close> 
47842
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

335 

bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

336 
declare [[record_codegen = false]] 
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

337 

bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

338 
record not_so_large_record = 
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

339 
bar520 :: nat 
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

340 
bar521 :: "nat * nat" 
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

341 

bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

342 
declare [[record_codegen = true]] 
bfc08ce7b7b9
provide [[record_codegen]] option for skipping codegen setup for records
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
46231
diff
changeset

343 

10052  344 
end 