700 text {*

   701   A notion of {\em thread graph} (@{text tG}) is introduced to hide derivations using 

   702   tRAG, so that it is easier to understand.

   703 *}

   704 

   705 

   706 definition "tG s = (map_prod the_thread the_thread) `(tRAG s)"

   707 

   708 lemma tG_alt_def: 

   709   "tG s = {(th1, th2) | th1 th2. 

   710                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R")

   711 proof -

   712   { fix th1 th2

   713     assume "(th1, th2) \<in> ?L" 

   714     hence "(th1, th2) \<in> ?R" by (auto simp:tG_def tRAG_alt_def)

   715   } moreover {

   716     fix th1 th2

   717     assume "(th1, th2) \<in> ?R"

   718     then obtain cs where "(Th th1, Cs cs) \<in> RAG s" "(Cs cs, Th th2) \<in> RAG s" by auto

   719     hence "(Th th1, Th th2) \<in> (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def)

   720     hence "(Th th1, Th th2) \<in> tRAG s" by (unfold tRAG_def, simp)

   721     hence "(th1, th2) \<in> ?L" by (simp add: tG_def rev_image_eqI)

   722   } ultimately show ?thesis by (meson pred_equals_eq2)

   723 qed

   724 

   725 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" (is "?L = ?R")

   726 proof -

   727   have "?L = (\<lambda> x. x) ` ?L" by simp

   728   also have "... = ?R"

   729   proof(unfold tG_def image_comp, induct rule:image_cong)

   730     case (2 e)

   731     thus ?case by (unfold tRAG_alt_def, auto)

   732   qed auto

   733   finally show ?thesis .

   734 qed

   735