new lemma
authornipkow
Mon Jun 01 10:02:01 2009 +0200 (2009-06-01)
changeset 31351b8d856545a02
parent 31350 f20a61cec3d4
child 31354 2ad53771c30f
new lemma
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Transitive_Closure.thy	Sun May 31 22:00:56 2009 -0700
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jun 01 10:02:01 2009 +0200
     1.3 @@ -698,6 +698,9 @@
     1.4    apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
     1.5    done
     1.6  
     1.7 +lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
     1.8 +by(induct n) auto
     1.9 +
    1.10  lemma rtrancl_imp_UN_rel_pow:
    1.11    assumes "p \<in> R^*"
    1.12    shows "p \<in> (\<Union>n. R ^^ n)"