--- a/Test.thy	Mon Jun 02 14:58:42 2014 +0100
+++ b/Test.thy	Tue Jun 03 15:00:12 2014 +0100
@@ -1,5 +1,5 @@
 theory Test 
-imports Precedence_ord
+imports Precedence_ord Graphs
 begin
 
 type_synonym thread = nat -- {* Type for thread identifiers. *}
@@ -244,7 +244,21 @@
 using assms wq_distinct[OF vt(1), of"cs"]
 by (auto simp add: Let_def wq_def)
 
-lemma waiting_unique:
+(*
+lemma single_valued_waits2:
+  assumes "vt s"
+  shows "single_valuedP (waits2 s)"
+using assms
+apply(induct)
+apply(simp add: waits2_def waits_def)
+apply(erule step.cases)
+apply(auto simp add: Let_def waits2_def)
+unfolding single_valued_def waits2_def waits_def
+apply(auto)
+*)
+
+
+lemma waits2_unique:
   assumes "vt s"
   and "waits2 s th cs1"
   and "waits2 s th cs2"
@@ -260,11 +274,34 @@
 apply (metis distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
 by (metis (full_types, hide_lams) distinct.simps(2) distinct_length_2_or_more list.sel(1) wq_def wq_distinct)
 
+lemma single_valued_holds2:
+  assumes "vt s"
+  shows "single_valuedP (\<lambda>cs th. holds2 s th cs)"
+unfolding single_valued_def holds2_def holds_def by simp
 
-lemma rtrancl_eq_trancl [simp]:
-  assumes "x \<noteq> y"
-  shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
-using assms by (metis rtrancl_eq_or_trancl) 
+
+lemma holds2_unique: 
+  assumes "holds2 s th1 cs"
+  and      "holds2 s th2 cs"
+  shows "th1 = th2"
+using assms
+unfolding holds2_def holds_def by auto
+
+lemma single_valued_waits2:
+  assumes "vt s"
+  shows "single_valuedP (waits2 s)"
+by (metis (erased, hide_lams) assms mem_Collect_eq old.prod.case single_valued_def waits2_unique)
+
+
+(* was unique_RAG2 *)
+lemma single_valued_RAG2:
+  assumes "vt s"
+  shows "single_valued (RAG2 s)"
+using single_valued_waits2[OF assms] single_valued_holds2[OF assms] 
+unfolding RAG2_def RAG_def 
+unfolding single_valued_def
+unfolding holds2_def waits2_def 
+by auto 
 
 lemma acyclic_RAG_step: 
   assumes vt: "vt s"
@@ -337,7 +374,7 @@
         have "waits2 s nth cs'" 
           using b(2) unfolding RAG2_def RAG_def waits2_def by simp
         ultimately have "cs = cs'" 
-          by (rule_tac waiting_unique[OF vt waits2_cs])
+          by (rule_tac waits2_unique[OF vt waits2_cs])
         then show "False" using a b(1) by simp
       qed
       ultimately 
@@ -416,4 +453,45 @@
 oops
 
 
+
+
+
+
+lemma dchain_unique:
+  assumes vt: "vt s"
+  and th1_d: "(n, Th th1) \<in> (RAG2 s)^+"
+  and th1_r: "th1 \<in> readys s"
+  and th2_d: "(n, Th th2) \<in> (RAG2 s)^+"
+  and th2_r: "th2 \<in> readys s"
+  shows "th1 = th2"
+proof(rule ccontr)
+  assume neq: "th1 \<noteq> th2"
+  hence "Th th1 \<noteq> Th th2" by simp
+  from unique_chain [OF _ th1_d th2_d this] and single_valued_RAG2 [OF vt]
+  have "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG2 s)\<^sup>+" 
+    unfolding single_valued_def by auto
+  then show "False"
+  proof
+    assume "(Th th1, Th th2) \<in> (RAG2 s)\<^sup>+"      
+    from trancl_split [OF this]
+    obtain n where dd: "(Th th1, n) \<in> RAG2 s" by auto
+    then obtain cs where eq_n: "n = Cs cs"
+      unfolding RAG2_def RAG_def by (case_tac n) (auto)
+    from dd eq_n have "th1 \<notin> readys s"
+      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
+    with th1_r show ?thesis by auto
+  next
+    assume "(Th th2, Th th1) \<in> (RAG2 s)\<^sup>+"
+    from trancl_split [OF this]
+    obtain n where dd: "(Th th2, n) \<in> RAG2 s" by auto
+    then obtain cs where eq_n: "n = Cs cs"
+      unfolding RAG2_def RAG_def by (case_tac n) (auto)
+    from dd eq_n have "th2 \<notin> readys s"
+      unfolding RAG2_def RAG_def waits2_def readys_def by (auto)
+    with th2_r show ?thesis by auto
+  qed
+qed
+
+
+
 end
\ No newline at end of file