1.1 --- a/Admin/Benchmarks/HOL-record/ROOT.ML	Thu Sep 01 16:46:07 2011 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML	Thu Sep 01 16:58:03 2011 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  Some benchmark on large record.
     1.5  *)
     1.6  
     1.7 -val tests = ["RecordBenchmark"];
     1.8 +val tests = ["Record_Benchmark"];
     1.9  
    1.10  Toplevel.timing := true;
    1.11  

     2.1 --- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Thu Sep 01 16:46:07 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,390 +0,0 @@
     2.4 -(*  Title:      Admin/Benchmarks/HOL-record/RecordBenchmark.thy
     2.5 -    Author:     Norbert Schirmer, DFKI
     2.6 -*)
     2.7 -
     2.8 -header {* Benchmark for large record *}
     2.9 -
    2.10 -theory RecordBenchmark
    2.11 -imports Main
    2.12 -begin
    2.13 -
    2.14 -declare [[record_timing]]
    2.15 -
    2.16 -record many_A =
    2.17 -A000::nat
    2.18 -A001::nat
    2.19 -A002::nat
    2.20 -A003::nat
    2.21 -A004::nat
    2.22 -A005::nat
    2.23 -A006::nat
    2.24 -A007::nat
    2.25 -A008::nat
    2.26 -A009::nat
    2.27 -A010::nat
    2.28 -A011::nat
    2.29 -A012::nat
    2.30 -A013::nat
    2.31 -A014::nat
    2.32 -A015::nat
    2.33 -A016::nat
    2.34 -A017::nat
    2.35 -A018::nat
    2.36 -A019::nat
    2.37 -A020::nat
    2.38 -A021::nat
    2.39 -A022::nat
    2.40 -A023::nat
    2.41 -A024::nat
    2.42 -A025::nat
    2.43 -A026::nat
    2.44 -A027::nat
    2.45 -A028::nat
    2.46 -A029::nat
    2.47 -A030::nat
    2.48 -A031::nat
    2.49 -A032::nat
    2.50 -A033::nat
    2.51 -A034::nat
    2.52 -A035::nat
    2.53 -A036::nat
    2.54 -A037::nat
    2.55 -A038::nat
    2.56 -A039::nat
    2.57 -A040::nat
    2.58 -A041::nat
    2.59 -A042::nat
    2.60 -A043::nat
    2.61 -A044::nat
    2.62 -A045::nat
    2.63 -A046::nat
    2.64 -A047::nat
    2.65 -A048::nat
    2.66 -A049::nat
    2.67 -A050::nat
    2.68 -A051::nat
    2.69 -A052::nat
    2.70 -A053::nat
    2.71 -A054::nat
    2.72 -A055::nat
    2.73 -A056::nat
    2.74 -A057::nat
    2.75 -A058::nat
    2.76 -A059::nat
    2.77 -A060::nat
    2.78 -A061::nat
    2.79 -A062::nat
    2.80 -A063::nat
    2.81 -A064::nat
    2.82 -A065::nat
    2.83 -A066::nat
    2.84 -A067::nat
    2.85 -A068::nat
    2.86 -A069::nat
    2.87 -A070::nat
    2.88 -A071::nat
    2.89 -A072::nat
    2.90 -A073::nat
    2.91 -A074::nat
    2.92 -A075::nat
    2.93 -A076::nat
    2.94 -A077::nat
    2.95 -A078::nat
    2.96 -A079::nat
    2.97 -A080::nat
    2.98 -A081::nat
    2.99 -A082::nat
   2.100 -A083::nat
   2.101 -A084::nat
   2.102 -A085::nat
   2.103 -A086::nat
   2.104 -A087::nat
   2.105 -A088::nat
   2.106 -A089::nat
   2.107 -A090::nat
   2.108 -A091::nat
   2.109 -A092::nat
   2.110 -A093::nat
   2.111 -A094::nat
   2.112 -A095::nat
   2.113 -A096::nat
   2.114 -A097::nat
   2.115 -A098::nat
   2.116 -A099::nat
   2.117 -A100::nat
   2.118 -A101::nat
   2.119 -A102::nat
   2.120 -A103::nat
   2.121 -A104::nat
   2.122 -A105::nat
   2.123 -A106::nat
   2.124 -A107::nat
   2.125 -A108::nat
   2.126 -A109::nat
   2.127 -A110::nat
   2.128 -A111::nat
   2.129 -A112::nat
   2.130 -A113::nat
   2.131 -A114::nat
   2.132 -A115::nat
   2.133 -A116::nat
   2.134 -A117::nat
   2.135 -A118::nat
   2.136 -A119::nat
   2.137 -A120::nat
   2.138 -A121::nat
   2.139 -A122::nat
   2.140 -A123::nat
   2.141 -A124::nat
   2.142 -A125::nat
   2.143 -A126::nat
   2.144 -A127::nat
   2.145 -A128::nat
   2.146 -A129::nat
   2.147 -A130::nat
   2.148 -A131::nat
   2.149 -A132::nat
   2.150 -A133::nat
   2.151 -A134::nat
   2.152 -A135::nat
   2.153 -A136::nat
   2.154 -A137::nat
   2.155 -A138::nat
   2.156 -A139::nat
   2.157 -A140::nat
   2.158 -A141::nat
   2.159 -A142::nat
   2.160 -A143::nat
   2.161 -A144::nat
   2.162 -A145::nat
   2.163 -A146::nat
   2.164 -A147::nat
   2.165 -A148::nat
   2.166 -A149::nat
   2.167 -A150::nat
   2.168 -A151::nat
   2.169 -A152::nat
   2.170 -A153::nat
   2.171 -A154::nat
   2.172 -A155::nat
   2.173 -A156::nat
   2.174 -A157::nat
   2.175 -A158::nat
   2.176 -A159::nat
   2.177 -A160::nat
   2.178 -A161::nat
   2.179 -A162::nat
   2.180 -A163::nat
   2.181 -A164::nat
   2.182 -A165::nat
   2.183 -A166::nat
   2.184 -A167::nat
   2.185 -A168::nat
   2.186 -A169::nat
   2.187 -A170::nat
   2.188 -A171::nat
   2.189 -A172::nat
   2.190 -A173::nat
   2.191 -A174::nat
   2.192 -A175::nat
   2.193 -A176::nat
   2.194 -A177::nat
   2.195 -A178::nat
   2.196 -A179::nat
   2.197 -A180::nat
   2.198 -A181::nat
   2.199 -A182::nat
   2.200 -A183::nat
   2.201 -A184::nat
   2.202 -A185::nat
   2.203 -A186::nat
   2.204 -A187::nat
   2.205 -A188::nat
   2.206 -A189::nat
   2.207 -A190::nat
   2.208 -A191::nat
   2.209 -A192::nat
   2.210 -A193::nat
   2.211 -A194::nat
   2.212 -A195::nat
   2.213 -A196::nat
   2.214 -A197::nat
   2.215 -A198::nat
   2.216 -A199::nat
   2.217 -A200::nat
   2.218 -A201::nat
   2.219 -A202::nat
   2.220 -A203::nat
   2.221 -A204::nat
   2.222 -A205::nat
   2.223 -A206::nat
   2.224 -A207::nat
   2.225 -A208::nat
   2.226 -A209::nat
   2.227 -A210::nat
   2.228 -A211::nat
   2.229 -A212::nat
   2.230 -A213::nat
   2.231 -A214::nat
   2.232 -A215::nat
   2.233 -A216::nat
   2.234 -A217::nat
   2.235 -A218::nat
   2.236 -A219::nat
   2.237 -A220::nat
   2.238 -A221::nat
   2.239 -A222::nat
   2.240 -A223::nat
   2.241 -A224::nat
   2.242 -A225::nat
   2.243 -A226::nat
   2.244 -A227::nat
   2.245 -A228::nat
   2.246 -A229::nat
   2.247 -A230::nat
   2.248 -A231::nat
   2.249 -A232::nat
   2.250 -A233::nat
   2.251 -A234::nat
   2.252 -A235::nat
   2.253 -A236::nat
   2.254 -A237::nat
   2.255 -A238::nat
   2.256 -A239::nat
   2.257 -A240::nat
   2.258 -A241::nat
   2.259 -A242::nat
   2.260 -A243::nat
   2.261 -A244::nat
   2.262 -A245::nat
   2.263 -A246::nat
   2.264 -A247::nat
   2.265 -A248::nat
   2.266 -A249::nat
   2.267 -A250::nat
   2.268 -A251::nat
   2.269 -A252::nat
   2.270 -A253::nat
   2.271 -A254::nat
   2.272 -A255::nat
   2.273 -A256::nat
   2.274 -A257::nat
   2.275 -A258::nat
   2.276 -A259::nat
   2.277 -A260::nat
   2.278 -A261::nat
   2.279 -A262::nat
   2.280 -A263::nat
   2.281 -A264::nat
   2.282 -A265::nat
   2.283 -A266::nat
   2.284 -A267::nat
   2.285 -A268::nat
   2.286 -A269::nat
   2.287 -A270::nat
   2.288 -A271::nat
   2.289 -A272::nat
   2.290 -A273::nat
   2.291 -A274::nat
   2.292 -A275::nat
   2.293 -A276::nat
   2.294 -A277::nat
   2.295 -A278::nat
   2.296 -A279::nat
   2.297 -A280::nat
   2.298 -A281::nat
   2.299 -A282::nat
   2.300 -A283::nat
   2.301 -A284::nat
   2.302 -A285::nat
   2.303 -A286::nat
   2.304 -A287::nat
   2.305 -A288::nat
   2.306 -A289::nat
   2.307 -A290::nat
   2.308 -A291::nat
   2.309 -A292::nat
   2.310 -A293::nat
   2.311 -A294::nat
   2.312 -A295::nat
   2.313 -A296::nat
   2.314 -A297::nat
   2.315 -A298::nat
   2.316 -A299::nat
   2.317 -
   2.318 -lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   2.319 -  by simp
   2.320 -
   2.321 -lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
   2.322 -  by simp
   2.323 -
   2.324 -lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   2.325 -  by simp
   2.326 -
   2.327 -lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   2.328 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
   2.329 -  done
   2.330 -
   2.331 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   2.332 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   2.333 -  apply simp
   2.334 -  done
   2.335 -
   2.336 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   2.337 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.338 -  apply simp
   2.339 -  done
   2.340 -
   2.341 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   2.342 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   2.343 -  apply simp
   2.344 -  done
   2.345 -
   2.346 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   2.347 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.348 -  apply simp
   2.349 -  done
   2.350 -
   2.351 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   2.352 -  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   2.353 -  apply auto
   2.354 -  done
   2.355 -
   2.356 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   2.357 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.358 -  apply auto
   2.359 -  done
   2.360 -
   2.361 -lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   2.362 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.363 -  apply auto
   2.364 -  done
   2.365 -
   2.366 -lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   2.367 -  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.368 -  apply auto
   2.369 -  done
   2.370 -
   2.371 -
   2.372 -lemma True
   2.373 -proof -
   2.374 -  {
   2.375 -    fix P r
   2.376 -    assume pre: "P (A155 r)"
   2.377 -    have "\<exists>x. P x"
   2.378 -      using pre
   2.379 -      apply -
   2.380 -      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   2.381 -      apply auto 
   2.382 -      done
   2.383 -  }
   2.384 -  show ?thesis ..
   2.385 -qed
   2.386 -
   2.387 -
   2.388 -lemma "\<exists>r. A155 r = x"
   2.389 -  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   2.390 -  done
   2.391 -
   2.392 -
   2.393 -end
   2.394 \ No newline at end of file

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/Benchmarks/HOL-record/Record_Benchmark.thy	Thu Sep 01 16:58:03 2011 +0200
     3.3 @@ -0,0 +1,390 @@
     3.4 +(*  Title:      Admin/Benchmarks/HOL-record/Record_Benchmark.thy
     3.5 +    Author:     Norbert Schirmer, DFKI
     3.6 +*)
     3.7 +
     3.8 +header {* Benchmark for large record *}
     3.9 +
    3.10 +theory Record_Benchmark
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +declare [[record_timing]]
    3.15 +
    3.16 +record many_A =
    3.17 +A000::nat
    3.18 +A001::nat
    3.19 +A002::nat
    3.20 +A003::nat
    3.21 +A004::nat
    3.22 +A005::nat
    3.23 +A006::nat
    3.24 +A007::nat
    3.25 +A008::nat
    3.26 +A009::nat
    3.27 +A010::nat
    3.28 +A011::nat
    3.29 +A012::nat
    3.30 +A013::nat
    3.31 +A014::nat
    3.32 +A015::nat
    3.33 +A016::nat
    3.34 +A017::nat
    3.35 +A018::nat
    3.36 +A019::nat
    3.37 +A020::nat
    3.38 +A021::nat
    3.39 +A022::nat
    3.40 +A023::nat
    3.41 +A024::nat
    3.42 +A025::nat
    3.43 +A026::nat
    3.44 +A027::nat
    3.45 +A028::nat
    3.46 +A029::nat
    3.47 +A030::nat
    3.48 +A031::nat
    3.49 +A032::nat
    3.50 +A033::nat
    3.51 +A034::nat
    3.52 +A035::nat
    3.53 +A036::nat
    3.54 +A037::nat
    3.55 +A038::nat
    3.56 +A039::nat
    3.57 +A040::nat
    3.58 +A041::nat
    3.59 +A042::nat
    3.60 +A043::nat
    3.61 +A044::nat
    3.62 +A045::nat
    3.63 +A046::nat
    3.64 +A047::nat
    3.65 +A048::nat
    3.66 +A049::nat
    3.67 +A050::nat
    3.68 +A051::nat
    3.69 +A052::nat
    3.70 +A053::nat
    3.71 +A054::nat
    3.72 +A055::nat
    3.73 +A056::nat
    3.74 +A057::nat
    3.75 +A058::nat
    3.76 +A059::nat
    3.77 +A060::nat
    3.78 +A061::nat
    3.79 +A062::nat
    3.80 +A063::nat
    3.81 +A064::nat
    3.82 +A065::nat
    3.83 +A066::nat
    3.84 +A067::nat
    3.85 +A068::nat
    3.86 +A069::nat
    3.87 +A070::nat
    3.88 +A071::nat
    3.89 +A072::nat
    3.90 +A073::nat
    3.91 +A074::nat
    3.92 +A075::nat
    3.93 +A076::nat
    3.94 +A077::nat
    3.95 +A078::nat
    3.96 +A079::nat
    3.97 +A080::nat
    3.98 +A081::nat
    3.99 +A082::nat
   3.100 +A083::nat
   3.101 +A084::nat
   3.102 +A085::nat
   3.103 +A086::nat
   3.104 +A087::nat
   3.105 +A088::nat
   3.106 +A089::nat
   3.107 +A090::nat
   3.108 +A091::nat
   3.109 +A092::nat
   3.110 +A093::nat
   3.111 +A094::nat
   3.112 +A095::nat
   3.113 +A096::nat
   3.114 +A097::nat
   3.115 +A098::nat
   3.116 +A099::nat
   3.117 +A100::nat
   3.118 +A101::nat
   3.119 +A102::nat
   3.120 +A103::nat
   3.121 +A104::nat
   3.122 +A105::nat
   3.123 +A106::nat
   3.124 +A107::nat
   3.125 +A108::nat
   3.126 +A109::nat
   3.127 +A110::nat
   3.128 +A111::nat
   3.129 +A112::nat
   3.130 +A113::nat
   3.131 +A114::nat
   3.132 +A115::nat
   3.133 +A116::nat
   3.134 +A117::nat
   3.135 +A118::nat
   3.136 +A119::nat
   3.137 +A120::nat
   3.138 +A121::nat
   3.139 +A122::nat
   3.140 +A123::nat
   3.141 +A124::nat
   3.142 +A125::nat
   3.143 +A126::nat
   3.144 +A127::nat
   3.145 +A128::nat
   3.146 +A129::nat
   3.147 +A130::nat
   3.148 +A131::nat
   3.149 +A132::nat
   3.150 +A133::nat
   3.151 +A134::nat
   3.152 +A135::nat
   3.153 +A136::nat
   3.154 +A137::nat
   3.155 +A138::nat
   3.156 +A139::nat
   3.157 +A140::nat
   3.158 +A141::nat
   3.159 +A142::nat
   3.160 +A143::nat
   3.161 +A144::nat
   3.162 +A145::nat
   3.163 +A146::nat
   3.164 +A147::nat
   3.165 +A148::nat
   3.166 +A149::nat
   3.167 +A150::nat
   3.168 +A151::nat
   3.169 +A152::nat
   3.170 +A153::nat
   3.171 +A154::nat
   3.172 +A155::nat
   3.173 +A156::nat
   3.174 +A157::nat
   3.175 +A158::nat
   3.176 +A159::nat
   3.177 +A160::nat
   3.178 +A161::nat
   3.179 +A162::nat
   3.180 +A163::nat
   3.181 +A164::nat
   3.182 +A165::nat
   3.183 +A166::nat
   3.184 +A167::nat
   3.185 +A168::nat
   3.186 +A169::nat
   3.187 +A170::nat
   3.188 +A171::nat
   3.189 +A172::nat
   3.190 +A173::nat
   3.191 +A174::nat
   3.192 +A175::nat
   3.193 +A176::nat
   3.194 +A177::nat
   3.195 +A178::nat
   3.196 +A179::nat
   3.197 +A180::nat
   3.198 +A181::nat
   3.199 +A182::nat
   3.200 +A183::nat
   3.201 +A184::nat
   3.202 +A185::nat
   3.203 +A186::nat
   3.204 +A187::nat
   3.205 +A188::nat
   3.206 +A189::nat
   3.207 +A190::nat
   3.208 +A191::nat
   3.209 +A192::nat
   3.210 +A193::nat
   3.211 +A194::nat
   3.212 +A195::nat
   3.213 +A196::nat
   3.214 +A197::nat
   3.215 +A198::nat
   3.216 +A199::nat
   3.217 +A200::nat
   3.218 +A201::nat
   3.219 +A202::nat
   3.220 +A203::nat
   3.221 +A204::nat
   3.222 +A205::nat
   3.223 +A206::nat
   3.224 +A207::nat
   3.225 +A208::nat
   3.226 +A209::nat
   3.227 +A210::nat
   3.228 +A211::nat
   3.229 +A212::nat
   3.230 +A213::nat
   3.231 +A214::nat
   3.232 +A215::nat
   3.233 +A216::nat
   3.234 +A217::nat
   3.235 +A218::nat
   3.236 +A219::nat
   3.237 +A220::nat
   3.238 +A221::nat
   3.239 +A222::nat
   3.240 +A223::nat
   3.241 +A224::nat
   3.242 +A225::nat
   3.243 +A226::nat
   3.244 +A227::nat
   3.245 +A228::nat
   3.246 +A229::nat
   3.247 +A230::nat
   3.248 +A231::nat
   3.249 +A232::nat
   3.250 +A233::nat
   3.251 +A234::nat
   3.252 +A235::nat
   3.253 +A236::nat
   3.254 +A237::nat
   3.255 +A238::nat
   3.256 +A239::nat
   3.257 +A240::nat
   3.258 +A241::nat
   3.259 +A242::nat
   3.260 +A243::nat
   3.261 +A244::nat
   3.262 +A245::nat
   3.263 +A246::nat
   3.264 +A247::nat
   3.265 +A248::nat
   3.266 +A249::nat
   3.267 +A250::nat
   3.268 +A251::nat
   3.269 +A252::nat
   3.270 +A253::nat
   3.271 +A254::nat
   3.272 +A255::nat
   3.273 +A256::nat
   3.274 +A257::nat
   3.275 +A258::nat
   3.276 +A259::nat
   3.277 +A260::nat
   3.278 +A261::nat
   3.279 +A262::nat
   3.280 +A263::nat
   3.281 +A264::nat
   3.282 +A265::nat
   3.283 +A266::nat
   3.284 +A267::nat
   3.285 +A268::nat
   3.286 +A269::nat
   3.287 +A270::nat
   3.288 +A271::nat
   3.289 +A272::nat
   3.290 +A273::nat
   3.291 +A274::nat
   3.292 +A275::nat
   3.293 +A276::nat
   3.294 +A277::nat
   3.295 +A278::nat
   3.296 +A279::nat
   3.297 +A280::nat
   3.298 +A281::nat
   3.299 +A282::nat
   3.300 +A283::nat
   3.301 +A284::nat
   3.302 +A285::nat
   3.303 +A286::nat
   3.304 +A287::nat
   3.305 +A288::nat
   3.306 +A289::nat
   3.307 +A290::nat
   3.308 +A291::nat
   3.309 +A292::nat
   3.310 +A293::nat
   3.311 +A294::nat
   3.312 +A295::nat
   3.313 +A296::nat
   3.314 +A297::nat
   3.315 +A298::nat
   3.316 +A299::nat
   3.317 +
   3.318 +lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   3.319 +  by simp
   3.320 +
   3.321 +lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
   3.322 +  by simp
   3.323 +
   3.324 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   3.325 +  by simp
   3.326 +
   3.327 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   3.328 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
   3.329 +  done
   3.330 +
   3.331 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   3.332 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   3.333 +  apply simp
   3.334 +  done
   3.335 +
   3.336 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   3.337 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.338 +  apply simp
   3.339 +  done
   3.340 +
   3.341 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   3.342 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   3.343 +  apply simp
   3.344 +  done
   3.345 +
   3.346 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   3.347 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.348 +  apply simp
   3.349 +  done
   3.350 +
   3.351 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.352 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   3.353 +  apply auto
   3.354 +  done
   3.355 +
   3.356 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.357 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.358 +  apply auto
   3.359 +  done
   3.360 +
   3.361 +lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.362 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.363 +  apply auto
   3.364 +  done
   3.365 +
   3.366 +lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.367 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.368 +  apply auto
   3.369 +  done
   3.370 +
   3.371 +
   3.372 +lemma True
   3.373 +proof -
   3.374 +  {
   3.375 +    fix P r
   3.376 +    assume pre: "P (A155 r)"
   3.377 +    have "\<exists>x. P x"
   3.378 +      using pre
   3.379 +      apply -
   3.380 +      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   3.381 +      apply auto 
   3.382 +      done
   3.383 +  }
   3.384 +  show ?thesis ..
   3.385 +qed
   3.386 +
   3.387 +
   3.388 +lemma "\<exists>r. A155 r = x"
   3.389 +  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   3.390 +  done
   3.391 +
   3.392 +
   3.393 +end
   3.394 \ No newline at end of file

     4.1 --- a/Admin/Benchmarks/IsaMakefile	Thu Sep 01 16:46:07 2011 +0200
     4.2 +++ b/Admin/Benchmarks/IsaMakefile	Thu Sep 01 16:58:03 2011 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4  HOL-record: HOL $(LOG)/HOL-record.gz
     4.5  
     4.6  $(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML	\
     4.7 -   HOL-record/RecordBenchmark.thy
     4.8 +   HOL-record/Record_Benchmark.thy
     4.9  	@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
    4.10  
    4.11