501 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
501 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
502 finally show ?thesis . |
502 finally show ?thesis . |
503 qed |
503 qed |
504 |
504 |
505 text {* |
505 text {* |
506 The following lemma shows how the counting of |
506 |
507 @{term "P"} and @{term "V"} operations affects |
507 The following lemma shows how the counters for @{term "P"} and |
508 the running state of threads in @{term t}. |
508 @{term "V"} operations relate to the running threads in the states |
509 |
509 @{term s} and @{term "t @ s"}. The lemma shows that if a thread's |
510 The lemma shows that if a thread's @{term "P"}-count equals |
510 @{term "P"}-count equals its @{term "V"}-count (which means it no |
511 its @{term "V"}-count (which means it no longer has any |
511 longer has any resource in its possession), it cannot be a running |
512 resource in its possession), it can not be in running thread. |
512 thread. |
513 |
513 |
514 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
514 The proof is by contraction with the assumption @{text "th' \<noteq> th"}. |
515 The key is the use of @{thm count_eq_dependants} |
515 The key is the use of @{thm count_eq_dependants} to derive the |
516 to derive the emptiness of @{text th'}s @{term dependants}-set |
516 emptiness of @{text th'}s @{term dependants}-set from the balance of |
517 from the balance of its @{term P} @{term V} counts. |
517 its @{term P} and @{term V} counts. From this, it can be shown |
518 From this, it can be shown @{text th'}s @{term cp}-value |
518 @{text th'}s @{term cp}-value equals to its own precedence. |
519 equals to its own precedence. |
519 |
520 |
520 On the other hand, since @{text th'} is running, by @{thm |
521 On the other hand, since @{text th'} is running, by |
521 runing_preced_inversion}, its @{term cp}-value equals to the |
522 @{thm runing_preced_inversion}, its @{term cp}-value |
522 precedence of @{term th}. |
523 equals to the precedence of @{term th}. |
523 |
524 |
524 Combining the above two resukts we have that @{text th'} and @{term |
525 Combining the above two we have that @{text th'} and |
525 th} have the same precedence. By uniqueness of precedences, we have |
526 @{term th} have the same precedence. By uniqueness of precedence, we |
526 @{text "th' = th"}, which is in contradiction with the assumption |
527 have @{text "th' = th"}, which is in contradiction with the |
527 @{text "th' \<noteq> th"}. |
528 assumption @{text "th' \<noteq> th"}. |
528 |
529 *} |
529 *} |
530 |
530 |
531 lemma eq_pv_blocked: (* ddd *) |
531 lemma eq_pv_blocked: (* ddd *) |
532 assumes neq_th': "th' \<noteq> th" |
532 assumes neq_th': "th' \<noteq> th" |
533 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
533 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |