--- a/src/HOL/Nat.thy Mon Jun 14 15:27:11 2010 +0200
+++ b/src/HOL/Nat.thy Mon Jun 14 16:00:46 2010 +0200
@@ -1203,9 +1203,9 @@
lemmas [code_unfold] = funpow_code_def [symmetric]
lemma [code]:
+ "funpow (Suc n) f = f o funpow n f"
"funpow 0 f = id"
- "funpow (Suc n) f = f o funpow n f"
- unfolding funpow_code_def by simp_all
+ by (simp_all add: funpow_code_def)
hide_const (open) funpow
@@ -1213,6 +1213,11 @@
"f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
by (induct m) simp_all
+lemma funpow_mult:
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "(f ^^ m) ^^ n = f ^^ (m * n)"
+ by (induct n) (simp_all add: funpow_add)
+
lemma funpow_swap1:
"f ((f ^^ n) x) = (f ^^ n) (f x)"
proof -