src/HOL/RComplete.thy
changeset 36826 4d4462d644ae
parent 36795 e05e1283c550
child 36979 da7c06ab3169
     1.1 --- a/src/HOL/RComplete.thy	Tue May 11 07:58:48 2010 -0700
     1.2 +++ b/src/HOL/RComplete.thy	Tue May 11 09:10:31 2010 -0700
     1.3 @@ -837,5 +837,27 @@
     1.4    apply simp
     1.5  done
     1.6  
     1.7 +subsection {* Exponentiation with floor *}
     1.8 +
     1.9 +lemma floor_power:
    1.10 +  assumes "x = real (floor x)"
    1.11 +  shows "floor (x ^ n) = floor x ^ n"
    1.12 +proof -
    1.13 +  have *: "x ^ n = real (floor x ^ n)"
    1.14 +    using assms by (induct n arbitrary: x) simp_all
    1.15 +  show ?thesis unfolding real_of_int_inject[symmetric]
    1.16 +    unfolding * floor_real_of_int ..
    1.17 +qed
    1.18 +
    1.19 +lemma natfloor_power:
    1.20 +  assumes "x = real (natfloor x)"
    1.21 +  shows "natfloor (x ^ n) = natfloor x ^ n"
    1.22 +proof -
    1.23 +  from assms have "0 \<le> floor x" by auto
    1.24 +  note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
    1.25 +  from floor_power[OF this]
    1.26 +  show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
    1.27 +    by simp
    1.28 +qed
    1.29  
    1.30  end