src/HOL/Power.thy
changeset 49824 c26665a197dc
parent 47255 30a1692557b0
child 51263 31e786e0e6a7
     1.1 --- a/src/HOL/Power.thy	Thu Oct 11 11:56:43 2012 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Oct 11 11:56:43 2012 +0200
     1.3 @@ -90,6 +90,19 @@
     1.4    unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
     1.5    unfolding power_Suc power_add Let_def mult_assoc ..
     1.6  
     1.7 +lemma funpow_times_power:
     1.8 +  "(times x ^^ f x) = times (x ^ f x)"
     1.9 +proof (induct "f x" arbitrary: f)
    1.10 +  case 0 then show ?case by (simp add: fun_eq_iff)
    1.11 +next
    1.12 +  case (Suc n)
    1.13 +  def g \<equiv> "\<lambda>x. f x - 1"
    1.14 +  with Suc have "n = g x" by simp
    1.15 +  with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    1.16 +  moreover from Suc g_def have "f x = g x + 1" by simp
    1.17 +  ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc)
    1.18 +qed
    1.19 +
    1.20  end
    1.21  
    1.22  context comm_monoid_mult
    1.23 @@ -727,3 +740,4 @@
    1.24    Power Arith
    1.25  
    1.26  end
    1.27 +