src/HOL/Nat.thy
changeset 49723 bbc2942ba09f
parent 49388 1ffd5a055acf
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Nat.thy	Fri Oct 05 18:01:48 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Oct 06 11:08:52 2012 +0200
     1.3 @@ -1249,6 +1249,19 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma funpow_Suc_right:
     1.8 +  "f ^^ Suc n = f ^^ n \<circ> f"
     1.9 +proof (induct n)
    1.10 +  case 0 then show ?case by simp
    1.11 +next
    1.12 +  fix n
    1.13 +  assume "f ^^ Suc n = f ^^ n \<circ> f"
    1.14 +  then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f"
    1.15 +    by (simp add: o_assoc)
    1.16 +qed
    1.17 +
    1.18 +lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
    1.19 +
    1.20  text {* for code generation *}
    1.21  
    1.22  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where