src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:33:22 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:34:59 2009 +0200
@@ -737,6 +737,9 @@
 lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
 by(induct n) auto
 
+lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
+  by (induct n) (simp, simp add: O_assoc [symmetric])
+
 lemma rtrancl_imp_UN_rel_pow:
   assumes "p \<in> R^*"
   shows "p \<in> (\<Union>n. R ^^ n)"