diff -r 32985f93e845 -r 2dd47ea013ac Implementation.thy
--- 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