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