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