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) 

(* NOT NEEDED : FIXME *)
lemma trancl_split: 
  "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)


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 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 single_valuedP_update:
  assumes "single_valuedP r"
  shows "single_valuedP (r(x := y))"
using assms
oops

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 "(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 "(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)"

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)
 



end