--- a/PIPDefs.thy	Tue Jul 12 15:09:09 2016 +0100
+++ b/PIPDefs.thy	Tue Aug 16 11:49:37 2016 +0100
@@ -697,6 +697,42 @@
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
  by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
 
+text {*
+  A notion of {\em thread graph} (@{text tG}) is introduced to hide derivations using 
+  tRAG, so that it is easier to understand.
+*}
+
+
+definition "tG s = (map_prod the_thread the_thread) `(tRAG s)"
+
+lemma tG_alt_def: 
+  "tG s = {(th1, th2) | th1 th2. 
+                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R")
+proof -
+  { fix th1 th2
+    assume "(th1, th2) \<in> ?L" 
+    hence "(th1, th2) \<in> ?R" by (auto simp:tG_def tRAG_alt_def)
+  } moreover {
+    fix th1 th2
+    assume "(th1, th2) \<in> ?R"
+    then obtain cs where "(Th th1, Cs cs) \<in> RAG s" "(Cs cs, Th th2) \<in> RAG s" by auto
+    hence "(Th th1, Th th2) \<in> (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def)
+    hence "(Th th1, Th th2) \<in> tRAG s" by (unfold tRAG_def, simp)
+    hence "(th1, th2) \<in> ?L" by (simp add: tG_def rev_image_eqI)
+  } ultimately show ?thesis by (meson pred_equals_eq2)
+qed
+
+lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" (is "?L = ?R")
+proof -
+  have "?L = (\<lambda> x. x) ` ?L" by simp
+  also have "... = ?R"
+  proof(unfold tG_def image_comp, induct rule:image_cong)
+    case (2 e)
+    thus ?case by (unfold tRAG_alt_def, auto)
+  qed auto
+  finally show ?thesis .
+qed
+
 
 fun actor  where
   "actor (Exit th) = th" |