--- a/PIPBasics.thy~	Sat Jan 09 22:19:27 2016 +0800
+++ b/PIPBasics.thy~	Tue Jan 12 08:35:36 2016 +0800
@@ -33,6 +33,13 @@
 context valid_trace
 begin
 
+lemma actor_inv: 
+  assumes "PIP s e"
+  and "\<not> isCreate e"
+  shows "actor e \<in> runing s"
+  using assms
+  by (induct, auto)
+
 lemma ind [consumes 0, case_names Nil Cons, induct type]:
   assumes "PP []"
      and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
@@ -1620,6 +1627,52 @@
   ultimately show ?thesis by (simp add:cntCS_def)
 qed 
 
+lemma count_rec1 [simp]: 
+  assumes "Q e"
+  shows "count Q (e#es) = Suc (count Q es)"
+  using assms
+  by (unfold count_def, auto)
+
+lemma count_rec2 [simp]: 
+  assumes "\<not>Q e"
+  shows "count Q (e#es) = (count Q es)"
+  using assms
+  by (unfold count_def, auto)
+
+lemma count_rec3 [simp]: 
+  shows "count Q [] =  0"
+  by (unfold count_def, auto)
+  
+lemma cntP_diff_inv:
+  assumes "cntP (e#s) th \<noteq> cntP s th"
+  shows "isP e \<and> actor e = th"
+proof(cases e)
+  case (P th' pty)
+  show ?thesis
+  by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 
+        insert assms P, auto simp:cntP_def)
+qed (insert assms, auto simp:cntP_def)
+
+lemma isP_E:
+  assumes "isP e"
+  obtains cs where "e = P (actor e) cs"
+  using assms by (cases e, auto)
+
+lemma isV_E:
+  assumes "isV e"
+  obtains cs where "e = V (actor e) cs"
+  using assms by (cases e, auto) (* ccc *)
+
+lemma cntV_diff_inv:
+  assumes "cntV (e#s) th \<noteq> cntV s th"
+  shows "isV e \<and> actor e = th"
+proof(cases e)
+  case (V th' pty)
+  show ?thesis
+  by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 
+        insert assms V, auto simp:cntV_def)
+qed (insert assms, auto simp:cntV_def)
+
 context valid_trace
 begin