--- 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,