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