--- a/Graphs.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/Graphs.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -7,49 +7,55 @@
   shows "(x, y) \<in> r\<^sup>* \<longleftrightarrow> (x, y) \<in> r\<^sup>+"
 using assms by (metis rtrancl_eq_or_trancl) 
 
+(* NOT NEEDED : FIXME *)
 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)
+
+section {* Single_Valuedness *}
+
+lemma single_valued_Collect:
+  assumes "single_valuedP r"
+  and "inj f"
+  shows "single_valued {(f x, g y) | x y. r x y}"
+using assms
+unfolding single_valued_def inj_on_def
+apply(auto)
+done
 
-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 single_valued_union:
+  assumes "single_valued r" "single_valued q"
+  and "Domain r \<inter> Domain q = {}"
+  shows "single_valued (r \<union> q)"
+using assms
+unfolding single_valued_def
+by auto
 
-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 single_valuedP_update:
+  assumes "single_valuedP r"
+  shows "single_valuedP (r(x := y))"
+using assms
+oops
 
-lemma unique_chain:
-  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
+lemma single_valued_confluent2:
+  assumes unique: "single_valued r"
   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 "(x, y) \<in> r^*" "(x, z) \<in> r^*" using xy xz by simp_all
+  with single_valued_confluent[OF unique]
   have "(y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*" by auto
   with neq_yz
-  show ?thesis by(auto)
+  show "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" by simp
 qed
 
+lemmas unique_chain = single_valued_confluent2
+
+
+
 definition funof :: "[('a * 'b)set, 'a] => 'b" where
    "funof r == (\<lambda>x. THE y. (x, y) \<in> r)"
 
@@ -64,8 +70,7 @@
      "[|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