diff -r 7ea6b019ce24 -r 0781a2fc93f1 Graphs.thy --- /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