2588 lemma threads_set_eq: |
2588 lemma threads_set_eq: |
2589 "the_thread ` (subtree (tRAG s) (Th th)) = |
2589 "the_thread ` (subtree (tRAG s) (Th th)) = |
2590 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
2590 {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R") |
2591 by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) |
2591 by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) |
2592 |
2592 |
|
2593 context valid_trace |
|
2594 begin |
|
2595 |
|
2596 lemma RAG_tRAG_transfer: |
|
2597 assumes "RAG s' = RAG s \<union> {(Th th, Cs cs)}" |
|
2598 and "(Cs cs, Th th'') \<in> RAG s" |
|
2599 shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R") |
|
2600 proof - |
|
2601 { fix n1 n2 |
|
2602 assume "(n1, n2) \<in> ?L" |
|
2603 from this[unfolded tRAG_alt_def] |
|
2604 obtain th1 th2 cs' where |
|
2605 h: "n1 = Th th1" "n2 = Th th2" |
|
2606 "(Th th1, Cs cs') \<in> RAG s'" |
|
2607 "(Cs cs', Th th2) \<in> RAG s'" by auto |
|
2608 from h(4) and assms(1) have cs_in: "(Cs cs', Th th2) \<in> RAG s" by auto |
|
2609 from h(3) and assms(1) |
|
2610 have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> |
|
2611 (Th th1, Cs cs') \<in> RAG s" by auto |
|
2612 hence "(n1, n2) \<in> ?R" |
|
2613 proof |
|
2614 assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" |
|
2615 hence eq_th1: "th1 = th" by simp |
|
2616 moreover have "th2 = th''" |
|
2617 proof - |
|
2618 from h1 have "cs' = cs" by simp |
|
2619 from assms(2) cs_in[unfolded this] |
|
2620 show ?thesis using unique_RAG by auto |
|
2621 qed |
|
2622 ultimately show ?thesis using h(1,2) by auto |
|
2623 next |
|
2624 assume "(Th th1, Cs cs') \<in> RAG s" |
|
2625 with cs_in have "(Th th1, Th th2) \<in> tRAG s" |
|
2626 by (unfold tRAG_alt_def, auto) |
|
2627 from this[folded h(1, 2)] show ?thesis by auto |
|
2628 qed |
|
2629 } moreover { |
|
2630 fix n1 n2 |
|
2631 assume "(n1, n2) \<in> ?R" |
|
2632 hence "(n1, n2) \<in>tRAG s \<or> (n1, n2) = (Th th, Th th'')" by auto |
|
2633 hence "(n1, n2) \<in> ?L" |
|
2634 proof |
|
2635 assume "(n1, n2) \<in> tRAG s" |
|
2636 moreover have "... \<subseteq> ?L" |
|
2637 proof(rule tRAG_mono) |
|
2638 show "RAG s \<subseteq> RAG s'" by (unfold assms(1), auto) |
|
2639 qed |
|
2640 ultimately show ?thesis by auto |
|
2641 next |
|
2642 assume eq_n: "(n1, n2) = (Th th, Th th'')" |
|
2643 from assms(1, 2) have "(Cs cs, Th th'') \<in> RAG s'" by auto |
|
2644 moreover have "(Th th, Cs cs) \<in> RAG s'" using assms(1) by auto |
|
2645 ultimately show ?thesis |
|
2646 by (unfold eq_n tRAG_alt_def, auto) |
|
2647 qed |
|
2648 } ultimately show ?thesis by auto |
|
2649 qed |
|
2650 |
2593 lemma dependants_alt_def: |
2651 lemma dependants_alt_def: |
2594 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
2652 "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}" |
2595 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
2653 by (metis eq_RAG s_dependants_def tRAG_trancl_eq) |
2596 |
2654 |
2597 lemma dependants_alt_def1: |
2655 lemma dependants_alt_def1: |
2598 "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}" |
2656 "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}" |
2599 using dependants_alt_def tRAG_trancl_eq by auto |
2657 using dependants_alt_def tRAG_trancl_eq by auto |
|
2658 |
|
2659 end |
2600 |
2660 |
2601 section {* Chain to readys *} |
2661 section {* Chain to readys *} |
2602 |
2662 |
2603 context valid_trace |
2663 context valid_trace |
2604 begin |
2664 begin |
4204 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
4264 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}" |
4205 using count_eq_tRAG_plus[OF assms] by auto |
4265 using count_eq_tRAG_plus[OF assms] by auto |
4206 |
4266 |
4207 end |
4267 end |
4208 |
4268 |
|
4269 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
|
4270 where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))" |
|
4271 |
|
4272 lemma detached_test: |
|
4273 shows "detached s th = (Th th \<notin> Field (RAG s))" |
|
4274 apply(simp add: detached_def Field_def) |
|
4275 apply(simp add: s_RAG_def) |
|
4276 apply(simp add: s_holding_abv s_waiting_abv) |
|
4277 apply(simp add: Domain_iff Range_iff) |
|
4278 apply(simp add: wq_def) |
|
4279 apply(auto) |
|
4280 done |
|
4281 |
|
4282 context valid_trace |
|
4283 begin |
|
4284 |
|
4285 lemma detached_intro: |
|
4286 assumes eq_pv: "cntP s th = cntV s th" |
|
4287 shows "detached s th" |
|
4288 proof - |
|
4289 from eq_pv cnp_cnv_cncs |
|
4290 have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:pvD_def) |
|
4291 thus ?thesis |
|
4292 proof |
|
4293 assume "th \<notin> threads s" |
|
4294 with rg_RAG_threads dm_RAG_threads |
|
4295 show ?thesis |
|
4296 by (auto simp add: detached_def s_RAG_def s_waiting_abv |
|
4297 s_holding_abv wq_def Domain_iff Range_iff) |
|
4298 next |
|
4299 assume "th \<in> readys s" |
|
4300 moreover have "Th th \<notin> Range (RAG s)" |
|
4301 proof - |
|
4302 from eq_pv_children[OF assms] |
|
4303 have "children (RAG s) (Th th) = {}" . |
|
4304 thus ?thesis |
|
4305 by (unfold children_def, auto) |
|
4306 qed |
|
4307 ultimately show ?thesis |
|
4308 by (auto simp add: detached_def s_RAG_def s_waiting_abv |
|
4309 s_holding_abv wq_def readys_def) |
|
4310 qed |
|
4311 qed |
|
4312 |
|
4313 lemma detached_elim: |
|
4314 assumes dtc: "detached s th" |
|
4315 shows "cntP s th = cntV s th" |
|
4316 proof - |
|
4317 have cncs_z: "cntCS s th = 0" |
|
4318 proof - |
|
4319 from dtc have "holdents s th = {}" |
|
4320 unfolding detached_def holdents_test s_RAG_def |
|
4321 by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) |
|
4322 thus ?thesis by (auto simp:cntCS_def) |
|
4323 qed |
|
4324 show ?thesis |
|
4325 proof(cases "th \<in> threads s") |
|
4326 case True |
|
4327 with dtc |
|
4328 have "th \<in> readys s" |
|
4329 by (unfold readys_def detached_def Field_def Domain_def Range_def, |
|
4330 auto simp:waiting_eq s_RAG_def) |
|
4331 with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) |
|
4332 next |
|
4333 case False |
|
4334 with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def) |
|
4335 qed |
|
4336 qed |
|
4337 |
|
4338 lemma detached_eq: |
|
4339 shows "(detached s th) = (cntP s th = cntV s th)" |
|
4340 by (insert vt, auto intro:detached_intro detached_elim) |
|
4341 |
|
4342 end |
|
4343 |
4209 section {* hhh *} |
4344 section {* hhh *} |
4210 |
|
4211 lemma RAG_tRAG_transfer: |
|
4212 assumes "vt s'" |
|
4213 assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}" |
|
4214 and "(Cs cs, Th th'') \<in> RAG s'" |
|
4215 shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R") |
|
4216 proof - |
|
4217 interpret vt_s': valid_trace "s'" using assms(1) |
|
4218 by (unfold_locales, simp) |
|
4219 { fix n1 n2 |
|
4220 assume "(n1, n2) \<in> ?L" |
|
4221 from this[unfolded tRAG_alt_def] |
|
4222 obtain th1 th2 cs' where |
|
4223 h: "n1 = Th th1" "n2 = Th th2" |
|
4224 "(Th th1, Cs cs') \<in> RAG s" |
|
4225 "(Cs cs', Th th2) \<in> RAG s" by auto |
|
4226 from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto |
|
4227 from h(3) and assms(2) |
|
4228 have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> |
|
4229 (Th th1, Cs cs') \<in> RAG s'" by auto |
|
4230 hence "(n1, n2) \<in> ?R" |
|
4231 proof |
|
4232 assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" |
|
4233 hence eq_th1: "th1 = th" by simp |
|
4234 moreover have "th2 = th''" |
|
4235 proof - |
|
4236 from h1 have "cs' = cs" by simp |
|
4237 from assms(3) cs_in[unfolded this] |
|
4238 show ?thesis using vt_s'.unique_RAG by auto |
|
4239 qed |
|
4240 ultimately show ?thesis using h(1,2) by auto |
|
4241 next |
|
4242 assume "(Th th1, Cs cs') \<in> RAG s'" |
|
4243 with cs_in have "(Th th1, Th th2) \<in> tRAG s'" |
|
4244 by (unfold tRAG_alt_def, auto) |
|
4245 from this[folded h(1, 2)] show ?thesis by auto |
|
4246 qed |
|
4247 } moreover { |
|
4248 fix n1 n2 |
|
4249 assume "(n1, n2) \<in> ?R" |
|
4250 hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto |
|
4251 hence "(n1, n2) \<in> ?L" |
|
4252 proof |
|
4253 assume "(n1, n2) \<in> tRAG s'" |
|
4254 moreover have "... \<subseteq> ?L" |
|
4255 proof(rule tRAG_mono) |
|
4256 show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto) |
|
4257 qed |
|
4258 ultimately show ?thesis by auto |
|
4259 next |
|
4260 assume eq_n: "(n1, n2) = (Th th, Th th'')" |
|
4261 from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto |
|
4262 moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto |
|
4263 ultimately show ?thesis |
|
4264 by (unfold eq_n tRAG_alt_def, auto) |
|
4265 qed |
|
4266 } ultimately show ?thesis by auto |
|
4267 qed |
|
4268 |
|
4269 context valid_trace |
|
4270 begin |
|
4271 |
|
4272 lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] |
|
4273 |
|
4274 end |
|
4275 |
4345 |
4276 lemma cp_alt_def1: |
4346 lemma cp_alt_def1: |
4277 "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" |
4347 "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" |
4278 proof - |
4348 proof - |
4279 have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = |
4349 have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = |
4297 obtain th where eq_a: "a = Th th" by auto |
4367 obtain th where eq_a: "a = Th th" by auto |
4298 show "cp_gen s a = (cp s \<circ> the_thread) a" |
4368 show "cp_gen s a = (cp s \<circ> the_thread) a" |
4299 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
4369 by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) |
4300 qed |
4370 qed |
4301 |
4371 |
4302 context valid_trace |
|
4303 begin |
|
4304 |
|
4305 lemma subtree_tRAG_thread: |
|
4306 assumes "th \<in> threads s" |
|
4307 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
4308 proof - |
|
4309 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4310 by (unfold tRAG_subtree_eq, simp) |
|
4311 also have "... \<subseteq> ?R" |
|
4312 proof |
|
4313 fix x |
|
4314 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4315 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
4316 from this(2) |
|
4317 show "x \<in> ?R" |
|
4318 proof(cases rule:subtreeE) |
|
4319 case 1 |
|
4320 thus ?thesis by (simp add: assms h(1)) |
|
4321 next |
|
4322 case 2 |
|
4323 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
|
4324 qed |
|
4325 qed |
|
4326 finally show ?thesis . |
|
4327 qed |
|
4328 |
|
4329 lemma readys_root: |
|
4330 assumes "th \<in> readys s" |
|
4331 shows "root (RAG s) (Th th)" |
|
4332 proof - |
|
4333 { fix x |
|
4334 assume "x \<in> ancestors (RAG s) (Th th)" |
|
4335 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
4336 from tranclD[OF this] |
|
4337 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
4338 with assms(1) have False |
|
4339 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
4340 by (fold wq_def, blast) |
|
4341 } thus ?thesis by (unfold root_def, auto) |
|
4342 qed |
|
4343 |
|
4344 lemma readys_in_no_subtree: |
|
4345 assumes "th \<in> readys s" |
|
4346 and "th' \<noteq> th" |
|
4347 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
4348 proof |
|
4349 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
4350 thus False |
|
4351 proof(cases rule:subtreeE) |
|
4352 case 1 |
|
4353 with assms show ?thesis by auto |
|
4354 next |
|
4355 case 2 |
|
4356 with readys_root[OF assms(1)] |
|
4357 show ?thesis by (auto simp:root_def) |
|
4358 qed |
|
4359 qed |
|
4360 |
|
4361 lemma not_in_thread_isolated: |
|
4362 assumes "th \<notin> threads s" |
|
4363 shows "(Th th) \<notin> Field (RAG s)" |
|
4364 proof |
|
4365 assume "(Th th) \<in> Field (RAG s)" |
|
4366 with dm_RAG_threads and rg_RAG_threads assms |
|
4367 show False by (unfold Field_def, blast) |
|
4368 qed |
|
4369 |
|
4370 end |
|
4371 |
|
4372 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
|
4373 where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))" |
|
4374 |
|
4375 |
|
4376 lemma detached_test: |
|
4377 shows "detached s th = (Th th \<notin> Field (RAG s))" |
|
4378 apply(simp add: detached_def Field_def) |
|
4379 apply(simp add: s_RAG_def) |
|
4380 apply(simp add: s_holding_abv s_waiting_abv) |
|
4381 apply(simp add: Domain_iff Range_iff) |
|
4382 apply(simp add: wq_def) |
|
4383 apply(auto) |
|
4384 done |
|
4385 |
|
4386 context valid_trace |
|
4387 begin |
|
4388 |
|
4389 lemma detached_intro: |
|
4390 assumes eq_pv: "cntP s th = cntV s th" |
|
4391 shows "detached s th" |
|
4392 proof - |
|
4393 from eq_pv cnp_cnv_cncs |
|
4394 have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:pvD_def) |
|
4395 thus ?thesis |
|
4396 proof |
|
4397 assume "th \<notin> threads s" |
|
4398 with rg_RAG_threads dm_RAG_threads |
|
4399 show ?thesis |
|
4400 by (auto simp add: detached_def s_RAG_def s_waiting_abv |
|
4401 s_holding_abv wq_def Domain_iff Range_iff) |
|
4402 next |
|
4403 assume "th \<in> readys s" |
|
4404 moreover have "Th th \<notin> Range (RAG s)" |
|
4405 proof - |
|
4406 from eq_pv_children[OF assms] |
|
4407 have "children (RAG s) (Th th) = {}" . |
|
4408 thus ?thesis |
|
4409 by (unfold children_def, auto) |
|
4410 qed |
|
4411 ultimately show ?thesis |
|
4412 by (auto simp add: detached_def s_RAG_def s_waiting_abv |
|
4413 s_holding_abv wq_def readys_def) |
|
4414 qed |
|
4415 qed |
|
4416 |
|
4417 lemma detached_elim: |
|
4418 assumes dtc: "detached s th" |
|
4419 shows "cntP s th = cntV s th" |
|
4420 proof - |
|
4421 have cncs_z: "cntCS s th = 0" |
|
4422 proof - |
|
4423 from dtc have "holdents s th = {}" |
|
4424 unfolding detached_def holdents_test s_RAG_def |
|
4425 by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) |
|
4426 thus ?thesis by (auto simp:cntCS_def) |
|
4427 qed |
|
4428 show ?thesis |
|
4429 proof(cases "th \<in> threads s") |
|
4430 case True |
|
4431 with dtc |
|
4432 have "th \<in> readys s" |
|
4433 by (unfold readys_def detached_def Field_def Domain_def Range_def, |
|
4434 auto simp:waiting_eq s_RAG_def) |
|
4435 with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) |
|
4436 next |
|
4437 case False |
|
4438 with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def) |
|
4439 qed |
|
4440 qed |
|
4441 |
|
4442 lemma detached_eq: |
|
4443 shows "(detached s th) = (cntP s th = cntV s th)" |
|
4444 by (insert vt, auto intro:detached_intro detached_elim) |
|
4445 |
|
4446 end |
|
4447 |
4372 |
4448 context valid_trace |
4373 context valid_trace |
4449 begin |
4374 begin |
4450 (* ddd *) |
4375 (* ddd *) |
4451 lemma cp_gen_rec: |
4376 lemma cp_gen_rec: |
4521 qed |
4446 qed |
4522 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
4447 thus ?thesis by (subst (1) h(1), unfold h(2), simp) |
4523 qed |
4448 qed |
4524 qed |
4449 qed |
4525 |
4450 |
4526 lemma next_th_holding: |
4451 section {* Relating @{term cp}-values of @{term threads} and @{term readys }*} |
4527 assumes nxt: "next_th s th cs th'" |
|
4528 shows "holding (wq s) th cs" |
|
4529 proof - |
|
4530 from nxt[unfolded next_th_def] |
|
4531 obtain rest where h: "wq s cs = th # rest" |
|
4532 "rest \<noteq> []" |
|
4533 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4534 thus ?thesis |
|
4535 by (unfold cs_holding_def, auto) |
|
4536 qed |
|
4537 |
|
4538 lemma next_th_waiting: |
|
4539 assumes nxt: "next_th s th cs th'" |
|
4540 shows "waiting (wq s) th' cs" |
|
4541 proof - |
|
4542 from nxt[unfolded next_th_def] |
|
4543 obtain rest where h: "wq s cs = th # rest" |
|
4544 "rest \<noteq> []" |
|
4545 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4546 from wq_distinct[of cs, unfolded h] |
|
4547 have dst: "distinct (th # rest)" . |
|
4548 have in_rest: "th' \<in> set rest" |
|
4549 proof(unfold h, rule someI2) |
|
4550 show "distinct rest \<and> set rest = set rest" using dst by auto |
|
4551 next |
|
4552 fix x assume "distinct x \<and> set x = set rest" |
|
4553 with h(2) |
|
4554 show "hd x \<in> set (rest)" by (cases x, auto) |
|
4555 qed |
|
4556 hence "th' \<in> set (wq s cs)" by (unfold h(1), auto) |
|
4557 moreover have "th' \<noteq> hd (wq s cs)" |
|
4558 by (unfold h(1), insert in_rest dst, auto) |
|
4559 ultimately show ?thesis by (auto simp:cs_waiting_def) |
|
4560 qed |
|
4561 |
|
4562 lemma next_th_RAG: |
|
4563 assumes nxt: "next_th (s::event list) th cs th'" |
|
4564 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
|
4565 using vt assms next_th_holding next_th_waiting |
|
4566 by (unfold s_RAG_def, simp) |
|
4567 |
|
4568 end |
|
4569 |
|
4570 lemma next_th_unique: |
|
4571 assumes nt1: "next_th s th cs th1" |
|
4572 and nt2: "next_th s th cs th2" |
|
4573 shows "th1 = th2" |
|
4574 using assms by (unfold next_th_def, auto) |
|
4575 |
|
4576 context valid_trace |
|
4577 begin |
|
4578 |
4452 |
4579 lemma threads_alt_def: |
4453 lemma threads_alt_def: |
4580 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
4454 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
4581 (is "?L = ?R") |
4455 (is "?L = ?R") |
4582 proof - |
4456 proof - |
4643 thus ?thesis by simp |
4517 thus ?thesis by simp |
4644 qed |
4518 qed |
4645 finally show ?thesis by simp |
4519 finally show ?thesis by simp |
4646 qed (auto simp:threads_alt_def) |
4520 qed (auto simp:threads_alt_def) |
4647 |
4521 |
4648 lemma create_pre: |
|
4649 assumes stp: "step s e" |
|
4650 and not_in: "th \<notin> threads s" |
|
4651 and is_in: "th \<in> threads (e#s)" |
|
4652 obtains prio where "e = Create th prio" |
|
4653 proof - |
|
4654 from assms |
|
4655 show ?thesis |
|
4656 proof(cases) |
|
4657 case (thread_create thread prio) |
|
4658 with is_in not_in have "e = Create th prio" by simp |
|
4659 from that[OF this] show ?thesis . |
|
4660 next |
|
4661 case (thread_exit thread) |
|
4662 with assms show ?thesis by (auto intro!:that) |
|
4663 next |
|
4664 case (thread_P thread) |
|
4665 with assms show ?thesis by (auto intro!:that) |
|
4666 next |
|
4667 case (thread_V thread) |
|
4668 with assms show ?thesis by (auto intro!:that) |
|
4669 next |
|
4670 case (thread_set thread) |
|
4671 with assms show ?thesis by (auto intro!:that) |
|
4672 qed |
|
4673 qed |
|
4674 |
|
4675 end |
4522 end |
4676 |
4523 |
4677 section {* Pending properties *} |
4524 section {* Pending properties *} |
|
4525 |
|
4526 lemma next_th_unique: |
|
4527 assumes nt1: "next_th s th cs th1" |
|
4528 and nt2: "next_th s th cs th2" |
|
4529 shows "th1 = th2" |
|
4530 using assms by (unfold next_th_def, auto) |
4678 |
4531 |
4679 lemma holding_next_thI: |
4532 lemma holding_next_thI: |
4680 assumes "holding s th cs" |
4533 assumes "holding s th cs" |
4681 and "length (wq s cs) > 1" |
4534 and "length (wq s cs) > 1" |
4682 obtains th' where "next_th s th cs th'" |
4535 obtains th' where "next_th s th cs th'" |
4702 using pip_e assms |
4555 using pip_e assms |
4703 by (induct, auto) |
4556 by (induct, auto) |
4704 |
4557 |
4705 end |
4558 end |
4706 |
4559 |
4707 end |
4560 context valid_trace |
4708 |
4561 begin |
|
4562 |
|
4563 lemma create_pre: |
|
4564 assumes stp: "step s e" |
|
4565 and not_in: "th \<notin> threads s" |
|
4566 and is_in: "th \<in> threads (e#s)" |
|
4567 obtains prio where "e = Create th prio" |
|
4568 proof - |
|
4569 from assms |
|
4570 show ?thesis |
|
4571 proof(cases) |
|
4572 case (thread_create thread prio) |
|
4573 with is_in not_in have "e = Create th prio" by simp |
|
4574 from that[OF this] show ?thesis . |
|
4575 next |
|
4576 case (thread_exit thread) |
|
4577 with assms show ?thesis by (auto intro!:that) |
|
4578 next |
|
4579 case (thread_P thread) |
|
4580 with assms show ?thesis by (auto intro!:that) |
|
4581 next |
|
4582 case (thread_V thread) |
|
4583 with assms show ?thesis by (auto intro!:that) |
|
4584 next |
|
4585 case (thread_set thread) |
|
4586 with assms show ?thesis by (auto intro!:that) |
|
4587 qed |
|
4588 qed |
|
4589 |
|
4590 lemma subtree_tRAG_thread: |
|
4591 assumes "th \<in> threads s" |
|
4592 shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R") |
|
4593 proof - |
|
4594 have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4595 by (unfold tRAG_subtree_eq, simp) |
|
4596 also have "... \<subseteq> ?R" |
|
4597 proof |
|
4598 fix x |
|
4599 assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
4600 then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto |
|
4601 from this(2) |
|
4602 show "x \<in> ?R" |
|
4603 proof(cases rule:subtreeE) |
|
4604 case 1 |
|
4605 thus ?thesis by (simp add: assms h(1)) |
|
4606 next |
|
4607 case 2 |
|
4608 thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) |
|
4609 qed |
|
4610 qed |
|
4611 finally show ?thesis . |
|
4612 qed |
|
4613 |
|
4614 lemma readys_root: |
|
4615 assumes "th \<in> readys s" |
|
4616 shows "root (RAG s) (Th th)" |
|
4617 proof - |
|
4618 { fix x |
|
4619 assume "x \<in> ancestors (RAG s) (Th th)" |
|
4620 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
4621 from tranclD[OF this] |
|
4622 obtain z where "(Th th, z) \<in> RAG s" by auto |
|
4623 with assms(1) have False |
|
4624 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
|
4625 by (fold wq_def, blast) |
|
4626 } thus ?thesis by (unfold root_def, auto) |
|
4627 qed |
|
4628 |
|
4629 lemma readys_in_no_subtree: |
|
4630 assumes "th \<in> readys s" |
|
4631 and "th' \<noteq> th" |
|
4632 shows "Th th \<notin> subtree (RAG s) (Th th')" |
|
4633 proof |
|
4634 assume "Th th \<in> subtree (RAG s) (Th th')" |
|
4635 thus False |
|
4636 proof(cases rule:subtreeE) |
|
4637 case 1 |
|
4638 with assms show ?thesis by auto |
|
4639 next |
|
4640 case 2 |
|
4641 with readys_root[OF assms(1)] |
|
4642 show ?thesis by (auto simp:root_def) |
|
4643 qed |
|
4644 qed |
|
4645 |
|
4646 lemma not_in_thread_isolated: |
|
4647 assumes "th \<notin> threads s" |
|
4648 shows "(Th th) \<notin> Field (RAG s)" |
|
4649 proof |
|
4650 assume "(Th th) \<in> Field (RAG s)" |
|
4651 with dm_RAG_threads and rg_RAG_threads assms |
|
4652 show False by (unfold Field_def, blast) |
|
4653 qed |
|
4654 |
|
4655 lemma next_th_holding: |
|
4656 assumes nxt: "next_th s th cs th'" |
|
4657 shows "holding (wq s) th cs" |
|
4658 proof - |
|
4659 from nxt[unfolded next_th_def] |
|
4660 obtain rest where h: "wq s cs = th # rest" |
|
4661 "rest \<noteq> []" |
|
4662 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4663 thus ?thesis |
|
4664 by (unfold cs_holding_def, auto) |
|
4665 qed |
|
4666 |
|
4667 lemma next_th_waiting: |
|
4668 assumes nxt: "next_th s th cs th'" |
|
4669 shows "waiting (wq s) th' cs" |
|
4670 proof - |
|
4671 from nxt[unfolded next_th_def] |
|
4672 obtain rest where h: "wq s cs = th # rest" |
|
4673 "rest \<noteq> []" |
|
4674 "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto |
|
4675 from wq_distinct[of cs, unfolded h] |
|
4676 have dst: "distinct (th # rest)" . |
|
4677 have in_rest: "th' \<in> set rest" |
|
4678 proof(unfold h, rule someI2) |
|
4679 show "distinct rest \<and> set rest = set rest" using dst by auto |
|
4680 next |
|
4681 fix x assume "distinct x \<and> set x = set rest" |
|
4682 with h(2) |
|
4683 show "hd x \<in> set (rest)" by (cases x, auto) |
|
4684 qed |
|
4685 hence "th' \<in> set (wq s cs)" by (unfold h(1), auto) |
|
4686 moreover have "th' \<noteq> hd (wq s cs)" |
|
4687 by (unfold h(1), insert in_rest dst, auto) |
|
4688 ultimately show ?thesis by (auto simp:cs_waiting_def) |
|
4689 qed |
|
4690 |
|
4691 lemma next_th_RAG: |
|
4692 assumes nxt: "next_th (s::event list) th cs th'" |
|
4693 shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s" |
|
4694 using vt assms next_th_holding next_th_waiting |
|
4695 by (unfold s_RAG_def, simp) |
|
4696 |
|
4697 end |
|
4698 |
|
4699 end |