src/HOL/Transitive_Closure.thy

 (*  Title:      HOL/Transitive_Closure.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
 
 header {* Reflexive and Transitive closure of a relation *}

   apply (erule rev_mp)
   apply (erule rtrancl_induct)
    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. *}
 
 lemma single_valued_confluent:
   "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>