--- a/Implementation.thy	Tue Jul 18 14:46:14 2017 +0100
+++ b/Implementation.thy	Wed Aug 02 13:18:14 2017 +0100
@@ -594,7 +594,7 @@
 
 context valid_trace_p_h
 begin
-
+       
 text {*
   It can be shown that the @{text tG} is not changed by 
   the @{text P}-action. The reason is that the edge added to @{text RAG}
@@ -603,6 +603,8 @@
   the node of @{text cs} is isolated from the original @{text RAG}.
 *}
 
+thm RAG_es
+
 lemma tG_es: "tG (e # s) = tG s"
 proof -
   have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"
@@ -640,12 +642,19 @@
   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
   using RAG_tRAG_transfer[OF RAG_es cs_held] .
 
+
+lemma tG_ancestors_tRAG_refute:
+  assumes "th'' \<notin> ancestors (tG (e#s)) th"
+  shows "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
+  using assms using node.inject(1) tRAG_ancestorsE_tG by force 
+
 text {*
   The following lemma shows only the ancestors of @{text th} (the initiating 
   thread of the @{text P}-operation) may possibly 
   need a @{text cp}-recalculation. All other threads (including @{text th} itself)
   do not need @{text cp}-recalculation. 
 *}
+
 lemma cp_kept:
   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
   shows "cp (e#s) th'' = cp s th''"
@@ -681,6 +690,12 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
+lemma cp_kept_tG:
+  assumes "th'' \<notin> ancestors (tG (e#s)) th"
+  shows "cp (e#s) th'' = cp s th''"
+  using cp_kept tG_ancestors_tRAG_refute assms
+  by blast
+  
 text {*
   Lemma @{thm cp_kept} means that the @{text cp}-recalculation starts from the parent of @{text th},
   going upwards along the chain of ancestors until one root (which is a thread 
@@ -817,6 +832,7 @@
   qed
 qed
 
+
 text {*
   The following lemma is about the possible early termination of 
   @{text cp}-recalculation. The lemma says that @{text cp}-recalculation 
@@ -843,6 +859,13 @@
   show ?thesis by metis
 qed
 
+lemma cp_up_tG:
+  assumes "th' \<in> ancestors (tG (e#s)) th"
+  and "cp (e#s) th' = cp s th'"
+  and "th'' \<in> ancestors (tG (e#s)) th'"
+  shows "cp (e#s) th'' = cp s th''"
+  using assms cp_up ancestors_tG_tRAG by blast   
+
 end
 
 text {* 

--- a/Journal/Paper.thy	Tue Jul 18 14:46:14 2017 +0100
+++ b/Journal/Paper.thy	Wed Aug 02 13:18:14 2017 +0100
@@ -2049,7 +2049,7 @@
   \end{isabelle}
 
   \noindent This means we need to add a holding edge to the @{text
-  RAG}. However, note while the @{text RAG} changes the corresponding
+  RAG}. However, note that while the @{text RAG} changes the corresponding
   @{text TDG} does not change. Together with the fact that the
   precedences of all threads are unchanged, no @{text cprec} value is
   changed. Therefore, no recalucation of the @{text cprec} value 
@@ -2063,8 +2063,9 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm (concl) valid_trace_p_hRAG_s}\\
-  %@ {thm (concl) valid_trace_p_h.eq_cp}
+  @{thm (concl) valid_trace_p_w.RAG_es}\\
+  @{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept} @{text "then"}
+  @{thm (concl) valid_trace_p_w.cp_kept_tG}
   \end{tabular}
   \end{isabelle}
 

Binary file journal.pdf has changed