src/HOL/Transitive_Closure.thy
changeset 31576 525073f7aff6
parent 31351 b8d856545a02
child 31577 ce3721fa1e17
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jun 11 22:04:23 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jun 11 22:17:13 2009 +0200
     1.3 @@ -478,6 +478,20 @@
     1.4  
     1.5  lemmas converse_trancl_induct = converse_tranclp_induct [to_set]
     1.6  
     1.7 +lemma converse_tranclpE:
     1.8 +  assumes "tranclp r x z "
     1.9 +  assumes "r x z ==> P"
    1.10 +  assumes "\<And> y. [| r x y; tranclp r y z |] ==> P"
    1.11 +  shows P
    1.12 +proof -
    1.13 +  from tranclpD[OF assms(1)]
    1.14 +  obtain y where "r x y" and "rtranclp r y z" by iprover
    1.15 +  with assms(2-3) rtranclpD[OF this(2)] this(1)
    1.16 +  show P by iprover
    1.17 +qed  
    1.18 +
    1.19 +lemmas converse_tranclE = converse_tranclpE [to_set]
    1.20 +
    1.21  lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y"
    1.22    apply (erule converse_tranclp_induct)
    1.23     apply auto