src/HOL/Transitive_Closure.thy
changeset 34970 4c316d777461
parent 34909 a799687944af
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 27 14:02:52 2010 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 27 14:02:53 2010 +0100
     1.3 @@ -309,6 +309,25 @@
     1.4  apply (blast intro:rtrancl_trans)
     1.5  done
     1.6  
     1.7 +lemma Image_closed_trancl:
     1.8 +  assumes "r `` X \<subseteq> X" shows "r\<^sup>* `` X = X"
     1.9 +proof -
    1.10 +  from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto
    1.11 +  have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X"
    1.12 +  proof -
    1.13 +    fix x y
    1.14 +    assume *: "y \<in> X"
    1.15 +    assume "(y, x) \<in> r\<^sup>*"
    1.16 +    then show "x \<in> X"
    1.17 +    proof induct
    1.18 +      case base show ?case by (fact *)
    1.19 +    next
    1.20 +      case step with ** show ?case by auto
    1.21 +    qed
    1.22 +  qed
    1.23 +  then show ?thesis by auto
    1.24 +qed
    1.25 +
    1.26  
    1.27  subsection {* Transitive closure *}
    1.28