--- 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)
--- 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)"