src/HOL/Transitive_Closure.thy
changeset 29609 a010aab5bed0
parent 26801 244184661a09
child 30107 f3b3b0e3d184
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Transitive_Closure.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1992  University of Cambridge
     1.8  *)
     1.9 @@ -568,6 +567,22 @@
    1.10     apply auto
    1.11    done
    1.12  
    1.13 +lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
    1.14 +  apply clarify
    1.15 +  apply (erule trancl_induct)
    1.16 +   apply (auto simp add: Field_def)
    1.17 +  done
    1.18 +
    1.19 +lemma finite_trancl: "finite (r^+) = finite r"
    1.20 +  apply auto
    1.21 +   prefer 2
    1.22 +   apply (rule trancl_subset_Field2 [THEN finite_subset])
    1.23 +   apply (rule finite_SigmaI)
    1.24 +    prefer 3
    1.25 +    apply (blast intro: r_into_trancl' finite_subset)
    1.26 +   apply (auto simp add: finite_Field)
    1.27 +  done
    1.28 +
    1.29  text {* More about converse @{text rtrancl} and @{text trancl}, should
    1.30    be merged with main body. *}
    1.31