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