# HG changeset patch
# User haftmann
# Date 1276524046 -7200
# Node ID a77740fc3957f9b40d9d9e2e4d2f1fb1ad284123
# Parent  2f064f1c2f14209aa14b93a6da2a8a037e41b837
added lemma funpow_mult

diff -r 2f064f1c2f14 -r a77740fc3957 doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy	Mon Jun 14 15:27:11 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Mon Jun 14 16:00:46 2010 +0200
@@ -14,11 +14,6 @@
 
 subsection {* Locales and interpretation *}
 
-lemma funpow_mult: -- FIXME
-  fixes f :: "'a \<Rightarrow> 'a"
-  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
-  by (induct n) (simp_all add: funpow_add)
-
 text {*
   A technical issue comes to surface when generating code from
   specifications stemming from locale interpretation.
@@ -86,7 +81,7 @@
 interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
   "power.powers (\<lambda>n f. f ^^ n) = funpows"
   by unfold_locales
-    (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
+    (simp_all add: expand_fun_eq funpow_mult [symmetric] mult_commute funpows_def)
 
 text {*
   \noindent This additional equation is trivially proved by the definition
diff -r 2f064f1c2f14 -r a77740fc3957 src/HOL/Nat.thy
--- 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 -