src/HOL/Transitive_Closure.thy
 changeset 31577 ce3721fa1e17 parent 31576 525073f7aff6 child 31690 cc37bf07f9bb
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jun 11 22:17:13 2009 +0200
1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jun 11 23:13:02 2009 +0200
1.3 @@ -478,20 +478,6 @@
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
1.24 @@ -500,6 +486,28 @@
1.25
1.26  lemmas tranclD = tranclpD [to_set]
1.27
1.28 +lemma converse_tranclpE:
1.29 +  assumes major: "tranclp r x z"
1.30 +  assumes base: "r x z ==> P"
1.31 +  assumes step: "\<And> y. [| r x y; tranclp r y z |] ==> P"
1.32 +  shows P
1.33 +proof -
1.34 +  from tranclpD[OF major]
1.35 +  obtain y where "r x y" and "rtranclp r y z" by iprover
1.36 +  from this(2) show P
1.37 +  proof (cases rule: rtranclp.cases)
1.38 +    case rtrancl_refl
1.39 +    with `r x y` base show P by iprover
1.40 +  next
1.41 +    case rtrancl_into_rtrancl
1.42 +    from this have "tranclp r y z"
1.43 +      by (iprover intro: rtranclp_into_tranclp1)
1.44 +    with `r x y` step show P by iprover
1.45 +  qed
1.46 +qed
1.47 +
1.48 +lemmas converse_tranclE = converse_tranclpE [to_set]
1.49 +
1.50  lemma tranclD2:
1.51    "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
1.52    by (blast elim: tranclE intro: trancl_into_rtrancl)
```