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"