merged
authorwenzelm
Fri Sep 02 16:20:09 2011 +0200 (2011-09-02 ago)
changeset 446521cc7df9ff83b
parent 44651 5d6a11e166cf
parent 44645 5938beb84adc
child 44653 6d8d09b90398
merged
Admin/Benchmarks/HOL-record/RecordBenchmark.thy
     1.1 --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Sep 02 14:43:20 2011 +0200
     1.2 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Sep 02 16:20:09 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  val tests = ["Brackin", "Instructions", "SML", "Verilog"];
     1.6  
     1.7 -timing := true;
     1.8 +Toplevel.timing := true;
     1.9  
    1.10  warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    1.11  use_thys tests;
     2.1 --- a/Admin/Benchmarks/HOL-record/ROOT.ML	Fri Sep 02 14:43:20 2011 +0200
     2.2 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML	Fri Sep 02 16:20:09 2011 +0200
     2.3 @@ -3,9 +3,9 @@
     2.4  Some benchmark on large record.
     2.5  *)
     2.6  
     2.7 -val tests = ["RecordBenchmark"];
     2.8 +val tests = ["Record_Benchmark"];
     2.9  
    2.10 -timing := true;
    2.11 +Toplevel.timing := true;
    2.12  
    2.13  warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
    2.14  use_thys tests;
     3.1 --- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy	Fri Sep 02 14:43:20 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,395 +0,0 @@
     3.4 -(*  Title:      Admin/Benchmarks/HOL-record/RecordBenchmark.thy
     3.5 -    Author:     Norbert Schirmer, DFKI
     3.6 -*)
     3.7 -
     3.8 -header {* Benchmark for large record *}
     3.9 -
    3.10 -theory RecordBenchmark
    3.11 -imports Main
    3.12 -begin
    3.13 -
    3.14 -ML {* Record.timing := true *}
    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
   3.329 -          (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*})
   3.330 -done
   3.331 -
   3.332 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   3.333 -  apply (tactic {* simp_tac
   3.334 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
   3.335 -  apply simp
   3.336 -  done
   3.337 -
   3.338 -lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   3.339 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.340 -  apply simp
   3.341 -  done
   3.342 -
   3.343 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   3.344 -  apply (tactic {* simp_tac
   3.345 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
   3.346 -  apply simp
   3.347 -  done
   3.348 -
   3.349 -lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   3.350 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.351 -  apply simp
   3.352 -  done
   3.353 -
   3.354 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.355 -  apply (tactic {* simp_tac
   3.356 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
   3.357 -  apply auto
   3.358 -  done
   3.359 -
   3.360 -lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.361 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.362 -  apply auto
   3.363 -  done
   3.364 -
   3.365 -lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.366 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.367 -  apply auto
   3.368 -  done
   3.369 -
   3.370 -lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   3.371 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.372 -  apply auto
   3.373 -  done
   3.374 -
   3.375 -
   3.376 -lemma True
   3.377 -proof -
   3.378 -  {
   3.379 -    fix P r
   3.380 -    assume pre: "P (A155 r)"
   3.381 -    have "\<exists>x. P x"
   3.382 -      using pre
   3.383 -      apply -
   3.384 -      apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
   3.385 -      apply auto 
   3.386 -      done
   3.387 -  }
   3.388 -  show ?thesis ..
   3.389 -qed
   3.390 -
   3.391 -
   3.392 -lemma "\<exists>r. A155 r = x"
   3.393 -  apply (tactic {*simp_tac 
   3.394 -           (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
   3.395 -  done
   3.396 -
   3.397 -
   3.398 -end
   3.399 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/Admin/Benchmarks/HOL-record/Record_Benchmark.thy	Fri Sep 02 16:20:09 2011 +0200
     4.3 @@ -0,0 +1,390 @@
     4.4 +(*  Title:      Admin/Benchmarks/HOL-record/Record_Benchmark.thy
     4.5 +    Author:     Norbert Schirmer, DFKI
     4.6 +*)
     4.7 +
     4.8 +header {* Benchmark for large record *}
     4.9 +
    4.10 +theory Record_Benchmark
    4.11 +imports Main
    4.12 +begin
    4.13 +
    4.14 +declare [[record_timing]]
    4.15 +
    4.16 +record many_A =
    4.17 +A000::nat
    4.18 +A001::nat
    4.19 +A002::nat
    4.20 +A003::nat
    4.21 +A004::nat
    4.22 +A005::nat
    4.23 +A006::nat
    4.24 +A007::nat
    4.25 +A008::nat
    4.26 +A009::nat
    4.27 +A010::nat
    4.28 +A011::nat
    4.29 +A012::nat
    4.30 +A013::nat
    4.31 +A014::nat
    4.32 +A015::nat
    4.33 +A016::nat
    4.34 +A017::nat
    4.35 +A018::nat
    4.36 +A019::nat
    4.37 +A020::nat
    4.38 +A021::nat
    4.39 +A022::nat
    4.40 +A023::nat
    4.41 +A024::nat
    4.42 +A025::nat
    4.43 +A026::nat
    4.44 +A027::nat
    4.45 +A028::nat
    4.46 +A029::nat
    4.47 +A030::nat
    4.48 +A031::nat
    4.49 +A032::nat
    4.50 +A033::nat
    4.51 +A034::nat
    4.52 +A035::nat
    4.53 +A036::nat
    4.54 +A037::nat
    4.55 +A038::nat
    4.56 +A039::nat
    4.57 +A040::nat
    4.58 +A041::nat
    4.59 +A042::nat
    4.60 +A043::nat
    4.61 +A044::nat
    4.62 +A045::nat
    4.63 +A046::nat
    4.64 +A047::nat
    4.65 +A048::nat
    4.66 +A049::nat
    4.67 +A050::nat
    4.68 +A051::nat
    4.69 +A052::nat
    4.70 +A053::nat
    4.71 +A054::nat
    4.72 +A055::nat
    4.73 +A056::nat
    4.74 +A057::nat
    4.75 +A058::nat
    4.76 +A059::nat
    4.77 +A060::nat
    4.78 +A061::nat
    4.79 +A062::nat
    4.80 +A063::nat
    4.81 +A064::nat
    4.82 +A065::nat
    4.83 +A066::nat
    4.84 +A067::nat
    4.85 +A068::nat
    4.86 +A069::nat
    4.87 +A070::nat
    4.88 +A071::nat
    4.89 +A072::nat
    4.90 +A073::nat
    4.91 +A074::nat
    4.92 +A075::nat
    4.93 +A076::nat
    4.94 +A077::nat
    4.95 +A078::nat
    4.96 +A079::nat
    4.97 +A080::nat
    4.98 +A081::nat
    4.99 +A082::nat
   4.100 +A083::nat
   4.101 +A084::nat
   4.102 +A085::nat
   4.103 +A086::nat
   4.104 +A087::nat
   4.105 +A088::nat
   4.106 +A089::nat
   4.107 +A090::nat
   4.108 +A091::nat
   4.109 +A092::nat
   4.110 +A093::nat
   4.111 +A094::nat
   4.112 +A095::nat
   4.113 +A096::nat
   4.114 +A097::nat
   4.115 +A098::nat
   4.116 +A099::nat
   4.117 +A100::nat
   4.118 +A101::nat
   4.119 +A102::nat
   4.120 +A103::nat
   4.121 +A104::nat
   4.122 +A105::nat
   4.123 +A106::nat
   4.124 +A107::nat
   4.125 +A108::nat
   4.126 +A109::nat
   4.127 +A110::nat
   4.128 +A111::nat
   4.129 +A112::nat
   4.130 +A113::nat
   4.131 +A114::nat
   4.132 +A115::nat
   4.133 +A116::nat
   4.134 +A117::nat
   4.135 +A118::nat
   4.136 +A119::nat
   4.137 +A120::nat
   4.138 +A121::nat
   4.139 +A122::nat
   4.140 +A123::nat
   4.141 +A124::nat
   4.142 +A125::nat
   4.143 +A126::nat
   4.144 +A127::nat
   4.145 +A128::nat
   4.146 +A129::nat
   4.147 +A130::nat
   4.148 +A131::nat
   4.149 +A132::nat
   4.150 +A133::nat
   4.151 +A134::nat
   4.152 +A135::nat
   4.153 +A136::nat
   4.154 +A137::nat
   4.155 +A138::nat
   4.156 +A139::nat
   4.157 +A140::nat
   4.158 +A141::nat
   4.159 +A142::nat
   4.160 +A143::nat
   4.161 +A144::nat
   4.162 +A145::nat
   4.163 +A146::nat
   4.164 +A147::nat
   4.165 +A148::nat
   4.166 +A149::nat
   4.167 +A150::nat
   4.168 +A151::nat
   4.169 +A152::nat
   4.170 +A153::nat
   4.171 +A154::nat
   4.172 +A155::nat
   4.173 +A156::nat
   4.174 +A157::nat
   4.175 +A158::nat
   4.176 +A159::nat
   4.177 +A160::nat
   4.178 +A161::nat
   4.179 +A162::nat
   4.180 +A163::nat
   4.181 +A164::nat
   4.182 +A165::nat
   4.183 +A166::nat
   4.184 +A167::nat
   4.185 +A168::nat
   4.186 +A169::nat
   4.187 +A170::nat
   4.188 +A171::nat
   4.189 +A172::nat
   4.190 +A173::nat
   4.191 +A174::nat
   4.192 +A175::nat
   4.193 +A176::nat
   4.194 +A177::nat
   4.195 +A178::nat
   4.196 +A179::nat
   4.197 +A180::nat
   4.198 +A181::nat
   4.199 +A182::nat
   4.200 +A183::nat
   4.201 +A184::nat
   4.202 +A185::nat
   4.203 +A186::nat
   4.204 +A187::nat
   4.205 +A188::nat
   4.206 +A189::nat
   4.207 +A190::nat
   4.208 +A191::nat
   4.209 +A192::nat
   4.210 +A193::nat
   4.211 +A194::nat
   4.212 +A195::nat
   4.213 +A196::nat
   4.214 +A197::nat
   4.215 +A198::nat
   4.216 +A199::nat
   4.217 +A200::nat
   4.218 +A201::nat
   4.219 +A202::nat
   4.220 +A203::nat
   4.221 +A204::nat
   4.222 +A205::nat
   4.223 +A206::nat
   4.224 +A207::nat
   4.225 +A208::nat
   4.226 +A209::nat
   4.227 +A210::nat
   4.228 +A211::nat
   4.229 +A212::nat
   4.230 +A213::nat
   4.231 +A214::nat
   4.232 +A215::nat
   4.233 +A216::nat
   4.234 +A217::nat
   4.235 +A218::nat
   4.236 +A219::nat
   4.237 +A220::nat
   4.238 +A221::nat
   4.239 +A222::nat
   4.240 +A223::nat
   4.241 +A224::nat
   4.242 +A225::nat
   4.243 +A226::nat
   4.244 +A227::nat
   4.245 +A228::nat
   4.246 +A229::nat
   4.247 +A230::nat
   4.248 +A231::nat
   4.249 +A232::nat
   4.250 +A233::nat
   4.251 +A234::nat
   4.252 +A235::nat
   4.253 +A236::nat
   4.254 +A237::nat
   4.255 +A238::nat
   4.256 +A239::nat
   4.257 +A240::nat
   4.258 +A241::nat
   4.259 +A242::nat
   4.260 +A243::nat
   4.261 +A244::nat
   4.262 +A245::nat
   4.263 +A246::nat
   4.264 +A247::nat
   4.265 +A248::nat
   4.266 +A249::nat
   4.267 +A250::nat
   4.268 +A251::nat
   4.269 +A252::nat
   4.270 +A253::nat
   4.271 +A254::nat
   4.272 +A255::nat
   4.273 +A256::nat
   4.274 +A257::nat
   4.275 +A258::nat
   4.276 +A259::nat
   4.277 +A260::nat
   4.278 +A261::nat
   4.279 +A262::nat
   4.280 +A263::nat
   4.281 +A264::nat
   4.282 +A265::nat
   4.283 +A266::nat
   4.284 +A267::nat
   4.285 +A268::nat
   4.286 +A269::nat
   4.287 +A270::nat
   4.288 +A271::nat
   4.289 +A272::nat
   4.290 +A273::nat
   4.291 +A274::nat
   4.292 +A275::nat
   4.293 +A276::nat
   4.294 +A277::nat
   4.295 +A278::nat
   4.296 +A279::nat
   4.297 +A280::nat
   4.298 +A281::nat
   4.299 +A282::nat
   4.300 +A283::nat
   4.301 +A284::nat
   4.302 +A285::nat
   4.303 +A286::nat
   4.304 +A287::nat
   4.305 +A288::nat
   4.306 +A289::nat
   4.307 +A290::nat
   4.308 +A291::nat
   4.309 +A292::nat
   4.310 +A293::nat
   4.311 +A294::nat
   4.312 +A295::nat
   4.313 +A296::nat
   4.314 +A297::nat
   4.315 +A298::nat
   4.316 +A299::nat
   4.317 +
   4.318 +lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   4.319 +  by simp
   4.320 +
   4.321 +lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
   4.322 +  by simp
   4.323 +
   4.324 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   4.325 +  by simp
   4.326 +
   4.327 +lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   4.328 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
   4.329 +  done
   4.330 +
   4.331 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   4.332 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   4.333 +  apply simp
   4.334 +  done
   4.335 +
   4.336 +lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   4.337 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.338 +  apply simp
   4.339 +  done
   4.340 +
   4.341 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   4.342 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   4.343 +  apply simp
   4.344 +  done
   4.345 +
   4.346 +lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   4.347 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.348 +  apply simp
   4.349 +  done
   4.350 +
   4.351 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   4.352 +  apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
   4.353 +  apply auto
   4.354 +  done
   4.355 +
   4.356 +lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   4.357 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.358 +  apply auto
   4.359 +  done
   4.360 +
   4.361 +lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   4.362 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.363 +  apply auto
   4.364 +  done
   4.365 +
   4.366 +lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   4.367 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.368 +  apply auto
   4.369 +  done
   4.370 +
   4.371 +
   4.372 +lemma True
   4.373 +proof -
   4.374 +  {
   4.375 +    fix P r
   4.376 +    assume pre: "P (A155 r)"
   4.377 +    have "\<exists>x. P x"
   4.378 +      using pre
   4.379 +      apply -
   4.380 +      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
   4.381 +      apply auto 
   4.382 +      done
   4.383 +  }
   4.384 +  show ?thesis ..
   4.385 +qed
   4.386 +
   4.387 +
   4.388 +lemma "\<exists>r. A155 r = x"
   4.389 +  apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
   4.390 +  done
   4.391 +
   4.392 +
   4.393 +end
   4.394 \ No newline at end of file
     5.1 --- a/Admin/Benchmarks/IsaMakefile	Fri Sep 02 14:43:20 2011 +0200
     5.2 +++ b/Admin/Benchmarks/IsaMakefile	Fri Sep 02 16:20:09 2011 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  HOL-record: HOL $(LOG)/HOL-record.gz
     5.5  
     5.6  $(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML	\
     5.7 -   HOL-record/RecordBenchmark.thy
     5.8 +   HOL-record/Record_Benchmark.thy
     5.9  	@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
    5.10  
    5.11  
     6.1 --- a/src/Pure/PIDE/document.ML	Fri Sep 02 14:43:20 2011 +0200
     6.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 02 16:20:09 2011 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4    type edit = string * node_edit
     6.5    type state
     6.6    val init_state: state
     6.7 -  val define_command: command_id -> string -> state -> state
     6.8 +  val define_command: command_id -> string -> string -> state -> state
     6.9    val join_commands: state -> state
    6.10    val cancel_execution: state -> Future.task list
    6.11    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    6.12 @@ -112,7 +112,13 @@
    6.13  fun map_entries f =
    6.14    map_node (fn (touched, header, perspective, entries, last_exec, result) =>
    6.15      (touched, header, perspective, f entries, last_exec, result));
    6.16 -fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
    6.17 +fun get_entries (Node {entries, ...}) = entries;
    6.18 +
    6.19 +fun iterate_entries f = Entries.iterate NONE f o get_entries;
    6.20 +fun iterate_entries_after start f (Node {entries, ...}) =
    6.21 +  (case Entries.get_after entries start of
    6.22 +    NONE => I
    6.23 +  | SOME id => Entries.iterate (SOME id) f entries);
    6.24  
    6.25  fun get_last_exec (Node {last_exec, ...}) = last_exec;
    6.26  fun set_last_exec last_exec =
    6.27 @@ -183,8 +189,9 @@
    6.28  
    6.29  fun touch_node name nodes =
    6.30    fold (fn desc =>
    6.31 -      update_node desc (set_touched true) #>
    6.32 -      desc <> name ? update_node desc (map_entries (reset_after NONE)))
    6.33 +      update_node desc
    6.34 +        (set_touched true #>
    6.35 +          desc <> name ? (map_entries (reset_after NONE) #> set_result no_result)))
    6.36      (Graph.all_succs nodes [name]) nodes;
    6.37  
    6.38  in
    6.39 @@ -231,7 +238,7 @@
    6.40  abstype state = State of
    6.41   {versions: version Inttab.table,  (*version_id -> document content*)
    6.42    commands:
    6.43 -    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
    6.44 +    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
    6.45      Toplevel.transition future list,  (*recent commands to be joined*)
    6.46    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    6.47      (*exec_id -> command_id with eval/print process*)
    6.48 @@ -246,7 +253,7 @@
    6.49  
    6.50  val init_state =
    6.51    make_state (Inttab.make [(no_id, empty_version)],
    6.52 -    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
    6.53 +    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
    6.54      Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    6.55      Future.new_group NONE);
    6.56  
    6.57 @@ -267,7 +274,7 @@
    6.58  
    6.59  (* commands *)
    6.60  
    6.61 -fun define_command (id: command_id) text =
    6.62 +fun define_command (id: command_id) name text =
    6.63    map_state (fn (versions, (commands, recent), execs, execution) =>
    6.64      let
    6.65        val id_string = print_id id;
    6.66 @@ -276,14 +283,14 @@
    6.67            Position.setmp_thread_data (Position.id_only id_string)
    6.68              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    6.69        val commands' =
    6.70 -        Inttab.update_new (id, tr) commands
    6.71 +        Inttab.update_new (id, (name, tr)) commands
    6.72            handle Inttab.DUP dup => err_dup "command" dup;
    6.73      in (versions, (commands', tr :: recent), execs, execution) end);
    6.74  
    6.75  fun the_command (State {commands, ...}) (id: command_id) =
    6.76    (case Inttab.lookup (#1 commands) id of
    6.77      NONE => err_undef "command" id
    6.78 -  | SOME tr => tr);
    6.79 +  | SOME command => command);
    6.80  
    6.81  val join_commands =
    6.82      map_state (fn (versions, (commands, recent), execs, execution) =>
    6.83 @@ -345,9 +352,7 @@
    6.84      val _ = Multithreading.interrupted ();
    6.85      val _ = Toplevel.status tr Markup.forked;
    6.86      val start = Timing.start ();
    6.87 -    val (errs, result) =
    6.88 -      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
    6.89 -      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    6.90 +    val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    6.91      val _ = timing tr (Timing.result start);
    6.92      val _ = Toplevel.status tr Markup.joined;
    6.93      val _ = List.app (Toplevel.error_msg tr) errs;
    6.94 @@ -384,28 +389,51 @@
    6.95  
    6.96  local
    6.97  
    6.98 -fun last_common last_visible node0 node =
    6.99 +fun last_common state last_visible node0 node =
   6.100    let
   6.101 -    fun get_common ((prev, id), exec) (found, (_, visible)) =
   6.102 +    fun update_flags prev (visible, initial) =
   6.103 +      let
   6.104 +        val visible' = visible andalso prev <> last_visible;
   6.105 +        val initial' = initial andalso
   6.106 +          (case prev of
   6.107 +            NONE => true
   6.108 +          | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id))));
   6.109 +      in (visible', initial') end;
   6.110 +    fun get_common ((prev, id), exec) (found, (_, flags)) =
   6.111        if found then NONE
   6.112        else
   6.113          let val found' = is_none exec orelse exec <> lookup_entry node0 id
   6.114 -        in SOME (found', (prev, visible andalso prev <> last_visible)) end;
   6.115 -  in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
   6.116 +        in SOME (found', (prev, update_flags prev flags)) end;
   6.117 +    val (found, (common, flags)) =
   6.118 +      iterate_entries get_common node (false, (NONE, (true, true)));
   6.119 +  in
   6.120 +    if found then (common, flags)
   6.121 +    else
   6.122 +      let val last = Entries.get_after (get_entries node) common
   6.123 +      in (last, update_flags last flags) end
   6.124 +  end;
   6.125 +
   6.126 +fun illegal_init () = error "Illegal theory header after end of theory";
   6.127  
   6.128 -fun new_exec state init command_id' (execs, exec) =
   6.129 -  let
   6.130 -    val command' = the_command state command_id';
   6.131 -    val exec_id' = new_id ();
   6.132 -    val exec' =
   6.133 -      snd exec |> Lazy.map (fn (st, _) =>
   6.134 -        let val tr =
   6.135 -          Future.join command'
   6.136 -          |> Toplevel.modify_init init
   6.137 -          |> Toplevel.put_id (print_id exec_id');
   6.138 -        in run_command tr st end)
   6.139 -      |> pair command_id';
   6.140 -  in ((exec_id', exec') :: execs, exec') end;
   6.141 +fun new_exec state bad_init command_id' (execs, exec, init) =
   6.142 +  if bad_init andalso is_none init then NONE
   6.143 +  else
   6.144 +    let
   6.145 +      val (name, tr0) = the_command state command_id';
   6.146 +      val (modify_init, init') =
   6.147 +        if Keyword.is_theory_begin name then
   6.148 +          (Toplevel.modify_init (the_default illegal_init init), NONE)
   6.149 +        else (I, init);
   6.150 +        val exec_id' = new_id ();
   6.151 +      val exec' =
   6.152 +        snd exec |> Lazy.map (fn (st, _) =>
   6.153 +          let val tr =
   6.154 +            Future.join tr0
   6.155 +            |> modify_init
   6.156 +            |> Toplevel.put_id (print_id exec_id');
   6.157 +          in run_command tr st end)
   6.158 +        |> pair command_id';
   6.159 +    in SOME ((exec_id', exec') :: execs, exec', init') end;
   6.160  
   6.161  fun make_required nodes =
   6.162    let
   6.163 @@ -417,6 +445,10 @@
   6.164          all_visible Symtab.empty;
   6.165    in Symtab.defined required end;
   6.166  
   6.167 +fun check_theory nodes name =
   6.168 +  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
   6.169 +  is_some (Exn.get_res (get_header (get_node nodes name)));
   6.170 +
   6.171  fun init_theory deps name node =
   6.172    let
   6.173      val (thy_name, imports, uses) = Exn.release (get_header node);
   6.174 @@ -454,6 +486,8 @@
   6.175              let
   6.176                val node0 = node_of old_version name;
   6.177                fun init () = init_theory deps name node;
   6.178 +              val bad_init =
   6.179 +                not (check_theory nodes name andalso forall (check_theory nodes o #1) deps);
   6.180              in
   6.181                (singleton o Future.forks)
   6.182                  {name = "Document.update", group = NONE,
   6.183 @@ -462,18 +496,19 @@
   6.184                    let
   6.185                      val required = is_required name;
   6.186                      val last_visible = #2 (get_perspective node);
   6.187 -                    val (common, visible) = last_common last_visible node0 node;
   6.188 +                    val (common, (visible, initial)) = last_common state last_visible node0 node;
   6.189                      val common_exec = the_exec state (the_default_entry node common);
   6.190  
   6.191 -                    val (execs, exec) = ([], common_exec) |>
   6.192 +                    val (execs, exec, _) =
   6.193 +                      ([], common_exec, if initial then SOME init else NONE) |>
   6.194                        (visible orelse required) ?
   6.195 -                        iterate_entries (after_entry node common)
   6.196 +                        iterate_entries_after common
   6.197                            (fn ((prev, id), _) => fn res =>
   6.198                              if not required andalso prev = last_visible then NONE
   6.199 -                            else SOME (new_exec state init id res)) node;
   6.200 +                            else new_exec state bad_init id res) node;
   6.201  
   6.202                      val no_execs =
   6.203 -                      iterate_entries (after_entry node0 common)
   6.204 +                      iterate_entries_after common
   6.205                          (fn ((_, id0), exec0) => fn res =>
   6.206                            if is_none exec0 then NONE
   6.207                            else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
   6.208 @@ -533,7 +568,7 @@
   6.209              (singleton o Future.forks)
   6.210                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   6.211                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
   6.212 -              (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   6.213 +              (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
   6.214  
   6.215      in (versions, commands, execs, execution) end);
   6.216  
     7.1 --- a/src/Pure/PIDE/document.scala	Fri Sep 02 14:43:20 2011 +0200
     7.2 +++ b/src/Pure/PIDE/document.scala	Fri Sep 02 16:20:09 2011 +0200
     7.3 @@ -47,6 +47,7 @@
     7.4            case other: Name => node == other.node
     7.5            case _ => false
     7.6          }
     7.7 +      override def toString: String = theory
     7.8      }
     7.9  
    7.10      sealed abstract class Edit[A, B]
     8.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Sep 02 14:43:20 2011 +0200
     8.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 16:20:09 2011 +0200
     8.3 @@ -9,7 +9,8 @@
     8.4  
     8.5  val _ =
     8.6    Isabelle_Process.add_command "Isar_Document.define_command"
     8.7 -    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
     8.8 +    (fn [id, name, text] =>
     8.9 +      Document.change_state (Document.define_command (Document.parse_id id) name text));
    8.10  
    8.11  val _ =
    8.12    Isabelle_Process.add_command "Isar_Document.cancel_execution"
     9.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Sep 02 14:43:20 2011 +0200
     9.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 02 16:20:09 2011 +0200
     9.3 @@ -148,8 +148,9 @@
     9.4  {
     9.5    /* commands */
     9.6  
     9.7 -  def define_command(id: Document.Command_ID, text: String): Unit =
     9.8 -    input("Isar_Document.define_command", Document.ID(id), text)
     9.9 +  def define_command(command: Command): Unit =
    9.10 +    input("Isar_Document.define_command",
    9.11 +      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
    9.12  
    9.13  
    9.14    /* document versions */
    10.1 --- a/src/Pure/System/session.scala	Fri Sep 02 14:43:20 2011 +0200
    10.2 +++ b/src/Pure/System/session.scala	Fri Sep 02 16:20:09 2011 +0200
    10.3 @@ -253,7 +253,7 @@
    10.4        {
    10.5          if (!global_state().defined_command(command.id)) {
    10.6            global_state.change(_.define_command(command))
    10.7 -          prover.get.define_command(command.id, Symbol.encode(command.source))
    10.8 +          prover.get.define_command(command)
    10.9          }
   10.10        }
   10.11        doc_edits foreach {
    11.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 02 14:43:20 2011 +0200
    11.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 02 16:20:09 2011 +0200
    11.3 @@ -93,7 +93,8 @@
    11.4            if (nodes_status != nodes_status1) {
    11.5              nodes_status = nodes_status1
    11.6              val order =
    11.7 -              Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    11.8 +              Library.sort_wrt((name: Document.Node.Name) => name.theory,
    11.9 +                nodes_status.keySet.toList)
   11.10              status.listData = order.map(name => name.theory + " " + nodes_status(name))
   11.11            }
   11.12        }