| changeset 31351 | b8d856545a02 |
| parent 30971 | 7fbebf75b3ef |
| child 31576 | 525073f7aff6 |
--- a/src/HOL/Transitive_Closure.thy Sun May 31 22:00:56 2009 -0700 +++ b/src/HOL/Transitive_Closure.thy Mon Jun 01 10:02:01 2009 +0200 @@ -698,6 +698,9 @@ apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) done +lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m" +by(induct n) auto + lemma rtrancl_imp_UN_rel_pow: assumes "p \<in> R^*" shows "p \<in> (\<Union>n. R ^^ n)"