|
1 (* Title: Admin/Benchmarks/HOL-record/Record_Benchmark.thy |
|
2 Author: Norbert Schirmer, DFKI |
|
3 *) |
|
4 |
|
5 header {* Benchmark for large record *} |
|
6 |
|
7 theory Record_Benchmark |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 declare [[record_timing]] |
|
12 |
|
13 record many_A = |
|
14 A000::nat |
|
15 A001::nat |
|
16 A002::nat |
|
17 A003::nat |
|
18 A004::nat |
|
19 A005::nat |
|
20 A006::nat |
|
21 A007::nat |
|
22 A008::nat |
|
23 A009::nat |
|
24 A010::nat |
|
25 A011::nat |
|
26 A012::nat |
|
27 A013::nat |
|
28 A014::nat |
|
29 A015::nat |
|
30 A016::nat |
|
31 A017::nat |
|
32 A018::nat |
|
33 A019::nat |
|
34 A020::nat |
|
35 A021::nat |
|
36 A022::nat |
|
37 A023::nat |
|
38 A024::nat |
|
39 A025::nat |
|
40 A026::nat |
|
41 A027::nat |
|
42 A028::nat |
|
43 A029::nat |
|
44 A030::nat |
|
45 A031::nat |
|
46 A032::nat |
|
47 A033::nat |
|
48 A034::nat |
|
49 A035::nat |
|
50 A036::nat |
|
51 A037::nat |
|
52 A038::nat |
|
53 A039::nat |
|
54 A040::nat |
|
55 A041::nat |
|
56 A042::nat |
|
57 A043::nat |
|
58 A044::nat |
|
59 A045::nat |
|
60 A046::nat |
|
61 A047::nat |
|
62 A048::nat |
|
63 A049::nat |
|
64 A050::nat |
|
65 A051::nat |
|
66 A052::nat |
|
67 A053::nat |
|
68 A054::nat |
|
69 A055::nat |
|
70 A056::nat |
|
71 A057::nat |
|
72 A058::nat |
|
73 A059::nat |
|
74 A060::nat |
|
75 A061::nat |
|
76 A062::nat |
|
77 A063::nat |
|
78 A064::nat |
|
79 A065::nat |
|
80 A066::nat |
|
81 A067::nat |
|
82 A068::nat |
|
83 A069::nat |
|
84 A070::nat |
|
85 A071::nat |
|
86 A072::nat |
|
87 A073::nat |
|
88 A074::nat |
|
89 A075::nat |
|
90 A076::nat |
|
91 A077::nat |
|
92 A078::nat |
|
93 A079::nat |
|
94 A080::nat |
|
95 A081::nat |
|
96 A082::nat |
|
97 A083::nat |
|
98 A084::nat |
|
99 A085::nat |
|
100 A086::nat |
|
101 A087::nat |
|
102 A088::nat |
|
103 A089::nat |
|
104 A090::nat |
|
105 A091::nat |
|
106 A092::nat |
|
107 A093::nat |
|
108 A094::nat |
|
109 A095::nat |
|
110 A096::nat |
|
111 A097::nat |
|
112 A098::nat |
|
113 A099::nat |
|
114 A100::nat |
|
115 A101::nat |
|
116 A102::nat |
|
117 A103::nat |
|
118 A104::nat |
|
119 A105::nat |
|
120 A106::nat |
|
121 A107::nat |
|
122 A108::nat |
|
123 A109::nat |
|
124 A110::nat |
|
125 A111::nat |
|
126 A112::nat |
|
127 A113::nat |
|
128 A114::nat |
|
129 A115::nat |
|
130 A116::nat |
|
131 A117::nat |
|
132 A118::nat |
|
133 A119::nat |
|
134 A120::nat |
|
135 A121::nat |
|
136 A122::nat |
|
137 A123::nat |
|
138 A124::nat |
|
139 A125::nat |
|
140 A126::nat |
|
141 A127::nat |
|
142 A128::nat |
|
143 A129::nat |
|
144 A130::nat |
|
145 A131::nat |
|
146 A132::nat |
|
147 A133::nat |
|
148 A134::nat |
|
149 A135::nat |
|
150 A136::nat |
|
151 A137::nat |
|
152 A138::nat |
|
153 A139::nat |
|
154 A140::nat |
|
155 A141::nat |
|
156 A142::nat |
|
157 A143::nat |
|
158 A144::nat |
|
159 A145::nat |
|
160 A146::nat |
|
161 A147::nat |
|
162 A148::nat |
|
163 A149::nat |
|
164 A150::nat |
|
165 A151::nat |
|
166 A152::nat |
|
167 A153::nat |
|
168 A154::nat |
|
169 A155::nat |
|
170 A156::nat |
|
171 A157::nat |
|
172 A158::nat |
|
173 A159::nat |
|
174 A160::nat |
|
175 A161::nat |
|
176 A162::nat |
|
177 A163::nat |
|
178 A164::nat |
|
179 A165::nat |
|
180 A166::nat |
|
181 A167::nat |
|
182 A168::nat |
|
183 A169::nat |
|
184 A170::nat |
|
185 A171::nat |
|
186 A172::nat |
|
187 A173::nat |
|
188 A174::nat |
|
189 A175::nat |
|
190 A176::nat |
|
191 A177::nat |
|
192 A178::nat |
|
193 A179::nat |
|
194 A180::nat |
|
195 A181::nat |
|
196 A182::nat |
|
197 A183::nat |
|
198 A184::nat |
|
199 A185::nat |
|
200 A186::nat |
|
201 A187::nat |
|
202 A188::nat |
|
203 A189::nat |
|
204 A190::nat |
|
205 A191::nat |
|
206 A192::nat |
|
207 A193::nat |
|
208 A194::nat |
|
209 A195::nat |
|
210 A196::nat |
|
211 A197::nat |
|
212 A198::nat |
|
213 A199::nat |
|
214 A200::nat |
|
215 A201::nat |
|
216 A202::nat |
|
217 A203::nat |
|
218 A204::nat |
|
219 A205::nat |
|
220 A206::nat |
|
221 A207::nat |
|
222 A208::nat |
|
223 A209::nat |
|
224 A210::nat |
|
225 A211::nat |
|
226 A212::nat |
|
227 A213::nat |
|
228 A214::nat |
|
229 A215::nat |
|
230 A216::nat |
|
231 A217::nat |
|
232 A218::nat |
|
233 A219::nat |
|
234 A220::nat |
|
235 A221::nat |
|
236 A222::nat |
|
237 A223::nat |
|
238 A224::nat |
|
239 A225::nat |
|
240 A226::nat |
|
241 A227::nat |
|
242 A228::nat |
|
243 A229::nat |
|
244 A230::nat |
|
245 A231::nat |
|
246 A232::nat |
|
247 A233::nat |
|
248 A234::nat |
|
249 A235::nat |
|
250 A236::nat |
|
251 A237::nat |
|
252 A238::nat |
|
253 A239::nat |
|
254 A240::nat |
|
255 A241::nat |
|
256 A242::nat |
|
257 A243::nat |
|
258 A244::nat |
|
259 A245::nat |
|
260 A246::nat |
|
261 A247::nat |
|
262 A248::nat |
|
263 A249::nat |
|
264 A250::nat |
|
265 A251::nat |
|
266 A252::nat |
|
267 A253::nat |
|
268 A254::nat |
|
269 A255::nat |
|
270 A256::nat |
|
271 A257::nat |
|
272 A258::nat |
|
273 A259::nat |
|
274 A260::nat |
|
275 A261::nat |
|
276 A262::nat |
|
277 A263::nat |
|
278 A264::nat |
|
279 A265::nat |
|
280 A266::nat |
|
281 A267::nat |
|
282 A268::nat |
|
283 A269::nat |
|
284 A270::nat |
|
285 A271::nat |
|
286 A272::nat |
|
287 A273::nat |
|
288 A274::nat |
|
289 A275::nat |
|
290 A276::nat |
|
291 A277::nat |
|
292 A278::nat |
|
293 A279::nat |
|
294 A280::nat |
|
295 A281::nat |
|
296 A282::nat |
|
297 A283::nat |
|
298 A284::nat |
|
299 A285::nat |
|
300 A286::nat |
|
301 A287::nat |
|
302 A288::nat |
|
303 A289::nat |
|
304 A290::nat |
|
305 A291::nat |
|
306 A292::nat |
|
307 A293::nat |
|
308 A294::nat |
|
309 A295::nat |
|
310 A296::nat |
|
311 A297::nat |
|
312 A298::nat |
|
313 A299::nat |
|
314 |
|
315 lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r" |
|
316 by simp |
|
317 |
|
318 lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r" |
|
319 by simp |
|
320 |
|
321 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
|
322 by simp |
|
323 |
|
324 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>" |
|
325 apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*}) |
|
326 done |
|
327 |
|
328 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
|
329 apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
|
330 apply simp |
|
331 done |
|
332 |
|
333 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)" |
|
334 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
335 apply simp |
|
336 done |
|
337 |
|
338 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
|
339 apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
|
340 apply simp |
|
341 done |
|
342 |
|
343 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)" |
|
344 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
345 apply simp |
|
346 done |
|
347 |
|
348 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
|
349 apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) |
|
350 apply auto |
|
351 done |
|
352 |
|
353 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
|
354 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
355 apply auto |
|
356 done |
|
357 |
|
358 lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
|
359 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
360 apply auto |
|
361 done |
|
362 |
|
363 lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)" |
|
364 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
365 apply auto |
|
366 done |
|
367 |
|
368 |
|
369 lemma True |
|
370 proof - |
|
371 { |
|
372 fix P r |
|
373 assume pre: "P (A155 r)" |
|
374 have "\<exists>x. P x" |
|
375 using pre |
|
376 apply - |
|
377 apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) |
|
378 apply auto |
|
379 done |
|
380 } |
|
381 show ?thesis .. |
|
382 qed |
|
383 |
|
384 |
|
385 lemma "\<exists>r. A155 r = x" |
|
386 apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*}) |
|
387 done |
|
388 |
|
389 |
|
390 end |