PrioGDef.thy
changeset 64 b4bcd1edbb6d
parent 63 b620a2a0806a
child 65 633b1fc8631b
--- a/PrioGDef.thy	Wed Jan 06 20:46:14 2016 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,614 +0,0 @@
-chapter {* Definitions *}
-(*<*)
-theory PrioGDef
-imports Precedence_ord Moment
-begin
-(*>*)
-
-text {*
-  In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented. 
-  The model is based on Paulson's inductive protocol verification method, where 
-  the state of the system is modelled as a list of events happened so far with the latest 
-  event put at the head. 
-*}
-
-text {*
-  To define events, the identifiers of {\em threads},
-  {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 
-  need to be represented. All three are represetned using standard 
-  Isabelle/HOL type @{typ "nat"}:
-*}
-
-type_synonym thread = nat -- {* Type for thread identifiers. *}
-type_synonym priority = nat  -- {* Type for priorities. *}
-type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
-
-text {*
-  \noindent
-  The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level.
-  Every system call is represented as an event. The format of events is defined 
-  defined as follows:
-  *}
-
-datatype event = 
-  Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
-  Exit thread | -- {* Thread @{text "thread"} finishing its execution. *}
-  P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
-  V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}
-  Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
-
-
-text {* 
-  As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events,
-  which is defined by the following type @{text "state"}:
-  *}
-type_synonym state = "event list"
-
-
-text {* 
-\noindent
-  Resource Allocation Graph (RAG for short) is used extensively in our formal analysis. 
-  The following type @{text "node"} is used to represent nodes in RAG.
-  *}
-datatype node = 
-   Th "thread" | -- {* Node for thread. *}
-   Cs "cs" -- {* Node for critical resource. *}
-
-text {*
-  \noindent
-  The following function
-  @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
-  in state @{text "s"}.
-  *}
-fun threads :: "state \<Rightarrow> thread set"
-  where 
-  -- {* At the start of the system, the set of threads is empty: *}
-  "threads [] = {}" | 
-  -- {* New thread is added to the @{text "threads"}: *}
-  "threads (Create thread prio#s) = {thread} \<union> threads s" | 
-  -- {* Finished thread is removed: *}
-  "threads (Exit thread # s) = (threads s) - {thread}" | 
-  -- {* 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
-  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 
-  (represented by event @{text "Set thread priority"}).
-*}
-
-fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
-  where
-  -- {* @{text "0"} is assigned to threads which have never been created: *}
-  "priority thread [] = 0" |
-  "priority thread (Create thread' prio#s) = 
-     (if thread' = thread then prio else priority thread s)" |
-  "priority thread (Set thread' prio#s) = 
-     (if thread' = thread then prio else priority thread s)" |
-  "priority thread (e#s) = priority thread s"
-
-text {*
-  \noindent
-  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.
-*}
-fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
-  where
-  "last_set thread [] = 0" |
-  "last_set thread ((Create thread' prio)#s) = 
-       (if (thread = thread') then length s else last_set thread s)" |
-  "last_set thread ((Set thread' prio)#s) = 
-       (if (thread = thread') then length s else last_set thread s)" |
-  "last_set thread (_#s) = last_set thread s"
-
-text {*
-  \noindent 
-  The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of 
-  a thread is the combination of its {\em original priority} and {\em time} the priority is set. 
-  The intention is to discriminate threads with the same priority by giving threads whose priority
-  is assigned earlier higher precedences, becasue such threads are more urgent to finish. 
-  This explains the following definition:
-  *}
-definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
-  where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
-
-
-text {*
-  \noindent
-  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 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.
-  *}
-
-consts 
-  holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" 
-  waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
-  RAG :: "'b \<Rightarrow> (node \<times> node) set"
-  dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
-
-defs (overloaded) 
-  -- {* 
-  \begin{minipage}{0.9\textwidth}
-  This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"},
-  where @{text "holding wq th cs"} means thread @{text "th"} is holding the critical 
-  resource @{text "cs"}. This decision is based on @{text "wq"}.
-  \end{minipage}
-  *}
-
-  cs_holding_def: 
-  "holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
-  -- {* 
-  \begin{minipage}{0.9\textwidth}
-  In accordance with the definition of @{text "holding wq th cs"}, 
-  a thread @{text "th"} is considered waiting for @{text "cs"} if 
-  it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head.
-  This is reflected in the definition of @{text "waiting wq th cs"} as follows:
-  \end{minipage}
-  *}
-  cs_waiting_def: 
-  "waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
-  -- {* 
-  \begin{minipage}{0.9\textwidth}
-  @{text "RAG wq"} generates RAG (a binary relations on @{text "node"})
-  out of waiting queues of the system (represented by the @{text "wq"} argument):
-  \end{minipage}
-  *}
-  cs_RAG_def: 
-  "RAG (wq::cs \<Rightarrow> thread list) \<equiv>
-      {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
-  -- {* 
-  \begin{minipage}{0.9\textwidth}
-  The following @{text "dependants wq th"} represents the set of threads which are RAGing on
-  thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}. 
-  Here, "RAGing" means waiting directly or indirectly on the critical resource. 
-  \end{minipage}
-  *}
-  cs_dependants_def: 
-  "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
-
-
-text {* \noindent 
-  The following
-  @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under
-  state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of 
-  Priority Inheritance that the {\em current precedence} of a thread is the precedence 
-  inherited from the maximum of all its dependants, i.e. the threads which are waiting 
-  directly or indirectly waiting for some resources from it. If no such thread exits, 
-  @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
-  @{text "preced th s"}.
-  *}
-
-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:
-  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
-  unfolding cpreced_def image_def
-  apply(rule eq_reflection)
-  apply(rule_tac f="Max" in arg_cong)
-  by (auto)
-(*>*)
-
-
-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')"
-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. 
-*}
-
-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 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 
-  -- {*
-  \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}
-  \begin{enumerate}
-  \item @{text "ps"} is the schedule state of last moment.
-  \item @{text "pwq"} is the waiting queue function of last moment.
-  \item @{text "pcp"} is the precedence function of last moment (NOT USED). 
-  \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement:
-  \begin{enumerate}
-      \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to 
-            the end of @{text "cs"}'s waiting queue.
-      \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state,
-            @{text "th'"} must equal to @{text "thread"}, 
-            because @{text "thread"} is the one currently holding @{text "cs"}. 
-            The case @{text "[] \<Longrightarrow> []"} may never be executed in a legal state.
-            the @{text "(SOME q. distinct q \<and> set q = set qs)"} is used to choose arbitrarily one 
-            thread in waiting to take over the released resource @{text "cs"}. In our representation,
-            this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
-      \item For other happening event, the schedule state just does not change.
-  \end{enumerate}
-  \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue 
-        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) = 
-       (let wq = wq_fun (schs s) in
-          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
-|  "schs (Exit th # s) = 
-       (let wq = wq_fun (schs s) in
-          (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
-|  "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
-          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
-|  "schs (V th cs # s) = 
-       (let wq = wq_fun (schs s) in
-        let new_wq = wq(cs := release (wq cs)) in
-          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
-
-lemma cpreced_initial: 
-  "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
-apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)
-apply(simp add: preced_def)
-done
-
-lemma sch_old_def:
-  "schs (e#s) = (let ps = schs s in 
-                  let pwq = wq_fun ps in 
-                  let nwq = case e of
-                             P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
-                             V th cs \<Rightarrow> let nq = case (pwq cs) of
-                                                      [] \<Rightarrow> [] | 
-                                                      (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
-                                            in pwq(cs:=nq)                 |
-                              _ \<Rightarrow> pwq
-                  in let ncp = cpreced nwq (e#s) in 
-                     \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
-                 )"
-apply(cases e)
-apply(simp_all)
-done
-
-
-text {* 
-  \noindent
-  The following @{text "wq"} is a shorthand for @{text "wq_fun"}. 
-  *}
-definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
-  where "wq s = wq_fun (schs s)"
-
-text {* \noindent 
-  The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 
-  *}
-definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cp s \<equiv> cprec_fun (schs s)"
-
-text {* \noindent
-  Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 
-  @{text "dependants"} still have the 
-  same meaning, but redefined so that they no longer RAG on the 
-  fictitious {\em waiting queue function}
-  @{text "wq"}, but on system state @{text "s"}.
-  *}
-defs (overloaded) 
-  s_holding_abv: 
-  "holding (s::state) \<equiv> holding (wq_fun (schs s))"
-  s_waiting_abv: 
-  "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
-  s_RAG_abv: 
-  "RAG (s::state) \<equiv> RAG (wq_fun (schs s))"
-  s_dependants_abv: 
-  "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
-
-
-text {* 
-  The following lemma can be proved easily, and the meaning is obvious.
-  *}
-lemma
-  s_holding_def: 
-  "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
-  by (auto simp:s_holding_abv wq_def cs_holding_def)
-
-lemma s_waiting_def: 
-  "waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
-  by (auto simp:s_waiting_abv wq_def cs_waiting_def)
-
-lemma s_RAG_def: 
-  "RAG (s::state) =
-    {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
-  by (auto simp:s_RAG_abv wq_def cs_RAG_def)
-
-lemma
-  s_dependants_def: 
-  "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG (wq s))^+}"
-  by (auto simp:s_dependants_abv wq_def cs_dependants_def)
-
-text {*
-  The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} 
-  for running if it is a live thread and it is not waiting for any critical resource.
-  *}
-definition readys :: "state \<Rightarrow> thread set"
-  where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
-
-text {* \noindent
-  The following function @{text "runing"} calculates the set of running thread, which is the ready 
-  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"}.
-  *}
-definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
-  where "holdents s th \<equiv> {cs . holding s th cs}"
-
-lemma holdents_test: 
-  "holdents s th = {cs . (Cs cs, Th th) \<in> RAG s}"
-unfolding holdents_def
-unfolding s_RAG_def
-unfolding s_holding_abv
-unfolding wq_def
-by (simp)
-
-text {* \noindent
-  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
-  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 (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
-  -- {* 
-  A thread can be created if it is not a live thread:
-  *}
-  thread_create: "\<lbrakk>thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |
-  -- {*
-  A thread can exit if it no longer hold any resource:
-  *}
-  thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |
-  -- {*
-  \begin{minipage}{0.9\textwidth}
-  A thread can request for an critical resource @{text "cs"}, if it is running and 
-  the request does not form a loop in the current RAG. The latter condition 
-  is set up to avoid deadlock. The condition also reflects our assumption all threads are 
-  carefully programmed so that deadlock can not happen:
-  \end{minipage}
-  *}
-  thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow> 
-                                                                step s (P thread cs)" |
-  -- {*
-  \begin{minipage}{0.9\textwidth}
-  A thread can release a critical resource @{text "cs"} 
-  if it is running and holding that resource:
-  \end{minipage}
-  *}
-  thread_V: "\<lbrakk>thread \<in> runing s;  holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
-  -- {*
-  \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
-  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"
-  where
-  -- {* Empty list @{text "[]"} is a legal state in any protocol:*}
-  vt_nil[intro]: "vt []" |
-  -- {* 
-  \begin{minipage}{0.9\textwidth}
-  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 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 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"
-  where "the_cs (Cs cs) = cs"
-
-fun the_th :: "node \<Rightarrow> thread"
-  where "the_th (Th th) = th"
-
-text {* \noindent
-  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))"
-
-text {* \noindent
-  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 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 observation @{text "cntV s"} returns the number of operation @{text "V"} happened 
-  before reaching state @{text "s"}.
-  *}
-definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
-  where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
-(*<*)
-
-end
-(*>*)
-