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