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 \ 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. *}