
diff -r e3cf792db636 -r 0f124691c191 PIPDefs.thy
--- a/PIPDefs.thy	Tue Jun 14 15:06:16 2016 +0100
+++ b/PIPDefs.thy	Fri Jun 17 09:46:25 2016 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory PIPDefs
-imports Precedence_ord RTree Max
+imports Precedence_ord Max
 begin
 (*>*)
 
@@ -8,8 +8,8 @@
 
 text {*
 
-  In this section, the formal model of Priority Inheritance Protocol (PIP)
-  is presented. The model is based on Paulson's inductive protocol
+  In this chapter, the formal model of the 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.
   *}
@@ -18,12 +18,12 @@
 
   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
+  represented. All three are represented using standard Isabelle/HOL type
   @{typ "nat"}: *}
 
-type_synonym thread = nat -- {* Type for thread identifiers. *}
+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). *}
+type_synonym cs = nat        -- {* Type for critical sections (or critical resources). *}
 
 text {*
 
@@ -38,33 +38,13 @@
 | 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  where
-  "actor (Exit th) = th" |
-  "actor (P th cs) = th" |
-  "actor (V th cs) = th" |
-  "actor (Set th pty) = th" |
-  "actor (Create th prio) = th"
 
--- {* The actions of a set of threads *}
-definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
-
-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"}: *}
+  As mentioned earlier, in Paulson's inductive method, the states of the
+  system are represented as lists of events, which is defined by the
+  following type @{text "state"}: *}
 
 type_synonym state = "event list"
 
@@ -91,7 +71,7 @@
   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
+  observed by @{text "threads s"} is the set of threads being live 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
@@ -102,11 +82,10 @@
 
 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"}). *}
+  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
@@ -209,10 +188,10 @@
 
 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} *}
+  \noindent The following @{text "dependants wq th"} represents the set of
+  threads which are waiting on thread @{text "th"} in Resource Allocation
+  Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or
+  indirectly on the critical resource. *}
 
 definition
   dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
@@ -233,7 +212,9 @@
 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))"
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
+
+
 
 text {*
 
@@ -245,12 +226,18 @@
   from. *}
 
 lemma cpreced_def2:
-  "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
+  "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
   unfolding cpreced_def image_def preceds_def
   apply(rule eq_reflection)
   apply(rule_tac f="Max" in arg_cong)
   by (auto)
 
+definition 
+  cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set"
+  where 
+  "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}"
+
+
 text {* 
 
   \noindent Assuming @{text "qs"} be the waiting queue of a critical
@@ -392,7 +379,7 @@
 apply(rule ext)
 apply(simp add: cpreced_def)
 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)
-apply(simp add: preced_def)
+apply(simp add: preced_def preceds_def)
 done
 
 text {* 
@@ -420,37 +407,19 @@
 
 definition 
   s_holding_abv: 
-  "holding (s::state) \<equiv> holding_raw (wq_fun (schs s))"
+  "holding (s::state) \<equiv> holding_raw (wq s)"
 
 definition
   s_waiting_abv: 
-  "waiting (s::state) \<equiv> waiting_raw (wq_fun (schs s))"
+  "waiting (s::state) \<equiv> waiting_raw (wq s)"
 
 definition
   s_RAG_abv: 
-  "RAG (s::state) \<equiv> RAG_raw (wq_fun (schs s))"
+  "RAG (s::state) \<equiv> RAG_raw (wq s)"
   
 definition
   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)
+  "dependants (s::state) \<equiv> dependants_raw (wq s)"
 
 lemma cp_eq: 
   shows "cp s th = cpreced (wq s) s th"
@@ -472,8 +441,8 @@
 
 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 holding_raw_def)
+  "holding (s::state) th cs \<equiv> (th \<in> set (wq s cs) \<and> th = hd (wq s cs))"
+  by(simp add: s_holding_abv 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))"
@@ -721,14 +690,37 @@
 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 RAG_raw_def, auto)
+using hRAG_def s_RAG_def s_holding_abv s_waiting_abv wRAG_def wq_def by auto
 
 lemma tRAG_alt_def: 
   "tRAG s = {(Th th1, Th th2) | th1 th2. 
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
 
+
+fun actor  where
+  "actor (Exit th) = th" |
+  "actor (P th cs) = th" |
+  "actor (V th cs) = th" |
+  "actor (Set th pty) = th" |
+  "actor (Create th prio) = th"
+
+-- {* The actions of a set of threads *}
+definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
+
+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"
+
+
 (*<*)
 
 end




