--- a/Correctness.thy Fri Oct 07 14:05:08 2016 +0100
+++ b/Correctness.thy Fri Oct 07 21:15:35 2016 +0100
@@ -501,13 +501,17 @@
precedence in the whole system.
*}
lemma running_preced_inversion:
- assumes running': "th' \<in> running (t@s)"
- shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+ assumes running': "th' \<in> running (t @ s)"
+ shows "cp (t @ s) th' = preced th s"
proof -
- have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
- by (unfold running_def, auto)
- also have "\<dots> = ?R"
- by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms
+ unfolding running_def by simp
+ also have "... = Max (cp (t @ s) ` threads (t @ s))"
+ using vat_t.max_cp_readys_threads .
+ also have "... = cp (t @ s) th"
+ using th_cp_max .
+ also have "\<dots> = preced th s"
+ using th_cp_preced .
finally show ?thesis .
qed