# HG changeset patch
# User haftmann
# Date 1264597373 -3600
# Node ID 4c316d777461bb5979e98fb08c4ebaf5532122d6
# Parent  acd6b305ffb5808b4ba719a578a1205ff24d00b5
lemma Image_closed_trancl

diff -r acd6b305ffb5 -r 4c316d777461 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Jan 27 14:02:52 2010 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Jan 27 14:02:53 2010 +0100
@@ -309,6 +309,25 @@
 apply (blast intro:rtrancl_trans)
 done
 
+lemma Image_closed_trancl:
+  assumes "r `` X \<subseteq> X" shows "r\<^sup>* `` X = X"
+proof -
+  from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto
+  have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X"
+  proof -
+    fix x y
+    assume *: "y \<in> X"
+    assume "(y, x) \<in> r\<^sup>*"
+    then show "x \<in> X"
+    proof induct
+      case base show ?case by (fact *)
+    next
+      case step with ** show ?case by auto
+    qed
+  qed
+  then show ?thesis by auto
+qed
+
 
 subsection {* Transitive closure *}