--- a/PrioGDef.thy	Tue Oct 06 13:08:00 2015 +0800
+++ b/PrioGDef.thy	Tue Oct 06 18:52:04 2015 +0800
@@ -121,11 +121,11 @@
 
 text {*
   \noindent
-  A number of important notions in PIP are represented as functions defined 
-  in terms of the waiting queues of the system, where the waiting queues 
+  A number of important notions in PIP are represented as the following functions, 
+  defined in terms of the waiting queues of the system, where the waiting queues 
   , as a whole, is represented by the @{text "wq"} argument of every notion function.
-  The @{text "wq"} argument is itself a functions which 
-  maps every critical resource @{text "cs"} to the list of threads which are holding or waiting for it. 
+  The @{text "wq"} argument is itself a functions which maps every critical resource 
+  @{text "cs"} to the list of threads which are holding or waiting for it. 
   The thread at the head of this list is designated as the thread which is current 
   holding the resrouce, which is slightly different from tradition where
   all threads in the waiting queue are considered as waiting for the resource.
@@ -177,14 +177,14 @@
   cs_dependants_def: 
   "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
 
-(* I stop here for the moment 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 and a function assigning precedence to 
-  threads:
+  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. *}
@@ -213,20 +213,41 @@
   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, 
+  the following abbreviation "release qs" is the waiting queue after the thread 
+  holding the resource (which is thread at the head of @{text "qs"}) released
+  the resource:
+*}
 abbreviation
   "release qs \<equiv> case qs of
              [] => [] 
-          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
+          |  (_#qs') => (SOME q. distinct q \<and> set q = set qs')"
+text {* \noindent
+  It can be seen from the definition that the thread at the head of @{text "qs"} is removed
+  from the return value, and the value @{term "q"} is an reordering of @{text "qs'"}, the 
+  tail of @{text "qs"}. Through this reordering, one of the waiting threads (those in @{text "qs'"} }
+  is chosen nondeterministically to be the head of the new queue @{text "q"}. 
+  Therefore, this thread is the one who takes over the resource. This is a little better different 
+  from common sense that the thread who comes the earliest should take over.  
+  The intention of this definition is to show that the choice of which thread to take over the 
+  release resource does not affect the correctness of the PIP protocol. 
+*}
+
+(* ccc *)
 
 text {* \noindent
-  The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
-  It is the key function to model Priority Inheritance:
+  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:
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where