--- a/Implementation.thy	Fri Jul 14 15:08:39 2017 +0100
+++ b/Implementation.thy	Tue Jul 18 14:46:14 2017 +0100
@@ -70,7 +70,7 @@
 *}
 
 lemma cp_rec_tG:
-  "cp s th = Max ({preced th s} \<union> cprecs (children (tG s) th) s)"
+  "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)"
 proof -
   have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp)
   have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = 
@@ -101,6 +101,8 @@
 context valid_trace_set
 begin
 
+find_theorems RAG "(e#s)" "_ = _"
+
 text {* (* ddd *)
   The following two lemmas confirm that @{text "Set"}-operation
   only changes the precedence of the initiating thread (or actor)
@@ -300,6 +302,7 @@
   @{text th} and then adding in one edge from @{text cs} to @{text taker}.
   The added edge represents acquisition of @{text cs} by @{text taker}.
 *}
+
 lemma RAG_s:
   "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union>
                                          {(Cs cs, Th taker)}"
@@ -380,6 +383,7 @@
   are not changed , additionally, since the @{text V}-operation does not change any precedence, 
   the @{text "cp"}-value of such threads are not changed.
 *}
+
 lemma cp_kept:
   assumes "th1 \<notin> {th, taker}"
   shows "cp (e#s) th1 = cp s th1"
@@ -396,12 +400,12 @@
   the @{text cp}-values for @{text th} and @{text taker}.
 *}
 
-lemma t1: "taker \<notin> children (tG (e#s)) th"
+lemma "taker \<notin> children (tG (e#s)) th"
   by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp
           subtree_ancestorsI taker_ready_es vat_es.root_readys_tG)
   
 
-lemma t2: "th \<notin> children (tG (e#s)) taker"
+lemma "th \<notin> children (tG (e#s)) taker"
   by (metis children_subtree empty_iff  neq_taker_th root_def 
          subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG)
   
@@ -511,11 +515,15 @@
   By combining @{thm cp_kept_1} and @{thm cp_kept_2}, it is shown that no @{text cp}-recalculation 
   is needed at all for this sub-case of @{text V}-operation.
 *}
-lemma eq_cp:
+lemma eq_cp_pre:
   shows "cp (e#s) th' = cp s th'"
   using cp_kept_1 cp_kept_2
   by (cases "th' = th", auto)
 
+lemma eq_cp: 
+  shows "cp (e#s) = cp s"
+  by (rule ext, unfold eq_cp_pre, simp)
+
 end
 
 section {* The @{term P} operation *} 
@@ -588,38 +596,30 @@
 begin
 
 text {*
-  According to @{thm RAG_es}, the only change to @{text RAG} by
-  the @{text P}-operation is the addition of the edge @{text "(Cs cs, Th th)"}, 
-  representing the newly acquisition of @{text cs} by @{text th}. 
-  The following lemma shows that this newly added edge only change the sub-tree
-  of @{text th}, the reason is that @{text th} is in no other sub-trees.
+  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}
+  by the @{text P}-action, namely @{text "(Cs cs, Th th)"},
+  does not bring any new thread into graph @{text tG}, because 
+  the node of @{text cs} is isolated from the original @{text RAG}.
 *}
 
-lemma subtree_kept:
-  assumes "th' \<noteq> th"
-  shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
-proof(unfold RAG_es, rule subtree_insert_next)
-  from in_no_others_subtree[OF assms] 
-  show "Th th \<notin> subtree (RAG s) (Th th')" .
+lemma tG_es: "tG (e # s) = tG s"
+proof -
+  have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"
+    by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding)
+  show ?thesis
+    apply (unfold tG_def_tRAG tRAG_alt_def RAG_es)
+    by (auto)
 qed
 
 text {*
-  With both sub-tree and precdences unchanged, the @{text cp}-values of 
-  threads other than @{text th} are not changed. Therefore, the 
-  only recalculation of @{text cp}-value happens at @{text th}, and 
-  the recalculation can be done locally using the 
-  {\em local recalculation principle}, because the @{text cp}-values
-  of its children are not changed.
+  Since both @{text tG} and precedences are not changed, it is easy
+  to show that all @{text cp}-value are not changed, therefore, 
+  no @{text cp}-recalculation is needed:
 *}
-lemma cp_kept: 
-  assumes "th' \<noteq> th"
-  shows "cp (e#s) th' = cp s th'"
-proof -
-  have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
-        (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
-        by (unfold preced_kept subtree_kept[OF assms], simp)
-  thus ?thesis by (unfold cp_alt_def, simp)
-qed
+
+lemma cp_kept: "cp (e#s) = cp s"
+  by (rule ext, simp add: cp_alt_def2 preced_kept tG_es)
 
 end
 
@@ -1011,6 +1011,7 @@
   the @{text cp}-values of all other threads are not changed. 
   The reasoning is almost the same as that of @{term Create}:
 *}
+
 lemma eq_cp:
   assumes neq_th: "th' \<noteq> th"
   shows "cp (e#s) th' = cp s th'"
@@ -1032,5 +1033,6 @@
 
 end
 
+
 end
 

--- a/Journal/Paper.thy	Fri Jul 14 15:08:39 2017 +0100
+++ b/Journal/Paper.thy	Tue Jul 18 14:46:14 2017 +0100
@@ -2012,10 +2012,8 @@
   @{text "th'"} can be done independently and also done locally by only 
   looking at the children: according to \eqref{fone} and \eqref{ftwo} 
   none of the @{text cprecs} of the children 
-  changes, just the children-sets changes by a @{text V}-event. This 
-  in turn means the recalculation of 
-  @{text cprec} for @{text th} and @{text "th'"} terminates since
-  none of the  @{text cprec} need the be recalculated.
+  changes, just the children-sets changes by a @{text V}-event. 
+  
 
 *}
 
@@ -2024,12 +2022,12 @@
   In the other case where there is no thread that takes over @{text cs}, 
   we can show how
   to recalculate the @{text RAG} and also show that no current precedence needs
-  to be recalculated.
+  to be recalculated for any thread @{text "th''"}.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm (concl) valid_trace_v_e.RAG_s}\\
-  @{thm (concl) valid_trace_v_e.eq_cp}
+  @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"}
   \end{tabular}
   \end{isabelle}
   *}
@@ -2045,14 +2043,19 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm valid_trace_p_h.RAG_es}\\
-  %@ { thm valid_trace_p_h.eq_cp}
+  @{thm (concl) valid_trace_p_h.RAG_es}\\
+  @{term "\<forall>th''. cprec (e#s) th'' = cprec s th''"}
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  This means we need to add a holding edge to the @{text RAG} and no
-  current precedence needs to be recalculated.*} 
+  \noindent This means we need to add a holding edge to the @{text
+  RAG}. However, note 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 
+  of any thread @{text "th''"} is needed.
+
+*} 
 
 text {*
   \noindent
@@ -2060,8 +2063,8 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  HERE %@ {thm[mode=IfThen] eq_cp}
+  %@ {thm (concl) valid_trace_p_hRAG_s}\\
+  %@ {thm (concl) valid_trace_p_h.eq_cp}
   \end{tabular}
   \end{isabelle}
 

Binary file journal.pdf has changed