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