--- 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
 

--- a/Journal/Paper.thy	Fri Oct 07 14:05:08 2016 +0100
+++ b/Journal/Paper.thy	Fri Oct 07 21:15:35 2016 +0100
@@ -403,7 +403,7 @@
   We also use the abbreviation 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  ???%%@  { thm  preceds_def}
+  @{abbrev "preceds ths s"}
   \end{isabelle}
 
   \noindent
@@ -1087,6 +1087,17 @@
   \begin{center}
   @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
   \end{center}
+
+  \noindent
+  We also know that this is equal to all threads, that is
+
+  \begin{center}
+  @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
+  \end{center}
+
+  \noindent
+  But the maximum of all threads is the @{term "cp"} of @{text "th"},
+  which is the @{term preced} of @{text th}.
   \end{proof}
 
   @{thm "th_blockedE_pretty"} -- thm-blockedE??

--- a/PIPBasics.thy	Fri Oct 07 14:05:08 2016 +0100
+++ b/PIPBasics.thy	Fri Oct 07 21:15:35 2016 +0100
@@ -3629,8 +3629,13 @@
   are disjoint.
 *}
 
+lemma subtree_RAG_tG: 
+  shows "subtree (tG s) th = {th'. Th th' \<in> subtree (RAG s) (Th th)}"
+  using subtree_tG_tRAG threads_set_eq by auto
+
+
 lemma threads_alt_def:
-  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+  "threads s = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
     (is "?L = ?R")
 proof -
   { fix th1
@@ -3658,6 +3663,10 @@
   } ultimately show ?thesis by auto
 qed
 
+lemma threads_alt_def1:
+  shows "(threads s) = (\<Union> th \<in> readys s. subtree (tG s) th)"
+unfolding threads_alt_def subtree_RAG_tG  ..
+
 lemma readys_subtree_disjoint:
   assumes "th1 \<in> readys s"
   and "th2 \<in> readys s"
@@ -3812,27 +3821,24 @@
   over the union of subtrees, the following equation can be derived:
 *}
 
-lemma max_cp_readys_max_preced:
+thm the_preced_def cpreceds_def
+
+lemma max_cp_readys_max_preced_tG:
   shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
 proof(cases "readys s = {}")
   case False
   have "?R = 
-    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-    by (simp add: threads_alt_def)  
-  also have "... = 
-    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
-          by (unfold image_UN, simp)
-  also have "... = 
-    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
+    Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))"
+    by (simp add: threads_alt_def1)  
+  also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) "
+    by (unfold image_UN, simp)
+  also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" 
   proof(rule Max_UNION)
-    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
-                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
-                        using finite_subtree_threads by auto
+    show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M"
+      using fsbttGs.finite_subtree by auto
   qed (auto simp:False subtree_def finite_readys)
-  also have "... = 
-     Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` 
-                        readys s)" 
-      by (simp add: image_comp)
+  also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)"
+    by (simp add: image_comp)
   also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
   proof -
     have "(?f ` ?A) = (?g ` ?A)"
@@ -3840,20 +3846,21 @@
       fix th1 
       assume "th1 \<in> ?A"
       thus "?f th1 = ?g th1"
-        by (unfold cp_alt_def, simp)
+        by (unfold cp_alt_def2, simp)
     qed
     thus ?thesis by simp
   qed
   finally show ?thesis by simp
 qed (auto simp:threads_alt_def)
 
+
 text {*
-  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
+  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
   and @{thm max_cp_eq}:
 *}
 lemma max_cp_readys_threads:
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
-    using max_cp_readys_max_preced max_cp_eq by auto
+    using max_cp_readys_max_preced_tG max_cp_eq by auto
 
 end
 

Binary file journal.pdf has changed