# HG changeset patch
# User xingyuan zhang <xingyuanzhang@126.com>
# Date 1445069433 -28800
# Node ID 8142e80f5d589c9b22b8f2844c57752a55d415eb
# Parent  8679d75b1d76962b6ca13229e188c3a4bfc86983
Finished comments on PrioGDef.thy

diff -r 8679d75b1d76 -r 8142e80f5d58 CpsG.thy
--- a/CpsG.thy	Tue Oct 06 18:52:04 2015 +0800
+++ b/CpsG.thy	Sat Oct 17 16:10:33 2015 +0800
@@ -1,8 +1,12 @@
-
+section {*
+  This file contains lemmas used to guide the recalculation of current precedence 
+  after every system call (or system operation)
+*}
 theory CpsG
 imports PrioG Max
 begin
 
+(* obvious lemma *)
 lemma not_thread_holdents:
   fixes th s
   assumes vt: "vt s"
@@ -126,8 +130,7 @@
   qed
 qed
 
-
-
+(* obvious lemma *)
 lemma next_th_neq: 
   assumes vt: "vt s"
   and nt: "next_th s th cs th'"
@@ -155,6 +158,7 @@
   qed
 qed
 
+(* obvious lemma *)
 lemma next_th_unique: 
   assumes nt1: "next_th s th cs th1"
   and nt2: "next_th s th cs th2"
@@ -170,8 +174,6 @@
   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
 qed
 
-
-
 definition child :: "state \<Rightarrow> (node \<times> node) set"
   where "child s \<equiv>
             {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
@@ -310,11 +312,15 @@
   qed
 qed
 
+text {* (* ??? *)
+*}
 lemma child_RAG_eq: 
   assumes vt: "vt s"
   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
   by (auto intro: RAG_child[OF vt] child_RAG_p)
 
+text {* (* ??? *)
+*}
 lemma children_no_dep:
   fixes s th th1 th2 th3
   assumes vt: "vt s"
@@ -348,6 +354,8 @@
   qed
 qed
 
+text {* (* ??? *)
+*}
 lemma unique_RAG_p:
   assumes vt: "vt s"
   and dp1: "(n, n1) \<in> (RAG s)^+"
@@ -359,6 +367,8 @@
   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 
+text {* (* ??? *)
+*}
 lemma dependants_child_unique:
   fixes s th th1 th2 th3
   assumes vt: "vt s"
@@ -395,6 +405,8 @@
   apply (unfold children_def)
   by (metis assms(2) children_def RAG_children eq_RAG)
 
+text {* (* ??? *)
+*}
 lemma dependants_expand:
   assumes "vt s"
   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
@@ -435,6 +447,8 @@
   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
 by auto
 
+text {* (* ??? *)
+*}
 lemma cp_rec:
   fixes s th
   assumes vt: "vt s"
@@ -902,8 +916,6 @@
 qed
 
 
-
-
 locale step_v_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (V th cs#s')"
diff -r 8679d75b1d76 -r 8142e80f5d58 PrioG.thy
--- a/PrioG.thy	Tue Oct 06 18:52:04 2015 +0800
+++ b/PrioG.thy	Sat Oct 17 16:10:33 2015 +0800
@@ -51,11 +51,12 @@
   qed
 qed
 
-lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
-  by(ind_cases "vt (e#s)", simp)
-
-lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
-  by(ind_cases "vt (e#s)", simp)
+text {*
+  The following lemma shows that only the @{text "P"}
+  operation can add new thread into waiting queues. 
+  Such kind of lemmas are very obvious, but need to be checked formally.
+  This is a kind of confirmation that our modelling is correct.
+*}
 
 lemma block_pre: 
   fixes thread cs s
@@ -111,6 +112,13 @@
   qed
 qed
 
+text {*
+  The following lemmas is also obvious and shallow. It says
+  that only running thread can request for a critical resource 
+  and that the requested resource must be one which is
+  not current held by the thread.
+*}
+
 lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 
   thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (RAG s)^+"
 apply (ind_cases "vt ((P thread cs)#s)")
@@ -202,6 +210,39 @@
     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 *)
 
+text {* (* ??? *)
+  The nature of the work is like this: since it starts from a very simple and basic 
+  model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
+  For instance, the fact 
+  that one thread can not be blocked by two critical resources at the same time
+  is obvious, because only running threads can make new requests, if one is waiting for 
+  a critical resource and get blocked, it can not make another resource request and get 
+  blocked the second time (because it is not running). 
+
+  To derive this fact, one needs to prove by contraction and 
+  reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
+  named @{text "p_split"}, which is about status changing along the time axis. It says if 
+  a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
+  but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} 
+  in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history 
+  of events leading to it), such that @{text "Q"} switched 
+  from being @{text "False"} to @{text "True"} and kept being @{text "True"}
+  till the last moment of @{text "s"}.
+
+  Suppose a thread @{text "th"} is blocked
+  on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, 
+  since no thread is blocked at the very beginning, by applying 
+  @{text "p_split"} to these two blocking facts, there exist 
+  two moments @{text "t1"} and @{text "t2"}  in @{text "s"}, such that 
+  @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} 
+  and kept on blocked on them respectively ever since.
+ 
+  Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
+  However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
+  in blocked state at moment @{text "t2"} and could not
+  make any request and get blocked the second time: Contradiction.
+*}
+
 lemma waiting_unique_pre:
   fixes cs1 cs2 s thread
   assumes vt: "vt s"
@@ -252,6 +293,7 @@
         case True
         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
           by auto
+          thm abs2
         from abs2 [OF vt_e True eq_th h2 h1]
         show ?thesis by auto
       next
@@ -354,6 +396,10 @@
   qed
 qed
 
+text {*
+  This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
+*}
+
 lemma waiting_unique:
   fixes s cs1 cs2
   assumes "vt s"
@@ -365,6 +411,11 @@
 by auto
 
 (* not used *)
+text {*
+  Every thread can only be blocked on one critical resource, 
+  symmetrically, every critical resource can only be held by one thread. 
+  This fact is much more easier according to our definition. 
+*}
 lemma held_unique:
   fixes s::"state"
   assumes "holding s th1 cs"
@@ -407,6 +458,7 @@
   thus ?thesis by auto
 qed
 
+(* An aux lemma used later *)
 lemma unique_minus:
   fixes x y z r
   assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
@@ -501,6 +553,12 @@
   qed
 qed
 
+text {*
+  The following three lemmas show that @{text "RAG"} does not change
+  by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
+  events, respectively.
+*}
+
 lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
 apply (unfold s_RAG_def s_waiting_def wq_def)
 by (simp add:Let_def)
@@ -514,10 +572,17 @@
 by (simp add:Let_def)
 
 
-
+text {* 
+  The following lemmas are used in the proof of 
+  lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed
+  by @{text "V"}-events. 
+  However, since our model is very concise, such  seemingly obvious lemmas need to be derived from scratch,
+  starting from the model definitions.
+*}
 lemma step_v_hold_inv[elim_format]:
   "\<And>c t. \<lbrakk>vt (V th cs # s); 
-  \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
+          \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> 
+            next_th s th cs t \<and> c = cs"
 proof -
   fix c t
   assume vt: "vt (V th cs # s)"
@@ -564,6 +629,10 @@
   qed
 qed
 
+text {* 
+  The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be
+  derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.
+*}
 lemma step_v_wait_inv[elim_format]:
     "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
            \<rbrakk>
@@ -773,6 +842,10 @@
   qed
 qed
 
+text {* (* ??? *) 
+  The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
+  with the happening of @{text "V"}-events:
+*}
 lemma step_RAG_v:
 fixes th::thread
 assumes vt:
@@ -790,6 +863,10 @@
   apply (erule_tac step_v_not_wait, auto)
   done
 
+text {* 
+  The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed
+  with the happening of @{text "P"}-events:
+*}
 lemma step_RAG_p:
   "vt (P th cs#s) \<Longrightarrow>
   RAG (P th cs # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
@@ -808,6 +885,12 @@
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_RAG_def, auto)
 
+text {*
+  The following lemma shows that @{text "RAG"} is acyclic.
+  The overall structure is by induction on the formation of @{text "vt s"}
+  and then case analysis on event @{text "e"}, where the non-trivial cases 
+  for those for @{text "V"} and @{text "P"} events.
+*}
 lemma acyclic_RAG: 
   fixes s
   assumes vt: "vt s"
@@ -1218,6 +1301,12 @@
     qed
 qed
 
+text {* \noindent
+  The following lemmas shows that: starting from any node in @{text "RAG"}, 
+  by chasing out-going edges, it is always possible to reach a node representing a ready
+  thread. In this lemma, it is the @{text "th'"}.
+*}
+
 lemma chain_building:
   assumes vt: "vt s"
   shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
@@ -1269,6 +1358,9 @@
   qed
 qed
 
+text {* \noindent
+  The following is just an instance of @{text "chain_building"}.
+*}
 lemma th_chain_to_ready:
   fixes s th
   assumes vt: "vt s"
@@ -1452,6 +1544,11 @@
   ultimately show ?thesis by (simp add:cntCS_def)
 qed 
 
+text {* (* ??? *) \noindent
+  The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 
+  of one particular thread. 
+*} 
+
 lemma cnp_cnv_cncs:
   fixes s th
   assumes vt: "vt s"
@@ -2294,8 +2391,6 @@
 apply (metis insertCI runing_unique)
 apply(auto) 
 done
-  
-
 
 lemma create_pre:
   assumes stp: "step s e"
@@ -2360,74 +2455,7 @@
   assumes "vt s"
   and "th \<notin> threads s"
   shows "cntP s th = cntV s th"
-proof -
-  from assms show ?thesis
-  proof(induct)
-    case (vt_cons s e)
-    have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
-    have not_in: "th \<notin> threads (e # s)" by fact
-    have "step s e" by fact
-    thus ?case proof(cases)
-      case (thread_create thread prio)
-      assume eq_e: "e = Create thread prio"
-      hence "thread \<in> threads (e#s)" by simp
-      with not_in and eq_e have "th \<notin> threads s" by auto
-      from ih [OF this] show ?thesis using eq_e
-        by (auto simp:cntP_def cntV_def count_def)
-    next
-      case (thread_exit thread)
-      assume eq_e: "e = Exit thread"
-        and not_holding: "holdents s thread = {}"
-      have vt_s: "vt s" by fact
-      from finite_holding[OF vt_s] have "finite (holdents s thread)" .
-      with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
-      moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
-      moreover note cnp_cnv_cncs[OF vt_s, of thread]
-      ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
-      show ?thesis
-      proof(cases "th = thread")
-        case True
-        with eq_thread eq_e show ?thesis 
-          by (auto simp:cntP_def cntV_def count_def)
-      next
-        case False
-        with not_in and eq_e have "th \<notin> threads s" by simp
-        from ih[OF this] and eq_e show ?thesis 
-           by (auto simp:cntP_def cntV_def count_def)
-      qed
-    next
-      case (thread_P thread cs)
-      assume eq_e: "e = P thread cs"
-      have "thread \<in> runing s" by fact
-      with not_in eq_e have neq_th: "thread \<noteq> th" 
-        by (auto simp:runing_def readys_def)
-      from not_in eq_e have "th \<notin> threads s" by simp
-      from ih[OF this] and neq_th and eq_e show ?thesis
-        by (auto simp:cntP_def cntV_def count_def)
-    next
-      case (thread_V thread cs)
-      assume eq_e: "e = V thread cs"
-      have "thread \<in> runing s" by fact
-      with not_in eq_e have neq_th: "thread \<noteq> th" 
-        by (auto simp:runing_def readys_def)
-      from not_in eq_e have "th \<notin> threads s" by simp
-      from ih[OF this] and neq_th and eq_e show ?thesis
-        by (auto simp:cntP_def cntV_def count_def)
-    next
-      case (thread_set thread prio)
-      assume eq_e: "e = Set thread prio"
-        and "thread \<in> runing s"
-      hence "thread \<in> threads (e#s)" 
-        by (simp add:runing_def readys_def)
-      with not_in and eq_e have "th \<notin> threads s" by auto
-      from ih [OF this] show ?thesis using eq_e
-        by (auto simp:cntP_def cntV_def count_def)  
-    qed
-  next
-    case vt_nil
-    show ?case by (auto simp:cntP_def cntV_def count_def)
-  qed
-qed
+ by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
 
 lemma eq_RAG: 
   "RAG (wq s) = RAG s"
@@ -2764,6 +2792,10 @@
   qed
 qed
 
+text {* (* ccc *) \noindent
+  Since the current precedence of the threads in ready queue will always be boosted,
+  there must be one inside it has the maximum precedence of the whole system. 
+*}
 lemma max_cp_readys_threads:
   assumes vt: "vt s"
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
@@ -2880,4 +2912,9 @@
   shows "(detached s th) = (cntP s th = cntV s th)"
   by (insert vt, auto intro:detached_intro detached_elim)
 
+text {* 
+  The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
+  from the concise and miniature model of PIP given in PrioGDef.thy.
+*}
+
 end
diff -r 8679d75b1d76 -r 8142e80f5d58 PrioGDef.thy
--- a/PrioGDef.thy	Tue Oct 06 18:52:04 2015 +0800
+++ b/PrioGDef.thy	Sat Oct 17 16:10:33 2015 +0800
@@ -1,3 +1,4 @@
+chapter {* Definitions *}
 (*<*)
 theory PrioGDef
 imports Precedence_ord Moment
@@ -70,15 +71,28 @@
   -- {* Other kind of events does not affect the value of @{text "threads"}: *}
   "threads (e#s) = threads s" 
 
+text {* 
+  \noindent
+  The function @{text "threads"} defined above is one of 
+  the so called {\em observation function}s which forms 
+  the very basis of Paulson's inductive protocol verification method.
+  Each observation function {\em observes} one particular aspect (or attribute)
+  of the system. For example, the attribute observed by  @{text "threads s"}
+  is the set of threads living in state @{text "s"}. 
+  The protocol being modelled 
+  The decision made the protocol being modelled is based on the {\em observation}s
+  returned by {\em observation function}s. Since {\observation function}s forms 
+  the very basis on which Paulson's inductive method is based, there will be 
+  a lot of such observation functions introduced in the following. In fact, any function 
+  which takes event list as argument is a {\em observation function}.
+  *}
+
 text {* \noindent
-  Functions such as @{text "threads"}, which extract information out of system states, are called
-  {\em observing functions}. A series of observing functions will be defined in the sequel in order to 
-  model the protocol. 
-  Observing function @{text "priority"} calculates 
-  the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
-  : @{text "priority th s" }. The {\em original priority} is the priority 
+  Observation @{text "priority th s"} is
+  the {\em original priority} of thread @{text "th"} in state @{text "s"}. 
+  The {\em original priority} is the priority 
   assigned to a thread when it is created or when it is reset by system call 
-  @{text "Set thread priority"}.
+  (represented by event @{text "Set thread priority"}).
 *}
 
 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
@@ -93,8 +107,7 @@
 
 text {*
   \noindent
-  In the following,
-  @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set, 
+  Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set, 
   observed from state @{text "s"}.
   The time in the system is measured by the number of events happened so far since the very beginning.
 *}
@@ -177,17 +190,6 @@
   cs_dependants_def: 
   "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
 
-text {*
-  The data structure used by the operating system for scheduling is referred to as 
-  {\em schedule state}. It is represented as a record consisting of 
-  a function assigning waiting queue to resources 
-  (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"} 
-  and  @{text "RAG"}, etc) and a function assigning precedence to threads:
-  *}
-
-record schedule_state = 
-    wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
-    cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
 
 text {* \noindent 
   The following
@@ -203,6 +205,15 @@
 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
   where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants wq th)))"
 
+text {*
+  Notice that the current precedence (@{text "cpreced"}) of one thread @{text "th"} can be boosted 
+  (becoming larger than its own precedence) by those threads in 
+  the @{text "dependants wq th"}-set. If one thread get boosted, we say 
+  it inherits the priority (or, more precisely, the precedence) of 
+  its dependants. This is how the word "Inheritance" in 
+  Priority Inheritance Protocol comes.
+*}
+
 (*<*)
 lemma 
   cpreced_def2:
@@ -213,13 +224,6 @@
   by (auto)
 (*>*)
 
-(*
-abbreviation
-  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
-
-abbreviation 
-  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
-*)
 
 text {* \noindent
   Assuming @{text "qs"} be the waiting queue of a critical resource, 
@@ -242,16 +246,53 @@
   release resource does not affect the correctness of the PIP protocol. 
 *}
 
-(* ccc *)
+text {*
+  The data structure used by the operating system for scheduling is referred to as 
+  {\em schedule state}. It is represented as a record consisting of 
+  a function assigning waiting queue to resources 
+  (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"} 
+  and  @{text "RAG"}, etc) and a function assigning precedence to threads:
+  *}
+
+record schedule_state = 
+    wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+    cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
 
 text {* \noindent
-  The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}
-  out of the current system state @{text "s"}.
-  It is the central function to model Priority Inheritance:
+  The following two abbreviations (@{text "all_unlocked"} and @{text "initial_cprec"}) 
+  are used to set the initial values of the @{text "wq_fun"} @{text "cprec_fun"} fields 
+  respectively of the @{text "schedule_state"} record by the following function @{text "sch"},
+  which is used to calculate the system's {\em schedule state}.
+
+  Since there is no thread at the very beginning to make request, all critical resources 
+  are free (or unlocked). This status is represented by the abbreviation
+  @{text "all_unlocked"}. 
+  *}
+abbreviation
+  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+
+text {* \noindent
+  The initial current precedence for a thread can be anything, because there is no thread then. 
+  We simply assume every thread has precedence @{text "Prc 0 0"}.
+  *}
+
+abbreviation 
+  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+
+
+text {* \noindent
+  The following function @{text "schs"} is used to calculate the system's schedule state @{text "schs s"}
+  out of the current system state @{text "s"}. It is the central function to model Priority Inheritance:
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
-  "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |
+  -- {*
+  \begin{minipage}{0.9\textwidth}
+    Setting the initial value of the @{text "schedule_state"} record (see the explanations above).
+  \end{minipage}
+  *}
+  "schs [] = (| wq_fun = all_unlocked,  cprec_fun = initial_cprec |)" |
 
   -- {*
   \begin{minipage}{0.9\textwidth}
@@ -276,6 +317,12 @@
         function. The RAGency of precedence function on waiting queue function is the reason to 
         put them in the same record so that they can evolve together.
   \end{enumerate}
+  
+
+  The calculation of @{text "cprec_fun"} depends on the value of @{text "wq_fun"}. 
+  Therefore, in the following cases, @{text "wq_fun"} is always calculated first, in 
+  the name of @{text "wq"} (if  @{text "wq_fun"} is not changed
+  by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed).
   \end{minipage}
      *}
    "schs (Create th prio # s) = 
@@ -287,6 +334,12 @@
 |  "schs (Set th prio # s) = 
        (let wq = wq_fun (schs s) in
           (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
+   -- {*
+   \begin{minipage}{0.9\textwidth}
+      Different from the forth coming cases, the @{text "wq_fun"} field of the schedule state 
+      is changed. So, the new value is calculated first, in the name of @{text "new_wq"}.
+   \end{minipage}   
+   *}
 |  "schs (P th cs # s) = 
        (let wq = wq_fun (schs s) in
         let new_wq = wq(cs := (wq cs @ [th])) in
@@ -353,7 +406,7 @@
 
 
 text {* 
-  The following lemma can be proved easily:
+  The following lemma can be proved easily, and the meaning is obvious.
   *}
 lemma
   s_holding_def: 
@@ -383,12 +436,19 @@
 
 text {* \noindent
   The following function @{text "runing"} calculates the set of running thread, which is the ready 
-  thread with the highest precedence. 
+  thread with the highest precedence.  
   *}
 definition runing :: "state \<Rightarrow> thread set"
   where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
 
 text {* \noindent
+  Notice that the definition of @{text "running"} reflects the preemptive scheduling strategy,  
+  because, if the @{text "running"}-thread (the one in @{text "runing"} set) 
+  lowered its precedence by resetting its own priority to a lower
+  one, it will lose its status of being the max in @{text "ready"}-set and be superseded.
+*}
+
+text {* \noindent
   The following function @{text "holdents s th"} returns the set of resources held by thread 
   @{text "th"} in state @{text "s"}.
   *}
@@ -404,16 +464,20 @@
 by (simp)
 
 text {* \noindent
-  @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
+  Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
   state @{text "s"}:
   *}
 definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntCS s th = card (holdents s th)"
 
 text {* \noindent
-  The fact that event @{text "e"} is eligible to happen next in state @{text "s"} 
+  According to the convention of Paulson's inductive method,
+  the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} 
   is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as 
-  follows:
+  follows (notice how the decision is based on the {\em observation function}s 
+  defined above, and also notice how a complicated protocol is modeled by a few simple 
+  observations, and how such a kind of simplicity gives rise to improved trust on
+  faithfulness):
   *}
 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
   where
@@ -443,13 +507,29 @@
   *}
   thread_V: "\<lbrakk>thread \<in> runing s;  holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
   -- {*
-  A thread can adjust its own priority as long as it is current running:
+  \begin{minipage}{0.9\textwidth}
+  A thread can adjust its own priority as long as it is current running. 
+  With the resetting of one thread's priority, its precedence may change. 
+  If this change lowered the precedence, according to the definition of @{text "running"}
+  function, 
+  \end{minipage}
   *}  
   thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
 
+text {*
+  In Paulson's inductive method, every protocol is defined by such a @{text "step"}
+  predicate. For instance, the predicate @{text "step"} given above 
+  defines the PIP protocol. So, it can also be called "PIP".
+*}
+
+abbreviation
+  "PIP \<equiv> step"
+
+
 text {* \noindent
-  With predicate @{text "step"}, the fact that @{text "s"} is a legal state in 
-  Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
+  For any protocol defined by a @{text "step"} predicate, 
+  the fact that @{text "s"} is a legal state in 
+  the protocol is expressed as: @{text "vt step s"}, where
   the predicate @{text "vt"} can be defined as the following:
   *}
 inductive vt :: "state \<Rightarrow> bool"
@@ -458,19 +538,32 @@
   vt_nil[intro]: "vt []" |
   -- {* 
   \begin{minipage}{0.9\textwidth}
-  If @{text "s"} a legal state, and event @{text "e"} is eligible to happen
-  in state @{text "s"}, then @{text "e#s"} is a legal state as well:
+  If @{text "s"} a legal state of the protocol defined by predicate @{text "step"}, 
+  and event @{text "e"} is allowed to happen under state @{text "s"} by the protocol 
+  predicate @{text "step"}, then @{text "e#s"} is a new legal state rendered by the 
+  happening of @{text "e"}:
   \end{minipage}
   *}
   vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
 
 text {*  \noindent
   It is easy to see that the definition of @{text "vt"} is generic. It can be applied to 
-  any step predicate to get the set of legal states.
+  any specific protocol specified by a @{text "step"}-predicate to get the set of
+  legal states of that particular protocol.
   *}
 
+text {* 
+  The following are two very basic properties of @{text "vt"}.
+*}
+
+lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
+  by(ind_cases "vt (e#s)", simp)
+
+lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
+  by(ind_cases "vt (e#s)", simp)
+
 text {* \noindent
-  The following two functions @{text "the_cs"} and @{text "the_th"} are used to extract
+  The following two auxiliary functions @{text "the_cs"} and @{text "the_th"} are used to extract
   critical resource and thread respectively out of RAG nodes.
   *}
 fun the_cs :: "node \<Rightarrow> cs"
@@ -483,27 +576,33 @@
   The following predicate @{text "next_th"} describe the next thread to 
   take over when a critical resource is released. In @{text "next_th s th cs t"}, 
   @{text "th"} is the thread to release, @{text "t"} is the one to take over.
+  Notice how this definition is backed up by the @{text "release"} function and its use 
+  in the @{text "V"}-branch of @{text "schs"} function. This @{text "next_th"} function
+  is not needed for the execution of PIP. It is introduced as an auxiliary function 
+  to state lemmas. The correctness of this definition will be confirmed by 
+  lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"}, 
+  @{text "step_v_get_hold"} and @{text "step_v_not_wait"}.
   *}
 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
   where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> 
-                                                t = hd (SOME q. distinct q \<and> set q = set rest))"
+                                     t = hd (SOME q. distinct q \<and> set q = set rest))"
 
 text {* \noindent
-  The function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}
+  The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}
   in list @{text "l"}:
   *}
 definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
   where "count Q l = length (filter Q l)"
 
 text {* \noindent
-  The following @{text "cntP s"} returns the number of operation @{text "P"} happened 
+  The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened 
   before reaching state @{text "s"}.
   *}
 definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
   where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
 
 text {* \noindent
-  The following @{text "cntV s"} returns the number of operation @{text "V"} happened 
+  The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened 
   before reaching state @{text "s"}.
   *}
 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"