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