diff -r 7003308ff73a -r 156bba334c12 src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Sun Oct 30 10:55:56 2005 +0100
+++ b/src/HOL/Relation_Power.thy	Mon Oct 31 01:43:22 2005 +0100
@@ -38,6 +38,14 @@
 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
 by(induct m) simp_all
 
+lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
+proof -
+  have "f((f^n) x) = (f^(n+1)) x" by simp
+  also have "\<dots>  = (f^n o f^1) x" by (simp only:funpow_add)
+  also have "\<dots> = (f^n)(f x)" by simp
+  finally show ?thesis .
+qed
+
 lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
 by simp
 declare rel_pow_1 [simp]