--- a/src/HOL/Transitive_Closure.thy Thu Jun 11 22:17:13 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 11 23:13:02 2009 +0200
@@ -478,20 +478,6 @@
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
@@ -500,6 +486,28 @@
lemmas tranclD = tranclpD [to_set]
+lemma converse_tranclpE:
+ assumes major: "tranclp r x z"
+ assumes base: "r x z ==> P"
+ assumes step: "\<And> y. [| r x y; tranclp r y z |] ==> P"
+ shows P
+proof -
+ from tranclpD[OF major]
+ obtain y where "r x y" and "rtranclp r y z" by iprover
+ from this(2) show P
+ proof (cases rule: rtranclp.cases)
+ case rtrancl_refl
+ with `r x y` base show P by iprover
+ next
+ case rtrancl_into_rtrancl
+ from this have "tranclp r y z"
+ by (iprover intro: rtranclp_into_tranclp1)
+ with `r x y` step show P by iprover
+ qed
+qed
+
+lemmas converse_tranclE = converse_tranclpE [to_set]
+
lemma tranclD2:
"(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
by (blast elim: tranclE intro: trancl_into_rtrancl)