--- a/PIPBasics.thy	Fri Apr 15 14:44:09 2016 +0100
+++ b/PIPBasics.thy	Thu Jun 02 13:15:03 2016 +0100
@@ -14,7 +14,7 @@
 *}
 
 
-section {* Generic aulxiliary lemmas *}
+section {* Generic auxiliary lemmas *}
 
 lemma rel_eqI:
   assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
@@ -540,6 +540,11 @@
   } ultimately show ?thesis by blast
 qed
 
+lemma image_eq:
+  assumes "A = B"
+  shows "f ` A = f ` B"
+  using assms by auto
+
 lemma tRAG_trancl_eq_Th:
    "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
     {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"
@@ -573,7 +578,8 @@
     proof
       assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
       with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto
-      thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
+      thus ?thesis using subtree_def tRAG_trancl_eq 
+        by fastforce (* ccc *)
     qed (insert h, auto simp:subtree_def)
   } ultimately show ?thesis by auto
 qed
@@ -4874,6 +4880,36 @@
 apply(auto)
 done
 
+lemma detached_cp_the_preced:
+  assumes "detached s th"
+  shows "cp s th = the_preced s th" (is "?L = ?R")
+proof -
+  have "?L =  Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+      by (unfold cp_alt_def, simp)
+  moreover have "{th'. Th th' \<in> subtree (RAG s) (Th th)} = {th}" 
+  proof -
+    { fix n
+      assume "n \<in> subtree (RAG s) (Th th)"
+      hence "n = Th th"
+      proof(cases rule:subtreeE)
+        case 2
+        from 2(2) have "Th th \<in> Range (RAG s)"
+          by (elim ancestors_Field, simp)
+        moreover from assms[unfolded detached_test] have "Th th \<notin> Field (RAG s)" .
+        ultimately have False by (auto simp:Field_def)
+        thus ?thesis by simp
+      qed simp
+    } thus ?thesis by auto
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma detached_cp_preced:
+  assumes "detached s th"
+  shows "cp s th = preced th s" 
+  using detached_cp_the_preced[OF assms] 
+  by (simp add:the_preced_def)
+
 context valid_trace
 begin
 
@@ -5071,4 +5107,98 @@
 
 end
 
+lemma PIP_actorE:
+  assumes "PIP s e"
+  and "actor e = th"
+  and "\<not> isCreate e"
+  shows "th \<in> runing s"
+  using assms
+  by (cases, auto)
+
+
+lemma holdents_RAG:
+  assumes "holdents s th = {}"
+  shows "Th th \<notin> Range (RAG s)"
+proof
+  assume "Th th \<in> Range (RAG s)"
+  thus False
+  proof(rule RangeE)
+    fix a
+    assume "(a, Th th) \<in> RAG s"
+    with assms[unfolded holdents_test]
+    show False
+      by (cases a, auto simp:cs_RAG_raw s_RAG_abv)
+  qed
+qed
+
+lemma readys_RAG:
+  assumes "th \<in> readys s"
+  shows "Th th \<notin> Domain (RAG s)"
+proof
+  assume "Th th \<in> Domain (RAG s)"
+  thus False
+  proof(rule DomainE)
+    fix b
+    assume "(Th th, b) \<in> RAG s"
+    with assms[unfolded readys_def s_waiting_def]
+    show False
+      by (cases b, auto simp:cs_RAG_raw s_RAG_abv cs_waiting_raw)
+  qed
+qed
+
+lemma readys_holdents_detached:
+  assumes "th \<in> readys s"
+  and "holdents s th = {}"
+  shows "detached s th"
+proof -
+  from readys_RAG[OF assms(1)] holdents_RAG[OF assms(2)]
+  show ?thesis
+    by (unfold detached_test Field_def, auto)
+qed
+
+lemma len_actions_of_sigma:
+  assumes "finite A"
+  shows "length (actions_of A t) = (\<Sum> th' \<in> A. length (actions_of {th'} t))"
+proof(induct t)
+  case h: (Cons e t)
+  thus ?case (is "?L = ?R" is "_ = ?T (e#t)") 
+  proof(cases "actor e \<in> A")
+    case True
+    have "?L = 1 + ?T t"
+      by (fold h, insert True, simp add:actions_of_def)
+    moreover have "?R = 1 + ?T t"
+    proof -
+      have "?R = length (actions_of {actor e} (e # t)) +
+                 (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))"
+            (is "_ = ?F (e#t) + ?G (e#t)")
+            by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", 
+                OF assms True], simp)
+      moreover have "?F (e#t) = 1 + ?F t" using True
+          by  (simp add:actions_of_def)
+      moreover have "?G (e#t) = ?G t"
+        by (rule setsum.cong, auto simp:actions_of_def)
+      moreover have "?F t + ?G t = ?T t"
+        by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", 
+              OF assms True], simp)
+      ultimately show ?thesis by simp
+    qed
+    ultimately show ?thesis by simp
+  next
+    case False
+    hence "?L = length (actions_of A t)"
+      by (simp add:actions_of_def)
+    also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h)
+    also have "... = ?R"
+      by (rule setsum.cong; insert False, auto simp:actions_of_def)
+    finally show ?thesis .
+  qed
+qed (auto simp:actions_of_def)
+
+lemma threads_Exit:
+    assumes "th \<in> threads s"
+    and "th \<notin> threads (e#s)"
+    shows "e = Exit th"
+    using assms
+    by (cases e, auto)
+
 end