src/HOL/Transitive_Closure.thy
changeset 14337 e13731554e50
parent 14208 144f45277d5a
child 14361 ad2f5da643b4
--- a/src/HOL/Transitive_Closure.thy	Sat Jan 03 16:09:39 2004 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 05 00:46:06 2004 +0100
@@ -402,6 +402,16 @@
 text {* More about converse @{text rtrancl} and @{text trancl}, should
   be merged with main body. *}
 
+lemma single_valued_confluent:
+  "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>
+  \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*"
+apply(erule rtrancl_induct)
+ apply simp
+apply(erule disjE)
+ apply(blast elim:converse_rtranclE dest:single_valuedD)
+apply(blast intro:rtrancl_trans)
+done
+
 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
   by (fast intro: trancl_trans)