chapter {* Definitions *}
(*<*)
theory PIPDefs
imports Precedence_ord Moment RTree Max
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"}. *}

fun actor :: "event \<Rightarrow> thread" where
  "actor (Create th pty) = th" |
  "actor (Exit th) = th" |
  "actor (P th cs) = th" |
  "actor (V th cs) = th" |
  "actor (Set th pty) = th"

fun isCreate :: "event \<Rightarrow> bool" where
  "isCreate (Create th pty) = True" |
  "isCreate _ = False"

fun isP :: "event \<Rightarrow> bool" where
  "isP (P th cs) = True" |
  "isP _ = False"

fun isV :: "event \<Rightarrow> bool" where
  "isV (V th cs) = True" |
  "isV _ = False"

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"

text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
       difference is the order of arguemts. *}
definition "the_preced s th = preced th s"

text {* @{term "the_thread"} extracts thread out of RAG node. *}
fun the_thread :: "node \<Rightarrow> thread" where
   "the_thread (Th th) = th"

text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

text {* 
  The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
  It characterizes the dependency between threads when calculating current
  precedences. It is defined as the composition of the above two sub-graphs, 
  names @{term "wRAG"} and @{term "hRAG"}.
 *}
definition "tRAG s = wRAG s O hRAG s"

text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
  by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 
             s_holding_abv cs_RAG_def, auto)

definition "cp_gen s x =
                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

(*<*)

end
(*>*)