diff -r 0781a2fc93f1 -r 66ed924aaa5c Graphs.thy --- a/Graphs.thy Tue Jun 03 15:00:12 2014 +0100 +++ b/Graphs.thy Mon Jun 09 16:01:28 2014 +0100 @@ -7,49 +7,55 @@ shows "(x, y) \ r\<^sup>* \ (x, y) \ r\<^sup>+" using assms by (metis rtrancl_eq_or_trancl) +(* NOT NEEDED : FIXME *) lemma trancl_split: "(a, b) \ r^+ \ \ c. (a, c) \ r" by (induct rule:trancl_induct, auto) -lemma unique_minus: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq: "y \ z" - shows "(y, z) \ r^+" -by (metis converse_tranclE neq unique xy xz) + +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 unique_base: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq_yz: "y \ z" - shows "(y, z) \ r^+" -by (metis neq_yz unique unique_minus xy xz) +lemma single_valued_union: + assumes "single_valued r" "single_valued q" + and "Domain r \ Domain q = {}" + shows "single_valued (r \ q)" +using assms +unfolding single_valued_def +by auto -lemma unique_chain_star: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r^*" - and xz: "(x, z) \ r^*" - shows "(y, z) \ r^* \ (z, y) \ r^*" -thm single_valued_confluent single_valued_def unique xy xz -by (metis single_valued_confluent single_valued_def unique xy xz) +lemma single_valuedP_update: + assumes "single_valuedP r" + shows "single_valuedP (r(x := y))" +using assms +oops -lemma unique_chain: - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" +lemma single_valued_confluent2: + assumes unique: "single_valued r" and xy: "(x, y) \ r^+" and xz: "(x, z) \ r^+" and neq_yz: "y \ z" shows "(y, z) \ r^+ \ (z, y) \ r^+" proof - - have xy_star: "(x, y) \ r^*" - and xz_star: "(x, z) \ r^*" using xy xz by simp_all - from unique_chain_star[OF unique xy_star xz_star] + have "(x, y) \ r^*" "(x, z) \ r^*" using xy xz by simp_all + with single_valued_confluent[OF unique] have "(y, z) \ r\<^sup>* \ (z, y) \ r\<^sup>*" by auto with neq_yz - show ?thesis by(auto) + show "(y, z) \ r^+ \ (z, y) \ r^+" by simp qed +lemmas unique_chain = single_valued_confluent2 + + + definition funof :: "[('a * 'b)set, 'a] => 'b" where "funof r == (\x. THE y. (x, y) \ r)" @@ -64,8 +70,7 @@ "[|r `` {x} \ A; single_valued r; x \ Domain r|] ==> funof r x \ A" by (force simp add: funof_eq) -lemma single_valuedP_update: - shows "single_valuedP r \ single_valuedP (r(x := y))" -oops + + end \ No newline at end of file