Correctness.thy
changeset 76 b6ea51cd2e88
parent 73 b0054fb0d1ce
child 82 c0a4e840aefe
equal deleted inserted replaced
75:2aa37de77f31 76:b6ea51cd2e88
   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'"