--- a/Implementation.thy	Sat Jan 09 22:19:27 2016 +0800
+++ b/Implementation.thy	Tue Jan 12 08:35:36 2016 +0800
@@ -22,16 +22,19 @@
   The complication of current precedence recalculation comes 
   because the changing of RAG needs to be taken into account, 
   in addition to the changing of precedence. 
+
   The reason RAG changing affects current precedence is that,
   according to the definition, current precedence 
-  of a thread is the maximum of the precedences of its dependants, 
-  where the dependants are defined in terms of RAG.
+  of a thread is the maximum of the precedences of every threads in its subtree, 
+  where the notion of sub-tree in RAG is defined in RTree.thy.
 
-  Therefore, each operation, lemmas concerning the change of the precedences 
-  and RAG are derived first, so that the lemmas about
-  current precedence recalculation can be based on.
+  Therefore, for each operation, lemmas about the change of precedences 
+  and RAG are derived first, on which lemmas about current precedence 
+  recalculation are based on.
 *}
 
+section {* The @{term Set} operation *}
+
 text {* (* ddd *)
   The following locale @{text "step_set_cps"} investigates the recalculation 
   after the @{text "Set"} operation.
@@ -59,8 +62,9 @@
 begin
 
 text {* (* ddd *)
-  The following two lemmas confirm that @{text "Set"}-operating only changes the precedence 
-  of the initiating thread.
+  The following two lemmas confirm that @{text "Set"}-operation
+  only changes the precedence of the initiating thread (or actor)
+  of the operation (or event).
 *}
 
 lemma eq_preced:
@@ -72,7 +76,6 @@
 qed
 
 lemma eq_the_preced: 
-  fixes th'
   assumes "th' \<noteq> th"
   shows "the_preced s th' = the_preced s' th'"
   using assms
@@ -86,14 +89,14 @@
   by (unfold s_def RAG_set_unchanged, auto)
 
 text {* (* ddd *)
-  Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"}
+  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"}. 
+  The proof of this lemma is simplified by using the alternative definition 
+  of @{text "cp"}. 
 *}
 
 lemma eq_cp_pre:
-  fixes th' 
   assumes nd: "Th th \<notin> subtree (RAG s') (Th th')"
   shows "cp s th' = cp s' th'"
 proof -
@@ -147,13 +150,14 @@
   of the initiating thread @{text "th"}.
 *}
 lemma eq_cp:
-  fixes th' 
   assumes "th' \<noteq> th"
   shows "cp s th' = cp s' th'"
   by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
 
 end
 
+section {* The @{term V} operation *}
+
 text {*
   The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
 *}
@@ -301,7 +305,7 @@
     and nt show ?thesis  by (auto intro:next_th_unique)
 qed
 
-lemma subtree_kept:
+lemma subtree_kept: (* ddd *)
   assumes "th1 \<notin> {th, th'}"
   shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R")
 proof -
@@ -429,7 +433,6 @@
  by (unfold cp_alt_def subtree_th preced_kept, auto)
 
 lemma eq_cp:
-  fixes th' 
   shows "cp s th' = cp s' th'"
   using cp_kept_1 cp_kept_2
   by (cases "th' = th", auto)
@@ -446,6 +449,8 @@
   from vt_s show "vt s" .
 qed
 
+section {* The @{term P} operation *}
+
 sublocale step_P_cps < vat_s' : valid_trace "s'"
 proof
   from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
@@ -727,6 +732,8 @@
 
 end
 
+section {* The @{term Create} operation *}
+
 locale step_create_cps =
   fixes s' th prio s 
   defines s_def : "s \<equiv> (Create th prio#s')"