src/HOL/Nat.thy
changeset 37430 a77740fc3957
parent 37387 3581483cca6c
child 37767 a2b7a20d6ea3
     1.1 --- a/src/HOL/Nat.thy	Mon Jun 14 15:27:11 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Jun 14 16:00:46 2010 +0200
     1.3 @@ -1203,9 +1203,9 @@
     1.4  lemmas [code_unfold] = funpow_code_def [symmetric]
     1.5  
     1.6  lemma [code]:
     1.7 +  "funpow (Suc n) f = f o funpow n f"
     1.8    "funpow 0 f = id"
     1.9 -  "funpow (Suc n) f = f o funpow n f"
    1.10 -  unfolding funpow_code_def by simp_all
    1.11 +  by (simp_all add: funpow_code_def)
    1.12  
    1.13  hide_const (open) funpow
    1.14  
    1.15 @@ -1213,6 +1213,11 @@
    1.16    "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
    1.17    by (induct m) simp_all
    1.18  
    1.19 +lemma funpow_mult:
    1.20 +  fixes f :: "'a \<Rightarrow> 'a"
    1.21 +  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
    1.22 +  by (induct n) (simp_all add: funpow_add)
    1.23 +
    1.24  lemma funpow_swap1:
    1.25    "f ((f ^^ n) x) = (f ^^ n) (f x)"
    1.26  proof -