--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Graphs.thy	Tue Jun 03 15:00:12 2014 +0100
@@ -0,0 +1,71 @@
+theory Graphs
+imports Main
+begin
+
+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 trancl_split: 
+  "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
+by (induct rule:trancl_induct, auto)
+
+lemma unique_minus:
+  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+  and xy: "(x, y) \<in> r"
+  and xz: "(x, z) \<in> r^+"
+  and neq: "y \<noteq> z"
+  shows "(y, z) \<in> r^+"
+by (metis converse_tranclE neq unique xy xz)
+
+lemma unique_base:
+  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+  and xy: "(x, y) \<in> r"
+  and xz: "(x, z) \<in> r^+"
+  and neq_yz: "y \<noteq> z"
+  shows "(y, z) \<in> r^+"
+by (metis neq_yz unique unique_minus xy xz)
+
+lemma unique_chain_star:
+  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+  and xy: "(x, y) \<in> r^*"
+  and xz: "(x, z) \<in> r^*"
+  shows "(y, z) \<in> r^* \<or> (z, y) \<in> r^*"
+thm single_valued_confluent single_valued_def unique xy xz
+by (metis single_valued_confluent single_valued_def unique xy xz)
+
+lemma unique_chain:
+  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+  and xy: "(x, y) \<in> r^+"
+  and xz: "(x, z) \<in> r^+"
+  and neq_yz: "y \<noteq> z"
+  shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"
+proof -
+  have xy_star: "(x, y) \<in> r^*"
+  and  xz_star: "(x, z) \<in> r^*" using xy xz by simp_all
+  from unique_chain_star[OF unique xy_star xz_star]
+  have "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" by auto
+  with neq_yz
+  show ?thesis by(auto)
+qed
+
+definition funof :: "[('a * 'b)set, 'a] => 'b" where
+   "funof r == (\<lambda>x. THE y. (x, y) \<in> r)"
+
+lemma funof_eq: "[|single_valued r; (x, y) \<in> r|] ==> funof r x = y"
+by (simp add: funof_def single_valued_def, blast)
+
+lemma funof_Pair_in:
+     "[|single_valued r; x \<in> Domain r|] ==> (x, funof r x) \<in> r"
+by (force simp add: funof_eq) 
+
+lemma funof_in:
+     "[|r `` {x} \<subseteq> A; single_valued r; x \<in> Domain r|] ==> funof r x \<in> A" 
+by (force simp add: funof_eq)
+ 
+lemma single_valuedP_update:
+  shows "single_valuedP r \<Longrightarrow> single_valuedP (r(x := y))"
+oops
+
+end
\ No newline at end of file

--- 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