src/HOL/Record_Benchmark/Record_Benchmark.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 46079 65bde43e829c
child 51717 9e7d1c139569
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Record_Benchmark/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 record many_B = many_A +
   316 B000::nat
   317 B001::nat
   318 B002::nat
   319 B003::nat
   320 B004::nat
   321 B005::nat
   322 B006::nat
   323 B007::nat
   324 B008::nat
   325 B009::nat
   326 B010::nat
   327 B011::nat
   328 B012::nat
   329 B013::nat
   330 B014::nat
   331 B015::nat
   332 B016::nat
   333 B017::nat
   334 B018::nat
   335 B019::nat
   336 B020::nat
   337 B021::nat
   338 B022::nat
   339 B023::nat
   340 B024::nat
   341 B025::nat
   342 B026::nat
   343 B027::nat
   344 B028::nat
   345 B029::nat
   346 B030::nat
   347 
   348 lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   349   by simp
   350 
   351 lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
   352   by simp
   353 
   354 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   355   by simp
   356 
   357 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   358   apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
   359   done
   360 
   361 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   362   apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   363   apply simp
   364   done
   365 
   366 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   367   apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   368   apply simp
   369   done
   370 
   371 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   372   apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   373   apply simp
   374   done
   375 
   376 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   377   apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   378   apply simp
   379   done
   380 
   381 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   382   apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   383   apply auto
   384   done
   385 
   386 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   387   apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   388   apply auto
   389   done
   390 
   391 lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   392   apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   393   apply auto
   394   done
   395 
   396 lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   397   apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   398   apply auto
   399   done
   400 
   401 
   402 notepad
   403 begin
   404   fix P r
   405   assume "P (A155 r)"
   406   then have "\<exists>x. P x"
   407     apply -
   408     apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   409     apply auto 
   410     done
   411 end
   412 
   413 
   414 lemma "\<exists>r. A155 r = x"
   415   apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   416   done
   417 
   418 
   419 end