equal
deleted
inserted
replaced
459 by (insert th_kept max_kept, auto) |
459 by (insert th_kept max_kept, auto) |
460 |
460 |
461 lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" |
461 lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" |
462 (is "?L = ?R") |
462 (is "?L = ?R") |
463 proof - |
463 proof - |
464 have "?L = cpreced (t@s) (wq (t@s)) th" |
464 have "?L = cpreced (wq (t@s)) (t@s) th" |
465 by (unfold cp_eq_cpreced, simp) |
465 by (unfold cp_eq_cpreced, simp) |
466 also have "\<dots> = ?R" |
466 also have "\<dots> = ?R" |
467 proof(unfold cpreced_def) |
467 proof(unfold cpreced_def) |
468 show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) = |
468 show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) = |
469 Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" |
469 Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" |