added lemma funpow_mult
authorhaftmann
Mon Jun 14 16:00:46 2010 +0200 (2010-06-14)
changeset 37430a77740fc3957
parent 37429 2f064f1c2f14
child 37431 e9004a3e0d94
added lemma funpow_mult
doc-src/Codegen/Thy/Further.thy
src/HOL/Nat.thy
     1.1 --- a/doc-src/Codegen/Thy/Further.thy	Mon Jun 14 15:27:11 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Further.thy	Mon Jun 14 16:00:46 2010 +0200
     1.3 @@ -14,11 +14,6 @@
     1.4  
     1.5  subsection {* Locales and interpretation *}
     1.6  
     1.7 -lemma funpow_mult: -- FIXME
     1.8 -  fixes f :: "'a \<Rightarrow> 'a"
     1.9 -  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
    1.10 -  by (induct n) (simp_all add: funpow_add)
    1.11 -
    1.12  text {*
    1.13    A technical issue comes to surface when generating code from
    1.14    specifications stemming from locale interpretation.
    1.15 @@ -86,7 +81,7 @@
    1.16  interpretation %quote fun_power: power "\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n" where
    1.17    "power.powers (\<lambda>n f. f ^^ n) = funpows"
    1.18    by unfold_locales
    1.19 -    (simp_all add: expand_fun_eq funpow_mult mult_commute funpows_def)
    1.20 +    (simp_all add: expand_fun_eq funpow_mult [symmetric] mult_commute funpows_def)
    1.21  
    1.22  text {*
    1.23    \noindent This additional equation is trivially proved by the definition
     2.1 --- a/src/HOL/Nat.thy	Mon Jun 14 15:27:11 2010 +0200
     2.2 +++ b/src/HOL/Nat.thy	Mon Jun 14 16:00:46 2010 +0200
     2.3 @@ -1203,9 +1203,9 @@
     2.4  lemmas [code_unfold] = funpow_code_def [symmetric]
     2.5  
     2.6  lemma [code]:
     2.7 +  "funpow (Suc n) f = f o funpow n f"
     2.8    "funpow 0 f = id"
     2.9 -  "funpow (Suc n) f = f o funpow n f"
    2.10 -  unfolding funpow_code_def by simp_all
    2.11 +  by (simp_all add: funpow_code_def)
    2.12  
    2.13  hide_const (open) funpow
    2.14  
    2.15 @@ -1213,6 +1213,11 @@
    2.16    "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
    2.17    by (induct m) simp_all
    2.18  
    2.19 +lemma funpow_mult:
    2.20 +  fixes f :: "'a \<Rightarrow> 'a"
    2.21 +  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
    2.22 +  by (induct n) (simp_all add: funpow_add)
    2.23 +
    2.24  lemma funpow_swap1:
    2.25    "f ((f ^^ n) x) = (f ^^ n) (f x)"
    2.26  proof -