519 @{term "V"} operations relate to the running threads in the states |
521 @{term "V"} operations relate to the running threads in the states |
520 @{term s} and @{term "t @ s"}. The lemma shows that if a thread's |
522 @{term s} and @{term "t @ s"}. The lemma shows that if a thread's |
521 @{term "P"}-count equals its @{term "V"}-count (which means it no |
523 @{term "P"}-count equals its @{term "V"}-count (which means it no |
522 longer has any resource in its possession), it cannot be a running |
524 longer has any resource in its possession), it cannot be a running |
523 thread. |
525 thread. |
524 |
526 |
525 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
527 (* eee *) |
526 The key is the use of @{thm eq_pv_dependants} to derive the |
528 The proof is by contradiction: |
527 emptiness of @{text th'}s @{term dependants}-set from the balance of |
529 If @{text th'} is running, it can be derived that @{text "th' = th"} which |
528 its @{term P} and @{term V} counts. From this, it can be shown |
530 is in contradiction with the assume @{text "th' \<noteq> th"}. |
529 @{text th'}s @{term cp}-value equals to its own precedence. |
531 |
530 |
532 The derivation of @{text "th' = th"} uses @{thm preced_unique}, according to which |
531 On the other hand, since @{text th'} is running, by @{thm |
533 we need to show the @{text th'} and @{text th} have the same precedence. The proof |
532 running_preced_inversion}, its @{term cp}-value equals to the |
534 of this is based on the combination of the following two facts: |
533 precedence of @{term th}. |
535 |
534 |
536 From @{thm vat_t.detached_intro} and assume |
535 Combining the above two resukts we have that @{text th'} and @{term |
537 @{text "cntP (t@s) th' = cntV (t@s) th'"} it can be derived that |
536 th} have the same precedence. By uniqueness of precedences, we have |
538 @{text th'} is detached. From this and @{thm detached_cp_preced} |
537 @{text "th' = th"}, which is in contradiction with the assumption |
539 it following the precedence of @{text th'} equals to its own @{text cp}-value. |
538 @{text "th' \<noteq> th"}. |
540 |
|
541 Since @{text th'} is running, from this and @{thm |
|
542 running_preced_inversion}, the precedence of @{text th'} equals to |
|
543 the precedence of @{term th}. |
|
544 |
|
545 By combining the above two results we have that @{text th'} and @{term |
|
546 th} have the same precedence. |
539 |
547 |
540 *} |
548 *} |
541 |
549 |
542 lemma eq_pv_blocked: (* ddd *) |
550 lemma eq_pv_blocked: (* ddd *) |
543 assumes neq_th': "th' \<noteq> th" |
551 assumes neq_th': "th' \<noteq> th" |
565 by (simp add: detached_cp_preced eq_pv vat_t.detached_intro) |
573 by (simp add: detached_cp_preced eq_pv vat_t.detached_intro) |
566 -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion}, |
574 -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion}, |
567 its @{term cp}-value equals @{term "preced th s"}, |
575 its @{term cp}-value equals @{term "preced th s"}, |
568 which equals to @{term "?R"} by simplification: *} |
576 which equals to @{term "?R"} by simplification: *} |
569 also have "... = ?R" |
577 also have "... = ?R" |
570 thm running_preced_inversion |
|
571 using running_preced_inversion[OF otherwise] by simp |
578 using running_preced_inversion[OF otherwise] by simp |
572 finally show ?thesis . |
579 finally show ?thesis . |
573 qed |
580 qed |
574 qed (auto simp: th'_in th_kept) |
581 qed (auto simp: th'_in th_kept) |
575 with `th' \<noteq> th` show ?thesis by simp |
582 with `th' \<noteq> th` show ?thesis by simp |