src/HOL/Transitive_Closure.thy
changeset 31970 ccaadfcf6941
parent 31690 cc37bf07f9bb
child 32215 87806301a813
     1.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:33:22 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:34:59 2009 +0200
     1.3 @@ -737,6 +737,9 @@
     1.4  lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
     1.5  by(induct n) auto
     1.6  
     1.7 +lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
     1.8 +  by (induct n) (simp, simp add: O_assoc [symmetric])
     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)"