--- a/PIPDefs.thy~	Thu Jan 14 00:55:54 2016 +0800
+++ b/PIPDefs.thy~	Sat Jan 16 10:59:03 2016 +0800
@@ -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,