
diff -r a88af0e4731f -r 38c6acf03f68 PIPDefs.thy
--- a/PIPDefs.thy	Tue Jun 07 13:51:39 2016 +0100
+++ b/PIPDefs.thy	Thu Jun 09 23:01:36 2016 +0100
@@ -7,29 +7,29 @@
 chapter {* Definitions *}
 
 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 (trace) happened so far with the 
-  latest event put at the head. 
-*}
+
+  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 (trace) 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"}:
-*}
+
+  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:
-  *}
+
+  \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"}. *}
@@ -61,173 +61,166 @@
   "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"}: *}
+  
+  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 {* 
-  Resource Allocation Graphs (RAG for short) are used extensively in our formal analysis. 
-  The following type @{text "node"} is used to represent the two types of nodes in RAGs. *}
-datatype node = 
-  Th "thread" -- {* Node for a thread. *}
-| Cs "cs"     -- {* Node for a critical resource. *}
+text {*
 
-text {*
-  The function @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
-  in state @{text "s"}. *}
+  The 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" | 
+  "threads (Create th prio#s) = {th} \<union> threads s" | 
   -- {* Finished thread is removed: *}
-  "threads (Exit thread # s) = (threads s) - {thread}" | 
+  "threads (Exit th # s) = (threads s) - {th}" | 
   -- {* Other kind of events does not affect the value of @{text "threads"}: *}
-  "threads (e#s) = threads s" 
+  "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
+  \noindent The function @{text "threads"} is one of the {\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}.  *}
+  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"}).  *}
+  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"
+  "priority th [] = 0" |
+  "priority th (Create th' prio # s) = 
+     (if th' = th then prio else priority th s)" |
+  "priority th (Set th' prio # s) = 
+     (if th' = th then prio else priority th s)" |
+  "priority th (e # s) = priority th 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.  *}
+  \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"
+  "last_set th [] = 0" |
+  "last_set th ((Create th' prio) # s) = 
+       (if (th = th') then length s else last_set th s)" |
+  "last_set th ((Set th' prio) # s) = 
+       (if (th = th') then length s else last_set th s)" |
+  "last_set th (_ # s) = last_set th 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: *}
+  \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 the {\em time} the priority was set. The intention
+  is to discriminate threads with the same priority by giving threads whose
+  priority is assigned earlier higher precedences, because such threads are
+  assumed more urgent to finish. *}
 
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
-  where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
+  where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
 
+definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"
+  where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"
 
 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.  *}
+  \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
+  resource, 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"
-*)
+text {* 
 
--- {* 
-  \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}
-  *}
+  \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} *}
 
 definition
-  cs_holding_raw:   
   "holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
 
+text {* 
+
+  \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} *}
 
 definition
-  -- {* 
-  \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}
-  *}
+  "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+
+text {* 
+
+  Resource Allocation Graphs (RAG for short) are used extensively in our
+  formal analysis. The following type @{text "node"} is used to represent
+  the two types of nodes in RAGs. *}
 
-  cs_waiting_raw: 
-  "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+datatype node = 
+  Th "thread" -- {* Node for a thread. *}
+| Cs "cs"     -- {* Node for a critical resource. *}
+
+
+text {*
+  
+  \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} *}
 
 definition
-  -- {* 
-  \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}
-  *}
+  RAG_raw :: "(cs \<Rightarrow> thread list) => (node * node) set"
+where
+  "RAG_raw wq \<equiv>
+      {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> 
+      {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
 
-  cs_RAG_raw: 
-  "RAG_raw (wq::cs \<Rightarrow> thread list) \<equiv>
-      {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
+text {*
+ 
+  \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} *}
 
 definition
-  -- {* 
-  \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_raw (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
+  dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
+where
+  "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw 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
@@ -235,39 +228,35 @@
   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"}. 
-*}
+  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_raw wq th)))"
+definition 
+  cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
+  where 
+  "cpreced wq s th = Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw 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.
-*}
+  @{text "th"} can be boosted (increased) by those threads in the @{text
+  "dependants wq th"}-set. If one thread gets boosted, we say it inherits
+  the priority (or, more precisely, the precedence) of its dependants. This
+  is whrere the word "Inheritance" in Priority Inheritance Protocol comes
+  from. *}
 
-(*<*)
-lemma 
-  cpreced_def2:
-  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants_raw wq th})"
-  unfolding cpreced_def image_def
+lemma cpreced_def2:
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
+  unfolding cpreced_def image_def preceds_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: 
-*}
+  @{text "qs"}) released the resource: *}
 
 abbreviation
   "release qs \<equiv> case qs of
@@ -275,6 +264,7 @@
           |  (_#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
@@ -284,22 +274,22 @@
   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. 
-*}
+  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:
-  *}
+  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
@@ -315,27 +305,28 @@
   "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"}.
-  *}
+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 
-  -- {*
+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.
+
   \begin{minipage}{0.9\textwidth}
-    Setting the initial value of the @{text "schedule_state"} record (see the explanations above).
+    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}
@@ -368,7 +359,11 @@
   by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed).
   \end{minipage}
      *}
-   "schs (Create th prio # s) = 
+
+fun schs :: "state \<Rightarrow> schedule_state"
+  where 
+  "schs [] = (| wq_fun = all_unlocked,  cprec_fun = initial_cprec |)" 
+| "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) = 
@@ -394,50 +389,34 @@
 
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
+apply(rule ext)
 apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw)
+apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_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"}.
+  *}
 
-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"}. 
-  *}
+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"}.
-  *}
+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"}. *}
 
 definition 
   s_holding_abv: 
@@ -455,56 +434,93 @@
   s_dependants_abv: 
   "dependants (s::state) \<equiv> dependants_raw (wq_fun (schs s))"
 
+text {* 
+
+  The following four lemmas relate the @{term wq} and non-@{term wq}
+  versions of @{term waiting}, @{term holding}, @{term dependants} and
+  @{term cp}. *}
+
+lemma waiting_eq: 
+  shows "waiting s th cs = waiting_raw (wq s) th cs"
+  by (simp add: s_waiting_abv wq_def)
+
+lemma holding_eq: 
+  shows "holding s th cs = holding_raw (wq s) th cs"
+  by (simp add: s_holding_abv wq_def)
+
+lemma eq_dependants: 
+  shows "dependants_raw (wq s) = dependants s"
+  by (simp add: s_dependants_abv wq_def)
+
+lemma cp_eq: 
+  shows "cp s th = cpreced (wq s) s th"
+unfolding cp_def wq_def
+apply(induct s rule: schs.induct)
+apply(simp add: Let_def cpreced_initial)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
 
 text {* 
-  The following lemma can be proved easily, and the meaning is obvious.
-  *}
+
+  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_raw)
+  by (auto simp:s_holding_abv wq_def holding_raw_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_raw)
+  by (auto simp:s_waiting_abv wq_def waiting_raw_def)
 
 lemma s_RAG_def: 
   "RAG (s::state) =
-    {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
-  by (auto simp:s_RAG_abv wq_def cs_RAG_raw)
+    {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union> 
+    {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
+  by (auto simp:s_RAG_abv wq_def RAG_raw_def)
 
-lemma
-  s_dependants_def: 
-  "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw (wq s))^+}"
-  by (auto simp:s_dependants_abv wq_def cs_dependants_def)
+lemma eq_RAG: 
+  "RAG_raw (wq s) = RAG s"
+  by (unfold RAG_raw_def s_RAG_def, auto)
+
+
+lemma s_dependants_def: 
+  shows "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG s)^+}"
+using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto
 
 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.
-  *}
+  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.
-  *}
+  
+  \noindent The following function @{text "running"} 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))}"
+definition running :: "state \<Rightarrow> thread set"
+  where "running 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
+  (the one in @{text "running"} 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 "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"}. *}
 
@@ -520,15 +536,18 @@
 unfolding wq_def
 by (simp)
 
-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):
-  *}
+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
   -- {* 
@@ -538,7 +557,7 @@
   -- {*
   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)" |
+  thread_exit: "\<lbrakk>thread \<in> running 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 
@@ -547,7 +566,7 @@
   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> 
+  thread_P: "\<lbrakk>thread \<in> running s;  (Cs cs, Th thread)  \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow> 
                                                                 step s (P thread cs)" |
   -- {*
   \begin{minipage}{0.9\textwidth}
@@ -555,7 +574,7 @@
   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)" |
+  thread_V: "\<lbrakk>thread \<in> running 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. 
@@ -564,24 +583,26 @@
   function, 
   \end{minipage}
   *}  
-  thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
+  thread_set: "\<lbrakk>thread \<in> running 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".
-*}
+
+  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:
-  *}
+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:*}
@@ -596,15 +617,16 @@
   *}
   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 {*  
+
+  \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"}.
-*}
+  
+  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)
@@ -700,7 +722,7 @@
 
 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_raw, auto)
+             s_holding_abv RAG_raw_def, auto)
 
 lemma tRAG_alt_def: 
   "tRAG s = {(Th th1, Th th2) | th1 th2. 




