--- a/NEWS Tue Mar 03 19:08:04 2015 +0100
+++ b/NEWS Wed Mar 04 23:31:04 2015 +0100
@@ -68,6 +68,11 @@
*** HOL ***
+* removed functions "natfloor" and "natceiling",
+ use "nat o floor" and "nat o ceiling" instead.
+ A few of the lemmas have been retained and adapted: in their names
+ "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling".
+
* Qualified some duplicated fact names required for boostrapping
the type class hierarchy:
ab_add_uminus_conv_diff ~> diff_conv_add_uminus
--- a/src/HOL/Library/Extended_Real.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Mar 04 23:31:04 2015 +0100
@@ -2064,7 +2064,7 @@
by (cases m n rule: enat2_cases) auto
lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
- by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
+by (cases n) (auto)
lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
by (cases n) auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 04 23:31:04 2015 +0100
@@ -1156,15 +1156,15 @@
{
fix x b :: 'a
assume [simp]: "b \<in> Basis"
- have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
- by (rule real_natceiling_ge)
- also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
- by (auto intro!: natceiling_mono)
- also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
+ have "\<bar>x \<bullet> b\<bar> \<le> real (ceiling \<bar>x \<bullet> b\<bar>)"
+ by (rule real_of_int_ceiling_ge)
+ also have "\<dots> \<le> real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
+ by (auto intro!: ceiling_mono)
+ also have "\<dots> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
by simp
- finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
+ finally have "\<bar>x \<bullet> b\<bar> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
- by auto
+ by (metis order.strict_trans reals_Archimedean2)
moreover have "\<And>x b::'a. \<And>n::nat. \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
by auto
ultimately show ?thesis
--- a/src/HOL/Probability/Bochner_Integration.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Wed Mar 04 23:31:04 2015 +0100
@@ -2423,8 +2423,8 @@
from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
by (auto split: split_indicator intro!: monoI)
{ fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
- by (rule eventually_sequentiallyI[of "natceiling x"])
- (auto split: split_indicator simp: natceiling_le_eq) }
+ by (rule eventually_sequentiallyI[of "nat(ceiling x)"])
+ (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
from filterlim_cong[OF refl refl this]
have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
by simp
--- a/src/HOL/Probability/Borel_Space.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Mar 04 23:31:04 2015 +0100
@@ -1061,10 +1061,6 @@
by (auto simp: vimage_def measurable_count_space_eq2_countable)
qed
-lemma measurable_real_natfloor[measurable]:
- "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
- by (simp add: natfloor_def[abs_def])
-
lemma measurable_real_ceiling[measurable]:
"(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
unfolding ceiling_def[abs_def] by simp
@@ -1072,10 +1068,6 @@
lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
by simp
-lemma borel_measurable_real_natfloor:
- "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
- by simp
-
lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel"
by (intro borel_measurable_continuous_on1 continuous_intros)
--- a/src/HOL/Probability/Distributions.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Distributions.thy Wed Mar 04 23:31:04 2015 +0100
@@ -119,7 +119,7 @@
apply (intro nn_integral_LIMSEQ)
apply (auto simp: incseq_def le_fun_def eventually_sequentially
split: split_indicator intro!: Lim_eventually)
- apply (metis natceiling_le_eq)
+ apply (metis nat_ceiling_le_eq)
done
have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
--- a/src/HOL/Probability/Interval_Integral.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy Wed Mar 04 23:31:04 2015 +0100
@@ -68,11 +68,11 @@
with `a < b` have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
by (cases a) auto
moreover have " (\<lambda>x. ereal (real (Suc x))) ----> \<infinity>"
- using natceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
+ using nat_ceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>"
apply (subst LIMSEQ_Suc_iff)
apply (subst Lim_PInfty)
- apply (metis add.commute diff_le_eq natceiling_le_eq ereal_less_eq(3))
+ apply (metis add.commute diff_le_eq nat_ceiling_le_eq ereal_less_eq(3))
done
ultimately show thesis
by (intro that[of "\<lambda>i. real a + Suc i"])
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Mar 04 23:31:04 2015 +0100
@@ -207,12 +207,12 @@
lemma simple_function_ereal[intro, simp]:
fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
shows "simple_function M (\<lambda>x. ereal (f x))"
- by (auto intro!: simple_function_compose1[OF sf])
+ by (rule simple_function_compose1[OF sf])
lemma simple_function_real_of_nat[intro, simp]:
fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
shows "simple_function M (\<lambda>x. real (f x))"
- by (auto intro!: simple_function_compose1[OF sf])
+ by (rule simple_function_compose1[OF sf])
lemma borel_measurable_implies_simple_function_sequence:
fixes u :: "'a \<Rightarrow> ereal"
@@ -220,21 +220,21 @@
shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
(\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
proof -
- def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"
+ def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else nat(floor (real (u x) * 2 ^ i))"
{ fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
proof (split split_if, intro conjI impI)
assume "\<not> real j \<le> u x"
- then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
- by (cases "u x") (auto intro!: natfloor_mono)
- moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
- by (intro real_natfloor_le) auto
- ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
+ then have "nat(floor (real (u x) * 2 ^ j)) \<le> nat(floor (j * 2 ^ j))"
+ by (cases "u x") (auto intro!: nat_mono floor_mono)
+ moreover have "real (nat(floor (j * 2 ^ j))) \<le> j * 2^j"
+ by linarith
+ ultimately show "nat(floor (real (u x) * 2 ^ j)) \<le> j * 2 ^ j"
unfolding real_of_nat_le_iff by auto
qed auto }
note f_upper = this
have real_f:
- "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (natfloor (real (u x) * 2 ^ i)))"
+ "\<And>i x. real (f x i) = (if real i \<le> u x then i * 2 ^ i else real (nat(floor (real (u x) * 2 ^ i))))"
unfolding f_def by auto
let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
@@ -251,7 +251,7 @@
by (rule finite_subset) auto
qed
then show "simple_function M (?g i)"
- by (auto intro: simple_function_ereal simple_function_div)
+ by (auto)
next
show "incseq ?g"
proof (intro incseq_ereal incseq_SucI le_funI)
@@ -259,27 +259,27 @@
have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
proof ((split split_if)+, intro conjI impI)
assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
- then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"
- by (cases "u x") (auto intro!: le_natfloor)
+ then show "i * 2 ^ i * 2 \<le> nat(floor (real (u x) * 2 ^ Suc i))"
+ by (cases "u x") (auto intro!: le_nat_floor)
next
assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"
- then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"
+ then show "nat(floor (real (u x) * 2 ^ i)) * 2 \<le> Suc i * 2 ^ Suc i"
by (cases "u x") auto
next
assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
- have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"
+ have "nat(floor (real (u x) * 2 ^ i)) * 2 = nat(floor (real (u x) * 2 ^ i)) * nat(floor(2::real))"
by simp
- also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
+ also have "\<dots> \<le> nat(floor (real (u x) * 2 ^ i * 2))"
proof cases
assume "0 \<le> u x" then show ?thesis
- by (intro le_mult_natfloor)
+ by (intro le_mult_nat_floor)
next
assume "\<not> 0 \<le> u x" then show ?thesis
- by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
+ by (cases "u x") (auto simp: nat_floor_neg mult_nonpos_nonneg)
qed
- also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"
+ also have "\<dots> = nat(floor (real (u x) * 2 ^ Suc i))"
by (simp add: ac_simps)
- finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .
+ finally show "nat(floor (real (u x) * 2 ^ i)) * 2 \<le> nat(floor (real (u x) * 2 ^ Suc i))" .
qed simp
then show "?g i x \<le> ?g (Suc i) x"
by (auto simp: field_simps)
@@ -288,8 +288,7 @@
fix x show "(SUP i. ?g i x) = max 0 (u x)"
proof (rule SUP_eqI)
fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
- by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
- mult_nonpos_nonneg)
+ by (cases "u x") (auto simp: field_simps nat_floor_neg mult_nonpos_nonneg)
next
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
have "\<And>i. 0 \<le> ?g i x" by auto
@@ -309,11 +308,11 @@
obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
then have "r * 2^max N m < p * 2^max N m - 1" by simp
moreover
- have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
+ have "real (nat(floor (p * 2 ^ max N m))) \<le> r * 2 ^ max N m"
using *[of "max N m"] m unfolding real_f using ux
by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
- by (metis real_natfloor_gt_diff_one less_le_trans)
+ by linarith
ultimately show False by auto
qed
then show "max 0 (u x) \<le> y" using real ux by simp
--- a/src/HOL/Real.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Real.thy Wed Mar 04 23:31:04 2015 +0100
@@ -1680,6 +1680,10 @@
"numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
using real_of_nat_less_iff[of "numeral w" n] by simp
+lemma numeral_le_real_of_nat_iff[simp]:
+ "(numeral n \<le> real(m::nat)) = (numeral n \<le> m)"
+by (metis not_le real_of_nat_less_numeral_iff)
+
lemma numeral_le_real_of_int_iff [simp]:
"((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
by (simp add: linorder_not_less [symmetric])
@@ -1866,170 +1870,29 @@
"\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)"
using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp
-subsubsection {* Versions for the natural numbers *}
-
-definition
- natfloor :: "real => nat" where
- "natfloor x = nat(floor x)"
-
-definition
- natceiling :: "real => nat" where
- "natceiling x = nat(ceiling x)"
-
-lemma natfloor_split[arith_split]: "P (natfloor t) \<longleftrightarrow> (t < 0 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n \<le> t \<and> t < of_nat n + 1 \<longrightarrow> P n)"
-proof -
- have [dest]: "\<And>n m::nat. real n \<le> t \<Longrightarrow> t < real n + 1 \<Longrightarrow> real m \<le> t \<Longrightarrow> t < real m + 1 \<Longrightarrow> n = m"
- by simp
- show ?thesis
- by (auto simp: natfloor_def real_of_nat_def[symmetric] split: split_nat floor_split)
-qed
+text{* The following lemmas are remnants of the erstwhile functions natfloor
+and natceiling. *}
-lemma natceiling_split[arith_split]:
- "P (natceiling t) \<longleftrightarrow> (t \<le> - 1 \<longrightarrow> P 0) \<and> (\<forall>n. of_nat n - 1 < t \<and> t \<le> of_nat n \<longrightarrow> P n)"
-proof -
- have [dest]: "\<And>n m::nat. real n - 1 < t \<Longrightarrow> t \<le> real n \<Longrightarrow> real m - 1 < t \<Longrightarrow> t \<le> real m \<Longrightarrow> n = m"
- by simp
- show ?thesis
- by (auto simp: natceiling_def real_of_nat_def[symmetric] split: split_nat ceiling_split)
-qed
-
-lemma natfloor_zero [simp]: "natfloor 0 = 0"
- by linarith
-
-lemma natfloor_one [simp]: "natfloor 1 = 1"
- by linarith
-
-lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
- by (unfold natfloor_def, simp)
-
-lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
+lemma nat_floor_neg: "(x::real) <= 0 ==> nat(floor x) = 0"
by linarith
-lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
- by linarith
-
-lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
- by linarith
-
-lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
- by linarith
-
-lemma le_natfloor: "real x <= a ==> x <= natfloor a"
- by linarith
-
-lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
- by linarith
-
-lemma less_natfloor: "0 \<le> x \<Longrightarrow> x < real (n :: nat) \<Longrightarrow> natfloor x < n"
- by linarith
-
-lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
- by linarith
-
-lemma le_natfloor_eq_numeral [simp]:
- "0 \<le> x \<Longrightarrow> (numeral n \<le> natfloor x) = (numeral n \<le> x)"
- by (subst le_natfloor_eq, assumption) simp
-
-lemma le_natfloor_eq_one [simp]: "(1 \<le> natfloor x) = (1 \<le> x)"
- by linarith
-
-lemma natfloor_eq: "real n \<le> x \<Longrightarrow> x < real n + 1 \<Longrightarrow> natfloor x = n"
- by linarith
-
-lemma real_natfloor_add_one_gt: "x < real (natfloor x) + 1"
- by linarith
-
-lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
- by linarith
-
-lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
- by linarith
-
-lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
+lemma le_nat_floor: "real x <= a ==> x <= nat(floor a)"
by linarith
-lemma natfloor_add_numeral [simp]:
- "0 <= x \<Longrightarrow> natfloor (x + numeral n) = natfloor x + numeral n"
- by (simp add: natfloor_add [symmetric])
-
-lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
- by linarith
-
-lemma natfloor_subtract [simp]:
- "natfloor(x - real a) = natfloor x - a"
- by linarith
+lemma le_mult_nat_floor:
+ shows "nat(floor a) * nat(floor b) \<le> nat(floor (a * b))"
+ by (cases "0 <= a & 0 <= b")
+ (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)
-lemma natfloor_div_nat: "natfloor (x / real y) = natfloor x div y"
-proof cases
- assume "0 \<le> x" then show ?thesis
- unfolding natfloor_def real_of_int_of_nat_eq[symmetric]
- by (subst floor_divide_real_eq_div) (simp_all add: nat_div_distrib)
-qed (simp add: divide_nonpos_nonneg natfloor_neg)
-
-lemma natfloor_div_numeral[simp]:
- "natfloor (numeral x / numeral y) = numeral x div numeral y"
- using natfloor_div_nat[of "numeral x" "numeral y"] by simp
-
-lemma le_mult_natfloor:
- shows "natfloor a * natfloor b \<le> natfloor (a * b)"
- by (cases "0 <= a & 0 <= b")
- (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg)
-
-lemma natceiling_zero [simp]: "natceiling 0 = 0"
- by linarith
-
-lemma natceiling_one [simp]: "natceiling 1 = 1"
- by linarith
-
-lemma zero_le_natceiling [simp]: "0 <= natceiling x"
+lemma nat_ceiling_le_eq: "(nat(ceiling x) <= a) = (x <= real a)"
by linarith
-lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
- by (simp add: natceiling_def)
-
-lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
- by linarith
-
-lemma real_natceiling_ge: "x <= real(natceiling x)"
- by linarith
-
-lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
- by linarith
-
-lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
- by linarith
-
-lemma natceiling_le: "x <= real a ==> natceiling x <= a"
- by linarith
-
-lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
+lemma real_nat_ceiling_ge: "x <= real(nat(ceiling x))"
by linarith
-lemma natceiling_le_eq_numeral [simp]:
- "(natceiling x <= numeral n) = (x <= numeral n)"
- by (simp add: natceiling_le_eq)
-
-lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
- by linarith
-
-lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
- by linarith
-
-lemma natceiling_add [simp]: "0 <= x ==> natceiling (x + real a) = natceiling x + a"
- by linarith
-
-lemma natceiling_add_numeral [simp]:
- "0 <= x ==> natceiling (x + numeral n) = natceiling x + numeral n"
- by (simp add: natceiling_add [symmetric])
-
-lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
- by linarith
-
-lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
- by linarith
lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
- by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
+ by (auto intro!: bexI[of _ "of_nat (nat(ceiling x))"]) linarith
lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
@@ -2048,7 +1911,7 @@
show ?thesis unfolding real_of_int_inject[symmetric]
unfolding * floor_real_of_int ..
qed
-
+(*
lemma natfloor_power:
assumes "x = real (natfloor x)"
shows "natfloor (x ^ n) = natfloor x ^ n"
@@ -2059,7 +1922,7 @@
show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
by simp
qed
-
+*)
lemma floor_numeral_power[simp]:
"\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
by (metis floor_of_int of_int_numeral of_int_power)
--- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Mar 04 23:31:04 2015 +0100
@@ -1521,9 +1521,8 @@
lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
unfolding filterlim_at_top
apply (intro allI)
- apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
- apply (auto simp: natceiling_le_eq)
- done
+ apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
+ by linarith
subsubsection {* Limits of Sequences *}
--- a/src/HOL/Transcendental.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 04 23:31:04 2015 +0100
@@ -2054,9 +2054,9 @@
fixes i::real
shows "b powr i =
(if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
- else if floor i = i then (if 0 \<le> i then b ^ natfloor i else 1 / b ^ natfloor (- i))
+ else if floor i = i then (if 0 \<le> i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
- by (auto simp: natfloor_def powr_int)
+ by (auto simp: powr_int)
lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
using powr_realpow [of x 1] by simp