# HG changeset patch
# User krauss
# Date 1247153699 -7200
# Node ID ccaadfcf6941479b71b97e935ea95c9a4747a2e4
# Parent  09524788a6b994f27cef0da22e5a2c7e2cb30562
move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure

diff -r 09524788a6b9 -r ccaadfcf6941 src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Thu Jul 09 17:33:22 2009 +0200
+++ b/src/HOL/IMP/Machines.thy	Thu Jul 09 17:34:59 2009 +0200
@@ -2,9 +2,6 @@
 imports Natural
 begin
 
-lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
-  by (induct n) (simp, simp add: O_assoc [symmetric])
-
 lemma converse_in_rel_pow_eq:
   "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
 apply(rule iffI)
diff -r 09524788a6b9 -r ccaadfcf6941 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)"