equal
deleted
inserted
replaced
499 The following lemmas shows that the @{term cp}-value |
499 The following lemmas shows that the @{term cp}-value |
500 of the blocking thread @{text th'} equals to the highest |
500 of the blocking thread @{text th'} equals to the highest |
501 precedence in the whole system. |
501 precedence in the whole system. |
502 *} |
502 *} |
503 lemma running_preced_inversion: |
503 lemma running_preced_inversion: |
504 assumes running': "th' \<in> running (t@s)" |
504 assumes running': "th' \<in> running (t @ s)" |
505 shows "cp (t@s) th' = preced th s" (is "?L = ?R") |
505 shows "cp (t @ s) th' = preced th s" |
506 proof - |
506 proof - |
507 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms |
507 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms |
508 by (unfold running_def, auto) |
508 unfolding running_def by simp |
509 also have "\<dots> = ?R" |
509 also have "... = Max (cp (t @ s) ` threads (t @ s))" |
510 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
510 using vat_t.max_cp_readys_threads . |
|
511 also have "... = cp (t @ s) th" |
|
512 using th_cp_max . |
|
513 also have "\<dots> = preced th s" |
|
514 using th_cp_preced . |
511 finally show ?thesis . |
515 finally show ?thesis . |
512 qed |
516 qed |
513 |
517 |
514 text {* |
518 text {* |
515 |
519 |