equal
deleted
inserted
replaced
976 insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric]) |
976 insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric]) |
977 by auto |
977 by auto |
978 from th_kept have "th \<in> threads (t@s)" by auto |
978 from th_kept have "th \<in> threads (t@s)" by auto |
979 from th_chain_to_ready[OF vt_t this] and not_ready |
979 from th_chain_to_ready[OF vt_t this] and not_ready |
980 obtain th' where th'_in: "th' \<in> readys (t@s)" |
980 obtain th' where th'_in: "th' \<in> readys (t@s)" |
981 and dp: "(Th th, Th th') \<in> (depend (t @ s))\<^sup>+" by auto |
981 and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto |
982 have "th' \<in> runing (t@s)" |
982 have "th' \<in> runing (t@s)" |
983 proof - |
983 proof - |
984 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
984 have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" |
985 proof - |
985 proof - |
986 have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) = |
986 have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) = |
1019 show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))" |
1019 show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))" |
1020 by (auto intro:finite_subset) |
1020 by (auto intro:finite_subset) |
1021 next |
1021 next |
1022 from dp |
1022 from dp |
1023 have "th \<in> dependants (wq (t @ s)) th'" |
1023 have "th \<in> dependants (wq (t @ s)) th'" |
1024 by (unfold cs_dependants_def, auto simp:eq_depend) |
1024 by (unfold cs_dependants_def, auto simp:eq_RAG) |
1025 thus "preced th (t @ s) \<in> |
1025 thus "preced th (t @ s) \<in> |
1026 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')" |
1026 (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')" |
1027 by auto |
1027 by auto |
1028 qed |
1028 qed |
1029 moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))" |
1029 moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))" |