--- a/Correctness.thy	Wed Jan 27 13:50:02 2016 +0000
+++ b/Correctness.thy	Thu Jan 28 13:46:45 2016 +0000
@@ -730,9 +730,9 @@
 *}
 
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  assumes "th \<notin> runing (t@s)"
+  assumes "th \<notin> runing (t @ s)"
   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-                    "th' \<in> runing (t@s)"
+                    "th' \<in> runing (t @ s)"
 proof -
   -- {* According to @{thm vat_t.th_chain_to_ready}, either 
         @{term "th"} is in @{term "readys"} or there is path leading from it to 

--- a/PIPDefs.thy	Wed Jan 27 13:50:02 2016 +0000
+++ b/PIPDefs.thy	Thu Jan 28 13:46:45 2016 +0000
@@ -1,10 +1,11 @@
-chapter {* Definitions *}
 (*<*)
 theory PIPDefs
 imports Precedence_ord Moment RTree Max
 begin
 (*>*)
 
+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 

--- a/PIPDefs.thy~	Wed Jan 27 13:50:02 2016 +0000
+++ b/PIPDefs.thy~	Thu Jan 28 13:46:45 2016 +0000
@@ -37,6 +37,24 @@
   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,

Binary file journal.pdf has changed