added lemma
authorbulwahn
Thu Jun 11 23:13:02 2009 +0200 (2009-06-11)
changeset 31577ce3721fa1e17
parent 31576 525073f7aff6
child 31578 86eeb9b7a4ba
added lemma
src/HOL/Transitive_Closure.thy
     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)