
diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Transitive_Closure.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
@@ -568,6 +567,22 @@
    apply auto
   done
 
+lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
+  apply clarify
+  apply (erule trancl_induct)
+   apply (auto simp add: Field_def)
+  done
+
+lemma finite_trancl: "finite (r^+) = finite r"
+  apply auto
+   prefer 2
+   apply (rule trancl_subset_Field2 [THEN finite_subset])
+   apply (rule finite_SigmaI)
+    prefer 3
+    apply (blast intro: r_into_trancl' finite_subset)
+   apply (auto simp add: finite_Field)
+  done
+
 text {* More about converse @{text rtrancl} and @{text trancl}, should
   be merged with main body. *}
 




