# HG changeset patch
# User nipkow
# Date 1425508264 -3600
# Node ID 8ea7b22525cbbc5de9de95a0e1330e0cbcd595a1
# Parent  cbc38731d42f18d9b645a1bde6ac60f3ab3e5752
Removed the obsolete functions "natfloor" and "natceiling"

diff -r cbc38731d42f -r 8ea7b22525cb NEWS
--- 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
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Library/Extended_Real.thy
--- 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
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Bochner_Integration.thy
--- 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
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Borel_Space.thy
--- 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)
 
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Distributions.thy
--- 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"
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Interval_Integral.thy
--- 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"])
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- 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
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Real.thy
--- 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)
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Real_Vector_Spaces.thy
--- 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 *}
 
diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Transcendental.thy
--- 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