# HG changeset patch
# User bulwahn
# Date 1244751433 -7200
# Node ID 525073f7aff6d9b6a9ead87a61a306a3c34823d8
# Parent  2263d89fa9308aa17e94e091ece7a3e9c6536442
added lemma

diff -r 2263d89fa930 -r 525073f7aff6 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Jun 11 22:04:23 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Jun 11 22:17:13 2009 +0200
@@ -478,6 +478,20 @@
 
 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
 
+lemma converse_tranclpE:
+  assumes "tranclp r x z "
+  assumes "r x z ==> P"
+  assumes "\<And> y. [| r x y; tranclp r y z |] ==> P"
+  shows P
+proof -
+  from tranclpD[OF assms(1)]
+  obtain y where "r x y" and "rtranclp r y z" by iprover
+  with assms(2-3) rtranclpD[OF this(2)] this(1)
+  show P by iprover
+qed  
+
+lemmas converse_tranclE = converse_tranclpE [to_set]
+
 lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y"
   apply (erule converse_tranclp_induct)
    apply auto