
diff -r abe117821c32 -r da27bece9575 Implementation.thy
--- a/Implementation.thy	Fri Jun 09 15:08:54 2017 +0100
+++ b/Implementation.thy	Fri Jun 23 00:27:16 2017 +0100
@@ -2,6 +2,13 @@
 imports PIPBasics
 begin
 
+
+(*
+  The use of dependants has been abandoned. Through a series of lemma 
+  named xxx_alt_def, lemma originally expressed using dependants 
+  is now expressed in terms of RAG, tRAG and tG.
+*)
+
 text {*
 
   This file contains lemmas used to guide the recalculation of current
@@ -9,39 +16,83 @@
   which is the most tricky part in the implementation of PIP.
 
   Following convention, lemmas are grouped into locales corresponding to
-  system operations, each explained in a separate section. *}
+  system operations, each explained in a separate section. To understand the relevant 
+  materials, one needs some acquaintance with locales, which are 
+  used to as contexts for lemmas to situate, where lemmas with the same assumptions
+  are grouped under the same locale.
+
+  Locale @{text "valid_trace s"} assumes that @{text "s"} is a valid trace (or state)
+  of PIP. Lemmas talking about general properties of valid states can be put under this 
+  locale. The locale @{text "valid_trace_e s e"} is an extension of @{text valid_trace}
+  by introducing an event @{text e} and assuming @{text "e#s"} is also valid state. 
+  The purpose of @{text valid_trace_e} is to set a context to investigate 
+  one step execution of PIP, where @{text e} is a fixed but arbitrary
+  action legitimate to happen under state @{text "s"}. General Properties about 
+  one step action of PIP are grouped under this locale.
+
+  @{text "valid_trace_e"} is further extended to accommodate specific actions. For example,
+  @{text "valid_trace_create s e th prio"} further assumes that the 
+  @{text "e"} action is @{text "Create th prio"}, and 
+  @{text "valid_trace_p s e th cs"} assumes that @{text "e"} is @{text "P th cs"}, etc.
 
-text {*
-  The following two lemmas are general about any valid system state, 
-  but are used in the derivation in more specific system operations. 
+  Since the recalculation of current precedence happens only when certain actions 
+  are taken, it is natural to put the lemmas about recalculation under the respective 
+  locales. In the following, each section corresponds one particular action of PIP, which,
+  in turn, is developed under the locale corresponding to the specific action.
+
+  By @{text cp_alt_def3}, the @{text cp}-value of one thread @{text th} is determined 
+  uniquely by static precedences of threads in its @{text "RAG"}-subtree 
+  (or @{text tRAG}-subtree, @{text "tG"}-subtree). Because of this, the decision where 
+  recalculation is needed is based on the change of @{text RAG} (@{text tRAG} or @{text tG})
+  as well the precedence of threads. Since most of PIP actions (except the @{text Set}-operation) 
+  only changes the formation of @{text RAG}, therefore, for non-@{text Set} operations,
+  if the change of @{text RAG} does not affect the subtree
+  of one thread, its @{text cp}-value may not change. 
+
+  In the following, the section corresponding to non-@{text Set} operations 
+  usually contain lemmas showing the subtrees of certain kind of threads are 
+  not changed. The proof of such lemmas is obvious based on the lemmas about the
+  change of @{text RAG}, which have already been derived in theory @{text PIPBasics}
+  all under the name @{text "RAG_es"} in the locale corresponding to different PIP 
+  operations.
 *}
 
+section {* The local recalculation principle for @{text cp}-value *}
+
+definition "cprecs Ths s = cp s ` Ths"
+
 context valid_trace
 begin
 
-lemma readys_root:
-  assumes "th \<in> readys s"
-  shows "root (RAG s) (Th th)"
-  unfolding root_def ancestors_def
-  using readys_RAG assms
-by (metis Collect_empty_eq Domain.DomainI trancl_domain)
+text {*
+  To minimize the cost of the recalculation, we derived the following localized alternative 
+  definition of @{term cp}:
+*}
 
-lemma readys_in_no_subtree:
-  assumes "th \<in> readys s"
-  and "th' \<noteq> th"
-  shows "Th th \<notin> subtree (RAG s) (Th th')" 
-proof
-   assume "Th th \<in> subtree (RAG s) (Th th')"
-   thus False
-   proof(cases rule:subtreeE)
-      case 1
-      with assms show ?thesis by auto
-   next
-      case 2
-      with readys_root[OF assms(1)]
-      show ?thesis by (auto simp:root_def)
-   qed
-qed
+lemma cp_rec_tG:
+  "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) = 
+                cp s ` children (tG s) th"
+                  apply (unfold tRAG_def_tG) 
+                  apply (subst fmap_children)
+                  apply (rule injI, simp)
+                  by (unfold image_comp, simp)
+  have [simp]: "preceds {th} s = {the_preced s th}"
+    by (unfold the_preced_def, simp)
+  show ?thesis 
+    by (unfold cp_rec cprecs_def, simp add:the_preced_def)
+qed    
+
+text {*
+  According to this lemma, @{text cp}-value of one thread can be calculated by calling recursively 
+  the @{text cp} function on its @{text tG}-children. However, one thing to be noted is that
+  the lemma also means the recursive call needs not to descend into lower levels if the
+  @{text "cp"}-value of one child is not changed. In this way, the recalculation can be {\em localized}
+  to those thread with changed @{text cp}-value. This is the reason why this lemma
+  is called a {\em localized lemma}.
+*}
 
 end
 
@@ -73,11 +124,14 @@
 
 
 text {* (* ddd *)
-  Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"}
-  only affects those threads, which as @{text "Th th"} in their sub-trees.
-  
-  The proof of this lemma is simplified by using the alternative definition 
-  of @{text "cp"}. 
+  According to @{thm RAG_es}, the @{text RAG} is not changed by @{text Set}-operation.
+  Moreover, because @{text th} is the only thread with precedence changed by @{text Set}, 
+  for any subtree, if it does not contain @{text th}, there will be no precedence change inside
+  the subtree, which means the @{text cp}-value of the root thread is not changed. 
+  This means that the @{text "cp"}-value of one thread needs to be recalculated only
+  when the subtree rooted by the threads contains @{text "th"}.
+ 
+  This argument is encapsulated in the following lemma:
 *}
 
 lemma eq_cp_pre:
@@ -110,8 +164,8 @@
 qed
 
 text {*
-  The following lemma shows that @{term "th"} is not in the 
-  sub-tree of any other thread. 
+  However, the following lemma shows that @{term "th"} is not in the 
+  subtree of any thread except itself. 
 *}
 lemma th_in_no_subtree:
   assumes "th' \<noteq> th"
@@ -122,26 +176,39 @@
 qed
 
 text {* 
-  By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 
-  it is obvious that the change of priority only affects the @{text "cp"}-value 
-  of the initiating thread @{text "th"}.
+  Combining the above two lemmas, it is concluded that the 
+  recalculation of @{text "cp"}-value is needed only on @{text th}.
 *}
+
 lemma eq_cp:
   assumes "th' \<noteq> th"
   shows "cp (e#s) th' = cp s th'"
   by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
 
+text {* 
+  Under the local recalculation principle @{thm cp_rec_tG}, 
+  @{thm eq_cp} also means the recalculation of @{text cp} for @{text th}
+  can be done locally by inspecting only @{text th} and its children.
+*}
+
 end
 
 section {* The @{term V} operation *}
 
 text {*
-  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
+  The following locale @{text "valid_trace_v"} is the locale for @{text "V"}-operation in 
+  general. The recalculation of @{text cp}-value needs to consider two more sub-case, each
+  encapsulated into a sub-locale of @{text "valid_trace_v"}. But first, 
+  some general properties about the @{text V}-operation are derived:
 *}
 
 context valid_trace_v
 begin
 
+text {*
+  Because @{text th} is running in state @{text s}, it does not in waiting of 
+  any resource, therefore, it has no ancestor in @{text "RAG s"}:
+*}
 lemma ancestors_th: "ancestors (RAG s) (Th th) = {}"
 proof -
   from readys_root[OF th_ready_s]
@@ -149,6 +216,10 @@
   by (unfold root_def, simp)
 qed
 
+text {*
+  Since @{text th} is holding @{text cs} (the resource to be released by this @{text V}-operation),
+  the edge @{text "(Cs cs, Th th)"} represents this fact.
+*}
 lemma edge_of_th:
     "(Cs cs, Th th) \<in> RAG s" 
 proof -
@@ -157,6 +228,10 @@
     by (unfold s_RAG_def s_holding_abv, auto)
 qed
 
+text {*
+  Since @{text cs} is held by @{text th} which has no ancestors, 
+  @{text th} is the only ancestor of @{text cs}:
+*}
 lemma ancestors_cs: 
   "ancestors (RAG s) (Cs cs) = {Th th}"
 proof -
@@ -165,15 +240,11 @@
   from this[unfolded ancestors_th] show ?thesis by simp
 qed
 
-end
-
 text {*
-  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
-  which represents the case when there is another thread @{text "th'"}
-  to take over the critical resource released by the initiating thread @{text "th"}.
+  As already said, all operations except @{text Set} may change precedence. 
+  The following lemma confirms this fact of the @{text V}-operation:
 *}
-
-lemma (in valid_trace_v)
+lemma 
   the_preced_es: "the_preced (e#s) = the_preced s"
 proof
   fix th'
@@ -181,14 +252,35 @@
     by (unfold the_preced_def preced_def is_v, simp)
 qed
 
+end
+
+
+text {*
+  The following sub-locale @{text "valid_trace_v_n"} 
+  deals with one of the sub-cases of @{text V}, which corresponds to the 
+  situation where there is another thread @{text "taker"}
+  to take over the release resource @{text cs}.
+*}
+
 context valid_trace_v_n
 begin
 
+text {*
+  The following lemma shows the two edges in @{text "RAG s"} which 
+  links @{text cs} with @{text taker} and @{text th} to form a chain. 
+  The existence of this chain set the stage for the @{text V}-operation 
+  in question to happen.
+*}
 lemma sub_RAGs': 
   "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
   using waiting_taker holding_th_cs_s
   by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto)
 
+text {*
+  The following lemma shows that @{text taker} has only two the ancestors.
+  The reason for this is very simple: The chain starting from @{text taker}
+  stops at @{text th}, which, as shown by @{thm ancestors_th}, has no ancestor. 
+*}
 lemma ancestors_th': 
   "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 
 proof -
@@ -199,11 +291,36 @@
   thus ?thesis using ancestors_th ancestors_cs by auto
 qed
 
+text {*
+  By composing several existing results, the following lemma
+  make clear the change of @{text RAG} where there is a 
+  @{text taker} to take over the resource @{text cs}. 
+  More specifically, the lemma says the change of @{text RAG}
+  is by first removing the chain linking @{text taker}, @{text cs} and 
+  @{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)}"
  by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
 
+text {*
+  The above lemma @{thm RAG_s} shows the effect of the @{text V}-operation
+  on @{text RAG} is the removal of two edges followed by the addition of 
+  one edge. Based on this, the following lemma will show that 
+  the sub-trees of threads other than @{text th} and @{text taker} are unchanged.
+  The intuition behind this is rather simple: the edges added and removed are not
+  in these sub-trees. 
+
+  Formally, an edge is said to be outside of a sub-tree if its
+  end point is. Note that when a set of edges are represented as a binary relation, the
+  set of their end points is essentially range of the relation (formally defined 
+  as @{term Range}). Therefore, a set of edges (represented as a relation) 
+  are outside of a sub-tree if its @{text Range}-set does not intersect 
+  with the sub-tree.
+*}
+
 lemma subtree_kept: (* ddd *)
   assumes "th1 \<notin> {th, taker}"
   shows "subtree (RAG (e#s)) (Th th1) = 
@@ -211,6 +328,7 @@
 proof -
   let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})"
   let ?RAG'' = "?RAG' \<union> {(Cs cs, Th taker)}"
+  -- {* The first step is to show the deletion of edges does not change the sub-tree *}
   have "subtree ?RAG' (Th th1) = ?R" 
   proof(rule subset_del_subtree_outside)
     show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \<inter> subtree (RAG s) (Th th1) = {}"
@@ -218,7 +336,7 @@
       have "(Th th) \<notin> subtree (RAG s) (Th th1)"
       proof(rule subtree_refute)
         show "Th th1 \<notin> ancestors (RAG s) (Th th)"
-          by (unfold ancestors_th, simp)
+            by (unfold ancestors_th, simp)
       next
         from assms show "Th th1 \<noteq> Th th" by simp
       qed
@@ -231,38 +349,84 @@
       thus ?thesis by simp
      qed
   qed
+  -- {* The second step is to show the addition of edges does not change the sub-tree *}
   moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"
-  proof(rule subtree_insert_next)
-    show "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
-    proof(rule subtree_refute)
-      show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
+  proof(rule subset_insert_subtree_outside)
+    show "Range {(Cs cs, Th taker)} \<inter> 
+          subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1) = {}"
+    proof -
+     have "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
+     proof(rule subtree_refute)
+        show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
             (is "_ \<notin> ?R")
-      proof -
+        proof -
           have "?R \<subseteq> ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto)
           moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp
           ultimately show ?thesis by auto
-      qed
-    next
-      from assms show "Th th1 \<noteq> Th taker" by simp
+        qed
+     next
+        from assms show "Th th1 \<noteq> Th taker" by simp
+     qed
+     thus ?thesis by auto
     qed
   qed
   ultimately show ?thesis by (unfold RAG_s, simp)
 qed
 
+text {* 
+  The following lemma shows threads not involved in the @{text V}-operation (i.e.
+  threads other than @{text th} and @{text taker}) do not need to do any @{text cp}-recalculation.
+  The reason is simple: according to @{thm subtree_kept}, the sub-trees of such threads 
+  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"
     by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
 
+text {*
+  Lemma @{thm cp_kept} also means @{text cp}-recalculation is needed only for
+  @{text th} and @{text taker}. The following lemmas are to ensure that
+  the recalculation can done locally using {\em local recalculation principle}.
+  Since @{text taker} and @{text th} are the only threads with changed @{text cp}-values
+  and neither one can not be a child of the other, it can be concluded that 
+  neither of these two threads has children with changed @{text cp}-value.
+  It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating 
+  the @{text cp}-values for @{text th} and @{text taker}.
+*}
+
+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 "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)
+  
+
 end
 
-
+text {*
+  The following locale @{text valid_trace_v_e} deals with the second sub-case 
+  of @{text V}-operation, where there is no thread to take over the release 
+  resource @{text cs}.
+*}
 context valid_trace_v_e
 begin
 
+text {*
+  Since no thread to take over @{text cs}, only the edge representing 
+  the holding of @{text cs} by @{text th} needs to be removed:
+*}
 lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"
   by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
 
+text {*
+  Since @{text th} has no ancestors, 
+  the removal of the holding edge only affects the sub-tree of @{text th}:
+*}
 lemma subtree_kept:
   assumes "th1 \<noteq> th"
   shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)"
@@ -280,11 +444,31 @@
   qed
 qed
 
+text {*
+  From lemma @{thm subtree_kept} and the fact that no precedence are changed, it 
+  can be derived the @{text cp}-values of all threads (except @{text th})
+  are not changed and therefore need no recalculation:
+*}
 lemma cp_kept_1:
   assumes "th1 \<noteq> th"
   shows "cp (e#s) th1 = cp s th1"
     by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
 
+text {*
+  The next several lemmas try to show that even the @{text cp}-value of 
+  @{text th} needs not be recalculated.
+ 
+  Although the @{text V}-operation detaches the sub-tree of @{text cs}
+  from the sub-tree of @{text th}, the @{text cp}-value of @{text th} 
+  is not affected. The reason is given by the following lemma @{text subtree_cs}, which
+  says that the sub-tree of @{text cs} contains only itself. 
+
+  According to @{text subtree_cs}, the detached sub-tree contains no thread node and
+  therefore makes no contribution to the @{text cp}-value of @{text th}, 
+  so its removal does not affect the @{text cp}-value neither, as confirmed 
+  by the lemma @{text cp_kept_2}.
+*}
+
 lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}"
   (is "?L = ?R")
 proof -
@@ -308,7 +492,9 @@
   } ultimately show ?thesis by auto
 qed
 
-
+text {*
+  The following @{text "subtree_th"} is just a technical lemma.
+*}
 lemma subtree_th: 
   "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
 proof(unfold RAG_s, fold subtree_cs, rule forest_RAG.subtree_del_inside)
@@ -321,6 +507,10 @@
   shows "cp (e#s) th = cp s th" 
  by (unfold cp_alt_def subtree_th the_preced_es, auto)
 
+text {*
+  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:
   shows "cp (e#s) th' = cp s th'"
   using cp_kept_1 cp_kept_2
@@ -328,15 +518,37 @@
 
 end
 
+section {* The @{term P} operation *} 
 
-section {* The @{term P} operation *}
+text {*
+  Like @{text V}-operation, the treatment of @{text P}-operation is also divided into
+  tow sub-cases. If the requested resource is available, it is dealt with in
+  sub-locale @{text valid_trace_p_h}, otherwise, it is dealt with 
+  in sub-locale @{text valid_trace_p_w}. 
+*}
+
+text {*
+  But first, the following base locale @{text valid_trace_p} contains
+  some general properties of the @{text P}-operation:
+*}
 
 context valid_trace_p
 begin
 
+text {*
+  The following lemma shows that @{text th} is a root in the 
+  @{text RAG} graph, which means @{text th} has no ancestors in the graph.
+  The reason is that: since @{text th} is in running state, it is 
+  in ready state, which means it is not waiting for any resource, therefore, 
+  it has no outbound edge.  
+*}
 lemma root_th: "root (RAG s) (Th th)"
   by (simp add: ready_th_s readys_root)
 
+text {*
+  For the same reason as @{thm root_th}, @{text th} is not in 
+  the sub-tree of any thread other than @{text th}:
+*}
 lemma in_no_others_subtree:
   assumes "th' \<noteq> th"
   shows "Th th \<notin> subtree (RAG s) (Th th')"
@@ -352,6 +564,10 @@
   qed
 qed
 
+text {*
+  The following lemma confirms that the @{text P}-operation does not 
+  affect the precedence of any thread. 
+*}
 lemma preced_kept: "the_preced (e#s) = the_preced s"
 proof
   fix th'
@@ -361,10 +577,24 @@
 
 end
 
+text {*
+  The following locale @{text valid_trace_p_h} deals with the 
+  sub-case of @{text P}-operation when the requested @{text cs}
+  is available and @{text th} gets hold of it instantaneously with 
+  the @{text P}-operation.
+*}
 
 context valid_trace_p_h
 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.
+*}
+
 lemma subtree_kept:
   assumes "th' \<noteq> th"
   shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
@@ -373,6 +603,14 @@
   show "Th th \<notin> subtree (RAG s) (Th th')" .
 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.
+*}
 lemma cp_kept: 
   assumes "th' \<noteq> th"
   shows "cp (e#s) th' = cp s th'"
@@ -385,6 +623,12 @@
 
 end
 
+text {*
+  The following locale @{text valid_trace_p_w} corresponds to 
+  the case when the requested resource @{text cs} is not available and
+  thread @{text th} is blocked.
+*}
+
 context valid_trace_p_w
 begin
 
@@ -396,6 +640,12 @@
   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
   using RAG_tRAG_transfer[OF RAG_es cs_held] .
 
+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''"
@@ -431,6 +681,15 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
+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 
+  in ready queue) is reached. Actually, recalculation can terminate earlier, as 
+  confirmed by the following two lemmas. 
+
+  The first lemma @{text cp_gen_update_stop} is a technical lemma used to
+  prove the lemma that follows.
+*}
 lemma cp_gen_update_stop: (* ddd *)
   assumes "u \<in> ancestors (tRAG (e#s)) (Th th)"
   and "cp_gen (e#s) u = cp_gen s u"
@@ -558,6 +817,17 @@
   qed
 qed
 
+text {*
+  The following lemma is about the possible early termination of 
+  @{text cp}-recalculation. The lemma says that @{text cp}-recalculation 
+  can terminate as soon as the recalculation yields an unchanged @{text cp}-value. 
+
+  The @{text th'} in the lemma is assumed to be the first ancestor of @{text th}
+  encountered by the recalculation procedure which has an unchanged @{text cp}-value 
+  and the @{text th''} represents any thread upstream of @{text th'}. The lemma shows 
+  that the @{text "cp"}-value @{text "th''"} is not changed, therefore, needs no 
+  recalculation. It means the recalculation can be stop at @{text "th'"}.
+*}
 lemma cp_up:
   assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)"
   and "cp (e#s) th' = cp s th'"
@@ -575,59 +845,86 @@
 
 end
 
+text {* 
+  The following locale deals with the @{text Create}-operation.
+*}
+
 section {* The @{term Create} operation *}
 
 context valid_trace_create
 begin 
 
+text {*
+  Since @{text Create}-operation does not change @{text RAG} (according to 
+  @{thm RAG_es}) and @{text tRAG} is determined uniquely by @{text RAG}, 
+  therefore, @{text tRAG} is not not changed by @{text Create} neither.
+*}
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
   by (unfold tRAG_alt_def RAG_es, auto)
 
+lemma tG_kept: "tG (e#s) = tG s"
+  by (unfold tG_def tRAG_kept, simp)
+
+text {*
+  The following lemma shows that @{text th} is completely isolated 
+  from @{text RAG}.
+*}
+lemma th_not_in: "Th th \<notin> Field (tRAG s)"
+  by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
+
+text {*
+  Based on @{thm th_not_in}, it can be derived that @{text th} is also 
+  isolated from @{text RAG}.
+*}
+lemma th_not_in_tG: "th \<notin> Field (tG s)"
+  using tG_threads th_not_live_s by blast
+  
+
+text {*
+  The @{text Create}-operation does not change the precedences
+  of other threads excepting sets a the initial precedence for the 
+  thread being created (i.e. @{text th}).
+*}
 lemma preced_kept:
   assumes "th' \<noteq> th"
   shows "the_preced (e#s) th' = the_preced s th'"
   by (unfold the_preced_def preced_def is_create, insert assms, auto)
 
-lemma th_not_in: "Th th \<notin> Field (tRAG s)"
-  by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
-
+text {*
+  The following lemma shows that the @{text cp}-values of
+  all other threads need not be recalculated. The reason is twofold, first, 
+  since @{text tG} is not changed, sub-trees of these threads are not changed;
+  second, the precedences of the threads in these sub-trees are not changed (because 
+  the only thread with a changed precedence is @{text th} and @{text th} is isolated
+  from @{text tG}). 
+*}
 lemma eq_cp:
   assumes neq_th: "th' \<noteq> th"
   shows "cp (e#s) th' = cp s th'"
 proof -
-  have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
-        (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
-  proof(unfold tRAG_kept, rule f_image_eq)
-    fix a
-    assume a_in: "a \<in> subtree (tRAG s) (Th th')"
-    then obtain th_a where eq_a: "a = Th th_a" 
-    proof(cases rule:subtreeE)
-      case 2
-      from ancestors_Field[OF 2(2)]
-      and that show ?thesis by (unfold tRAG_alt_def, auto)
-    qed auto
-    have neq_th_a: "th_a \<noteq> th"
-    proof -
-      have "(Th th) \<notin> subtree (tRAG s) (Th th')"
-      proof
-        assume "Th th \<in> subtree (tRAG s) (Th th')"
-        thus False
-        proof(cases rule:subtreeE)
-          case 2
-          from ancestors_Field[OF this(2)]
-          and th_not_in[unfolded Field_def]
-          show ?thesis by auto
-        qed (insert assms, auto)
-      qed
-      with a_in[unfolded eq_a] show ?thesis by auto
-    qed
-    from preced_kept[OF this]
-    show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
-      by (unfold eq_a, simp)
-  qed
-  thus ?thesis by (unfold cp_alt_def1, simp)
+  have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
+        (the_preced s ` subtree (tG s) th')"
+  proof -
+    { fix a
+      assume "a \<in> subtree (tG s) th'"
+      with th_not_in_tG have "a \<noteq> th"
+        by (metis ancestors_Field dm_tG_threads neq_th subtree_ancestorsI th_not_live_s) 
+      from preced_kept[OF this]  
+      have "the_preced (e # s) a = the_preced s a" .
+    }
+    thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq)
+  qed   
+  thus ?thesis by (unfold cp_alt_def2, simp)
 qed
 
+text {*
+  The following two lemmas deal with the @{text cp}-calculation of @{text th}. 
+  The first lemma @{text children_of_th} says @{text th} has no children. 
+  The reason is simple, @{text th} is isolated from @{text "RAG"} before the
+  @{term Create}-operation and @{text Create} does not change @{text RAG}, so 
+  @{text th} keeps isolated after the operation.
+*}
+
 lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}"
 proof -
   { fix a
@@ -638,24 +935,44 @@
   } thus ?thesis by auto
 qed
 
+text {*
+  Now, since @{term th} has no children, by definition its @{text cp} value 
+  equals its precedence:
+*}
 lemma eq_cp_th: "cp (e#s) th = preced th (e#s)"
  by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
 
 end
 
-
+text {*
+  The following locale @{text valid_trace_exit} deals with the @{term Exit}-operation.
+*}
 context valid_trace_exit
 begin
 
+text {*
+  The treatment of @{text Exit} is very similar to @{text Create}.
+  First, the precedences of threads other than @{text th} are not changed.
+*}
+
 lemma preced_kept:
   assumes "th' \<noteq> th"
   shows "the_preced (e#s) th' = the_preced s th'"
   using assms
   by (unfold the_preced_def is_exit preced_def, simp)
 
+text {*
+  Second, @{term tRAG} is not changed by @{text Exit} either.
+*}
 lemma tRAG_kept: "tRAG (e#s) = tRAG s"
   by (unfold tRAG_alt_def RAG_es, auto)
 
+text {*
+  Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.
+*}
+lemma tG_kept: "tG (e#s) = tG s"
+  by (unfold tG_def tRAG_kept, simp)
+
 lemma th_RAG: "Th th \<notin> Field (RAG s)"
 proof -
   have "Th th \<notin> Range (RAG s)"
@@ -677,37 +994,40 @@
   ultimately show ?thesis by (auto simp:Field_def)
 qed
 
+
 lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)"
   using th_RAG tRAG_Field by auto
 
+
+text {*
+  Based on @{thm th_RAG}, it can be derived that @{text th} is also 
+  isolated from @{text tG}.
+*}
+lemma th_not_in_tG: "th \<notin> Field (tG s)"
+  using tG_kept vat_es.tG_threads by auto
+
+text {*
+  Because of @{thm preced_kept}, @{thm tG_kept} and @{thm th_tRAG},
+  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'"
 proof -
-  have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
-        (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
-  proof(unfold tRAG_kept, rule f_image_eq)
-    fix a
-    assume a_in: "a \<in> subtree (tRAG s) (Th th')"
-    then obtain th_a where eq_a: "a = Th th_a" 
-    proof(cases rule:subtreeE)
-      case 2
-      from ancestors_Field[OF 2(2)]
-      and that show ?thesis by (unfold tRAG_alt_def, auto)
-    qed auto
-    have neq_th_a: "th_a \<noteq> th"
-    proof -
-      from readys_in_no_subtree[OF th_ready_s assms]
-      have "(Th th) \<notin> subtree (RAG s) (Th th')" .
-      with tRAG_subtree_RAG[of s "Th th'"]
-      have "(Th th) \<notin> subtree (tRAG s) (Th th')" by auto
-      with a_in[unfolded eq_a] show ?thesis by auto
-    qed
-    from preced_kept[OF this]
-    show "(the_preced (e#s) \<circ> the_thread) a = (the_preced s \<circ> the_thread) a"
-      by (unfold eq_a, simp)
-  qed
-  thus ?thesis by (unfold cp_alt_def1, simp)
+  have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
+        (the_preced s ` subtree (tG s) th')"
+  proof -
+    { fix a
+      assume "a \<in> subtree (tG s) th'"
+      with th_not_in_tG have "a \<noteq> th"
+        by (metis ex_in_conv neq_th root_def root_readys_tG subtree_ancestorsI th_ready_s)
+      from preced_kept[OF this]  
+      have "the_preced (e # s) a = the_preced s a" .
+    }
+    thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq)
+  qed   
+  thus ?thesis by (unfold cp_alt_def2, simp)
 qed
 
 end




