Removed the obsolete functions "natfloor" and "natceiling"
authornipkow
Wed Mar 04 23:31:04 2015 +0100 (2015-03-04)
changeset 595878ea7b22525cb
parent 59580 cbc38731d42f
child 59588 c6f3dbe466b6
Removed the obsolete functions "natfloor" and "natceiling"
NEWS
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Interval_Integral.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/NEWS	Wed Mar 04 23:31:04 2015 +0100
     1.3 @@ -68,6 +68,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* removed functions "natfloor" and "natceiling",
     1.8 +  use "nat o floor" and "nat o ceiling" instead.
     1.9 +  A few of the lemmas have been retained and adapted: in their names
    1.10 +  "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling".
    1.11 +
    1.12  * Qualified some duplicated fact names required for boostrapping
    1.13  the type class hierarchy:
    1.14    ab_add_uminus_conv_diff ~> diff_conv_add_uminus
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 03 19:08:04 2015 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 04 23:31:04 2015 +0100
     2.3 @@ -2064,7 +2064,7 @@
     2.4    by (cases m n rule: enat2_cases) auto
     2.5  
     2.6  lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
     2.7 -  by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
     2.8 +by (cases n) (auto)
     2.9  
    2.10  lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
    2.11    by (cases n) auto
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 03 19:08:04 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 04 23:31:04 2015 +0100
     3.3 @@ -1156,15 +1156,15 @@
     3.4    {
     3.5      fix x b :: 'a
     3.6      assume [simp]: "b \<in> Basis"
     3.7 -    have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
     3.8 -      by (rule real_natceiling_ge)
     3.9 -    also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    3.10 -      by (auto intro!: natceiling_mono)
    3.11 -    also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    3.12 +    have "\<bar>x \<bullet> b\<bar> \<le> real (ceiling \<bar>x \<bullet> b\<bar>)"
    3.13 +      by (rule real_of_int_ceiling_ge)
    3.14 +    also have "\<dots> \<le> real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    3.15 +      by (auto intro!: ceiling_mono)
    3.16 +    also have "\<dots> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    3.17        by simp
    3.18 -    finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
    3.19 +    finally have "\<bar>x \<bullet> b\<bar> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
    3.20    then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
    3.21 -    by auto
    3.22 +    by (metis order.strict_trans reals_Archimedean2)
    3.23    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"
    3.24      by auto
    3.25    ultimately show ?thesis
     4.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Tue Mar 03 19:08:04 2015 +0100
     4.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Mar 04 23:31:04 2015 +0100
     4.3 @@ -2423,8 +2423,8 @@
     4.4    from nonneg have "AE x in M. mono (\<lambda>n::nat. f x * indicator {..real n} x)"
     4.5      by (auto split: split_indicator intro!: monoI)
     4.6    { fix x have "eventually (\<lambda>n. f x * indicator {..real n} x = f x) sequentially"
     4.7 -      by (rule eventually_sequentiallyI[of "natceiling x"])
     4.8 -         (auto split: split_indicator simp: natceiling_le_eq) }
     4.9 +      by (rule eventually_sequentiallyI[of "nat(ceiling x)"])
    4.10 +         (auto split: split_indicator simp: nat_le_iff ceiling_le_iff) }
    4.11    from filterlim_cong[OF refl refl this]
    4.12    have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
    4.13      by simp
     5.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 03 19:08:04 2015 +0100
     5.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Mar 04 23:31:04 2015 +0100
     5.3 @@ -1061,10 +1061,6 @@
     5.4      by (auto simp: vimage_def measurable_count_space_eq2_countable)
     5.5  qed
     5.6  
     5.7 -lemma measurable_real_natfloor[measurable]:
     5.8 -  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
     5.9 -  by (simp add: natfloor_def[abs_def])
    5.10 -
    5.11  lemma measurable_real_ceiling[measurable]:
    5.12    "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
    5.13    unfolding ceiling_def[abs_def] by simp
    5.14 @@ -1072,10 +1068,6 @@
    5.15  lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
    5.16    by simp
    5.17  
    5.18 -lemma borel_measurable_real_natfloor:
    5.19 -  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
    5.20 -  by simp
    5.21 -
    5.22  lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel"
    5.23    by (intro borel_measurable_continuous_on1 continuous_intros)
    5.24  
     6.1 --- a/src/HOL/Probability/Distributions.thy	Tue Mar 03 19:08:04 2015 +0100
     6.2 +++ b/src/HOL/Probability/Distributions.thy	Wed Mar 04 23:31:04 2015 +0100
     6.3 @@ -119,7 +119,7 @@
     6.4      apply (intro nn_integral_LIMSEQ)
     6.5      apply (auto simp: incseq_def le_fun_def eventually_sequentially
     6.6                  split: split_indicator intro!: Lim_eventually)
     6.7 -    apply (metis natceiling_le_eq)
     6.8 +    apply (metis nat_ceiling_le_eq)
     6.9      done
    6.10  
    6.11    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"
     7.1 --- a/src/HOL/Probability/Interval_Integral.thy	Tue Mar 03 19:08:04 2015 +0100
     7.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Wed Mar 04 23:31:04 2015 +0100
     7.3 @@ -68,11 +68,11 @@
     7.4    with `a < b` have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
     7.5      by (cases a) auto
     7.6    moreover have " (\<lambda>x. ereal (real (Suc x))) ----> \<infinity>"
     7.7 -    using natceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
     7.8 +    using nat_ceiling_le_eq by (subst LIMSEQ_Suc_iff) (auto simp: Lim_PInfty)
     7.9    moreover have "\<And>r. (\<lambda>x. ereal (r + real (Suc x))) ----> \<infinity>"
    7.10      apply (subst LIMSEQ_Suc_iff)
    7.11      apply (subst Lim_PInfty)
    7.12 -    apply (metis add.commute diff_le_eq natceiling_le_eq ereal_less_eq(3))
    7.13 +    apply (metis add.commute diff_le_eq nat_ceiling_le_eq ereal_less_eq(3))
    7.14      done
    7.15    ultimately show thesis
    7.16      by (intro that[of "\<lambda>i. real a + Suc i"])
     8.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Mar 03 19:08:04 2015 +0100
     8.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Mar 04 23:31:04 2015 +0100
     8.3 @@ -207,12 +207,12 @@
     8.4  lemma simple_function_ereal[intro, simp]: 
     8.5    fixes f g :: "'a \<Rightarrow> real" assumes sf: "simple_function M f"
     8.6    shows "simple_function M (\<lambda>x. ereal (f x))"
     8.7 -  by (auto intro!: simple_function_compose1[OF sf])
     8.8 +  by (rule simple_function_compose1[OF sf])
     8.9  
    8.10  lemma simple_function_real_of_nat[intro, simp]: 
    8.11    fixes f g :: "'a \<Rightarrow> nat" assumes sf: "simple_function M f"
    8.12    shows "simple_function M (\<lambda>x. real (f x))"
    8.13 -  by (auto intro!: simple_function_compose1[OF sf])
    8.14 +  by (rule simple_function_compose1[OF sf])
    8.15  
    8.16  lemma borel_measurable_implies_simple_function_sequence:
    8.17    fixes u :: "'a \<Rightarrow> ereal"
    8.18 @@ -220,21 +220,21 @@
    8.19    shows "\<exists>f. incseq f \<and> (\<forall>i. \<infinity> \<notin> range (f i) \<and> simple_function M (f i)) \<and>
    8.20               (\<forall>x. (SUP i. f i x) = max 0 (u x)) \<and> (\<forall>i x. 0 \<le> f i x)"
    8.21  proof -
    8.22 -  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else natfloor (real (u x) * 2 ^ i)"
    8.23 +  def f \<equiv> "\<lambda>x i. if real i \<le> u x then i * 2 ^ i else nat(floor (real (u x) * 2 ^ i))"
    8.24    { fix x j have "f x j \<le> j * 2 ^ j" unfolding f_def
    8.25      proof (split split_if, intro conjI impI)
    8.26        assume "\<not> real j \<le> u x"
    8.27 -      then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
    8.28 -         by (cases "u x") (auto intro!: natfloor_mono)
    8.29 -      moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
    8.30 -        by (intro real_natfloor_le) auto
    8.31 -      ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
    8.32 +      then have "nat(floor (real (u x) * 2 ^ j)) \<le> nat(floor (j * 2 ^ j))"
    8.33 +         by (cases "u x") (auto intro!: nat_mono floor_mono)
    8.34 +      moreover have "real (nat(floor (j * 2 ^ j))) \<le> j * 2^j"
    8.35 +        by linarith
    8.36 +      ultimately show "nat(floor (real (u x) * 2 ^ j)) \<le> j * 2 ^ j"
    8.37          unfolding real_of_nat_le_iff by auto
    8.38      qed auto }
    8.39    note f_upper = this
    8.40  
    8.41    have real_f:
    8.42 -    "\<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)))"
    8.43 +    "\<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))))"
    8.44      unfolding f_def by auto
    8.45  
    8.46    let ?g = "\<lambda>j x. real (f x j) / 2^j :: ereal"
    8.47 @@ -251,7 +251,7 @@
    8.48          by (rule finite_subset) auto
    8.49      qed
    8.50      then show "simple_function M (?g i)"
    8.51 -      by (auto intro: simple_function_ereal simple_function_div)
    8.52 +      by (auto)
    8.53    next
    8.54      show "incseq ?g"
    8.55      proof (intro incseq_ereal incseq_SucI le_funI)
    8.56 @@ -259,27 +259,27 @@
    8.57        have "f x i * 2 \<le> f x (Suc i)" unfolding f_def
    8.58        proof ((split split_if)+, intro conjI impI)
    8.59          assume "ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
    8.60 -        then show "i * 2 ^ i * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)"
    8.61 -          by (cases "u x") (auto intro!: le_natfloor)
    8.62 +        then show "i * 2 ^ i * 2 \<le> nat(floor (real (u x) * 2 ^ Suc i))"
    8.63 +          by (cases "u x") (auto intro!: le_nat_floor)
    8.64        next
    8.65          assume "\<not> ereal (real i) \<le> u x" "ereal (real (Suc i)) \<le> u x"
    8.66 -        then show "natfloor (real (u x) * 2 ^ i) * 2 \<le> Suc i * 2 ^ Suc i"
    8.67 +        then show "nat(floor (real (u x) * 2 ^ i)) * 2 \<le> Suc i * 2 ^ Suc i"
    8.68            by (cases "u x") auto
    8.69        next
    8.70          assume "\<not> ereal (real i) \<le> u x" "\<not> ereal (real (Suc i)) \<le> u x"
    8.71 -        have "natfloor (real (u x) * 2 ^ i) * 2 = natfloor (real (u x) * 2 ^ i) * natfloor 2"
    8.72 +        have "nat(floor (real (u x) * 2 ^ i)) * 2 = nat(floor (real (u x) * 2 ^ i)) * nat(floor(2::real))"
    8.73            by simp
    8.74 -        also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
    8.75 +        also have "\<dots> \<le> nat(floor (real (u x) * 2 ^ i * 2))"
    8.76          proof cases
    8.77            assume "0 \<le> u x" then show ?thesis
    8.78 -            by (intro le_mult_natfloor) 
    8.79 +            by (intro le_mult_nat_floor) 
    8.80          next
    8.81            assume "\<not> 0 \<le> u x" then show ?thesis
    8.82 -            by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
    8.83 +            by (cases "u x") (auto simp: nat_floor_neg mult_nonpos_nonneg)
    8.84          qed
    8.85 -        also have "\<dots> = natfloor (real (u x) * 2 ^ Suc i)"
    8.86 +        also have "\<dots> = nat(floor (real (u x) * 2 ^ Suc i))"
    8.87            by (simp add: ac_simps)
    8.88 -        finally show "natfloor (real (u x) * 2 ^ i) * 2 \<le> natfloor (real (u x) * 2 ^ Suc i)" .
    8.89 +        finally show "nat(floor (real (u x) * 2 ^ i)) * 2 \<le> nat(floor (real (u x) * 2 ^ Suc i))" .
    8.90        qed simp
    8.91        then show "?g i x \<le> ?g (Suc i) x"
    8.92          by (auto simp: field_simps)
    8.93 @@ -288,8 +288,7 @@
    8.94      fix x show "(SUP i. ?g i x) = max 0 (u x)"
    8.95      proof (rule SUP_eqI)
    8.96        fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
    8.97 -        by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
    8.98 -                                     mult_nonpos_nonneg)
    8.99 +        by (cases "u x") (auto simp: field_simps nat_floor_neg mult_nonpos_nonneg)
   8.100      next
   8.101        fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
   8.102        have "\<And>i. 0 \<le> ?g i x" by auto
   8.103 @@ -309,11 +308,11 @@
   8.104            obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
   8.105            then have "r * 2^max N m < p * 2^max N m - 1" by simp
   8.106            moreover
   8.107 -          have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
   8.108 +          have "real (nat(floor (p * 2 ^ max N m))) \<le> r * 2 ^ max N m"
   8.109              using *[of "max N m"] m unfolding real_f using ux
   8.110              by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
   8.111            then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
   8.112 -            by (metis real_natfloor_gt_diff_one less_le_trans)
   8.113 +            by linarith
   8.114            ultimately show False by auto
   8.115          qed
   8.116          then show "max 0 (u x) \<le> y" using real ux by simp
     9.1 --- a/src/HOL/Real.thy	Tue Mar 03 19:08:04 2015 +0100
     9.2 +++ b/src/HOL/Real.thy	Wed Mar 04 23:31:04 2015 +0100
     9.3 @@ -1680,6 +1680,10 @@
     9.4    "numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
     9.5    using real_of_nat_less_iff[of "numeral w" n] by simp
     9.6  
     9.7 +lemma numeral_le_real_of_nat_iff[simp]:
     9.8 +  "(numeral n \<le> real(m::nat)) = (numeral n \<le> m)"
     9.9 +by (metis not_le real_of_nat_less_numeral_iff)
    9.10 +
    9.11  lemma numeral_le_real_of_int_iff [simp]:
    9.12       "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
    9.13  by (simp add: linorder_not_less [symmetric])
    9.14 @@ -1866,170 +1870,29 @@
    9.15    "\<lceil>- (numeral a / numeral b :: real)\<rceil> = - (numeral a div numeral b)"
    9.16    using ceiling_divide_eq_div[of "- numeral a" "numeral b"] by simp
    9.17  
    9.18 -subsubsection {* Versions for the natural numbers *}
    9.19 -
    9.20 -definition
    9.21 -  natfloor :: "real => nat" where
    9.22 -  "natfloor x = nat(floor x)"
    9.23 -
    9.24 -definition
    9.25 -  natceiling :: "real => nat" where
    9.26 -  "natceiling x = nat(ceiling x)"
    9.27 -
    9.28 -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)"
    9.29 -proof -
    9.30 -  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"
    9.31 -    by simp
    9.32 -  show ?thesis
    9.33 -    by (auto simp: natfloor_def real_of_nat_def[symmetric] split: split_nat floor_split)
    9.34 -qed
    9.35 +text{* The following lemmas are remnants of the erstwhile functions natfloor
    9.36 +and natceiling. *}
    9.37  
    9.38 -lemma natceiling_split[arith_split]:
    9.39 -  "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)"
    9.40 -proof -
    9.41 -  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"
    9.42 -    by simp
    9.43 -  show ?thesis
    9.44 -    by (auto simp: natceiling_def real_of_nat_def[symmetric] split: split_nat ceiling_split)
    9.45 -qed
    9.46 -
    9.47 -lemma natfloor_zero [simp]: "natfloor 0 = 0"
    9.48 -  by linarith
    9.49 -
    9.50 -lemma natfloor_one [simp]: "natfloor 1 = 1"
    9.51 -  by linarith
    9.52 -
    9.53 -lemma natfloor_numeral_eq [simp]: "natfloor (numeral n) = numeral n"
    9.54 -  by (unfold natfloor_def, simp)
    9.55 -
    9.56 -lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n"
    9.57 +lemma nat_floor_neg: "(x::real) <= 0 ==> nat(floor x) = 0"
    9.58    by linarith
    9.59  
    9.60 -lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x"
    9.61 -  by linarith
    9.62 -
    9.63 -lemma natfloor_neg: "x <= 0 ==> natfloor x = 0"
    9.64 -  by linarith
    9.65 -
    9.66 -lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y"
    9.67 -  by linarith
    9.68 -
    9.69 -lemma le_natfloor: "real x <= a ==> x <= natfloor a"
    9.70 -  by linarith
    9.71 -
    9.72 -lemma natfloor_less_iff: "0 \<le> x \<Longrightarrow> natfloor x < n \<longleftrightarrow> x < real n"
    9.73 -  by linarith
    9.74 -
    9.75 -lemma less_natfloor: "0 \<le> x \<Longrightarrow> x < real (n :: nat) \<Longrightarrow> natfloor x < n"
    9.76 -  by linarith
    9.77 -
    9.78 -lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)"
    9.79 -  by linarith
    9.80 -
    9.81 -lemma le_natfloor_eq_numeral [simp]:
    9.82 -    "0 \<le> x \<Longrightarrow> (numeral n \<le> natfloor x) = (numeral n \<le> x)"
    9.83 -  by (subst le_natfloor_eq, assumption) simp
    9.84 -
    9.85 -lemma le_natfloor_eq_one [simp]: "(1 \<le> natfloor x) = (1 \<le> x)"
    9.86 -  by linarith
    9.87 -
    9.88 -lemma natfloor_eq: "real n \<le> x \<Longrightarrow> x < real n + 1 \<Longrightarrow> natfloor x = n"
    9.89 -  by linarith
    9.90 -
    9.91 -lemma real_natfloor_add_one_gt: "x < real (natfloor x) + 1"
    9.92 -  by linarith
    9.93 -
    9.94 -lemma real_natfloor_gt_diff_one: "x - 1 < real(natfloor x)"
    9.95 -  by linarith
    9.96 -
    9.97 -lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n"
    9.98 -  by linarith
    9.99 -
   9.100 -lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a"
   9.101 +lemma le_nat_floor: "real x <= a ==> x <= nat(floor a)"
   9.102    by linarith
   9.103  
   9.104 -lemma natfloor_add_numeral [simp]:
   9.105 -    "0 <= x \<Longrightarrow> natfloor (x + numeral n) = natfloor x + numeral n"
   9.106 -  by (simp add: natfloor_add [symmetric])
   9.107 -
   9.108 -lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
   9.109 -  by linarith
   9.110 -
   9.111 -lemma natfloor_subtract [simp]:
   9.112 -    "natfloor(x - real a) = natfloor x - a"
   9.113 -  by linarith
   9.114 +lemma le_mult_nat_floor:
   9.115 +  shows "nat(floor a) * nat(floor b) \<le> nat(floor (a * b))"
   9.116 +  by (cases "0 <= a & 0 <= b")
   9.117 +     (auto simp add: nat_mult_distrib[symmetric] nat_mono le_mult_floor)
   9.118  
   9.119 -lemma natfloor_div_nat: "natfloor (x / real y) = natfloor x div y"
   9.120 -proof cases
   9.121 -  assume "0 \<le> x" then show ?thesis
   9.122 -    unfolding natfloor_def real_of_int_of_nat_eq[symmetric]
   9.123 -    by (subst floor_divide_real_eq_div) (simp_all add: nat_div_distrib)
   9.124 -qed (simp add: divide_nonpos_nonneg natfloor_neg)
   9.125 -
   9.126 -lemma natfloor_div_numeral[simp]:
   9.127 -  "natfloor (numeral x / numeral y) = numeral x div numeral y"
   9.128 -  using natfloor_div_nat[of "numeral x" "numeral y"] by simp
   9.129 -
   9.130 -lemma le_mult_natfloor:
   9.131 -  shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   9.132 -  by (cases "0 <= a & 0 <= b")
   9.133 -    (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg)
   9.134 -
   9.135 -lemma natceiling_zero [simp]: "natceiling 0 = 0"
   9.136 -  by linarith
   9.137 -
   9.138 -lemma natceiling_one [simp]: "natceiling 1 = 1"
   9.139 -  by linarith
   9.140 -
   9.141 -lemma zero_le_natceiling [simp]: "0 <= natceiling x"
   9.142 +lemma nat_ceiling_le_eq: "(nat(ceiling x) <= a) = (x <= real a)"
   9.143    by linarith
   9.144  
   9.145 -lemma natceiling_numeral_eq [simp]: "natceiling (numeral n) = numeral n"
   9.146 -  by (simp add: natceiling_def)
   9.147 -
   9.148 -lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n"
   9.149 -  by linarith
   9.150 -
   9.151 -lemma real_natceiling_ge: "x <= real(natceiling x)"
   9.152 -  by linarith
   9.153 -
   9.154 -lemma natceiling_neg: "x <= 0 ==> natceiling x = 0"
   9.155 -  by linarith
   9.156 -
   9.157 -lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y"
   9.158 -  by linarith
   9.159 -
   9.160 -lemma natceiling_le: "x <= real a ==> natceiling x <= a"
   9.161 -  by linarith
   9.162 -
   9.163 -lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
   9.164 +lemma real_nat_ceiling_ge: "x <= real(nat(ceiling x))"
   9.165    by linarith
   9.166  
   9.167 -lemma natceiling_le_eq_numeral [simp]:
   9.168 -    "(natceiling x <= numeral n) = (x <= numeral n)"
   9.169 -  by (simp add: natceiling_le_eq)
   9.170 -
   9.171 -lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
   9.172 -  by linarith
   9.173 -
   9.174 -lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
   9.175 -  by linarith
   9.176 -
   9.177 -lemma natceiling_add [simp]: "0 <= x ==> natceiling (x + real a) = natceiling x + a"
   9.178 -  by linarith
   9.179 -
   9.180 -lemma natceiling_add_numeral [simp]:
   9.181 -    "0 <= x ==> natceiling (x + numeral n) = natceiling x + numeral n"
   9.182 -  by (simp add: natceiling_add [symmetric])
   9.183 -
   9.184 -lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
   9.185 -  by linarith
   9.186 -
   9.187 -lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
   9.188 -  by linarith
   9.189  
   9.190  lemma Rats_no_top_le: "\<exists> q \<in> \<rat>. (x :: real) \<le> q"
   9.191 -  by (auto intro!: bexI[of _ "of_nat (natceiling x)"]) (metis real_natceiling_ge real_of_nat_def)
   9.192 +  by (auto intro!: bexI[of _ "of_nat (nat(ceiling x))"]) linarith
   9.193  
   9.194  lemma Rats_no_bot_less: "\<exists> q \<in> \<rat>. q < (x :: real)"
   9.195    apply (auto intro!: bexI[of _ "of_int (floor x - 1)"])
   9.196 @@ -2048,7 +1911,7 @@
   9.197    show ?thesis unfolding real_of_int_inject[symmetric]
   9.198      unfolding * floor_real_of_int ..
   9.199  qed
   9.200 -
   9.201 +(*
   9.202  lemma natfloor_power:
   9.203    assumes "x = real (natfloor x)"
   9.204    shows "natfloor (x ^ n) = natfloor x ^ n"
   9.205 @@ -2059,7 +1922,7 @@
   9.206    show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
   9.207      by simp
   9.208  qed
   9.209 -
   9.210 +*)
   9.211  lemma floor_numeral_power[simp]:
   9.212    "\<lfloor>numeral x ^ n\<rfloor> = numeral x ^ n"
   9.213    by (metis floor_of_int of_int_numeral of_int_power)
    10.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 03 19:08:04 2015 +0100
    10.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Mar 04 23:31:04 2015 +0100
    10.3 @@ -1521,9 +1521,8 @@
    10.4  lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
    10.5    unfolding filterlim_at_top
    10.6    apply (intro allI)
    10.7 -  apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
    10.8 -  apply (auto simp: natceiling_le_eq)
    10.9 -  done
   10.10 +  apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
   10.11 +  by linarith
   10.12  
   10.13  subsubsection {* Limits of Sequences *}
   10.14  
    11.1 --- a/src/HOL/Transcendental.thy	Tue Mar 03 19:08:04 2015 +0100
    11.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 04 23:31:04 2015 +0100
    11.3 @@ -2054,9 +2054,9 @@
    11.4    fixes i::real
    11.5    shows "b powr i =
    11.6      (if b \<le> 0 then Code.abort (STR ''op powr with nonpositive base'') (\<lambda>_. b powr i)
    11.7 -    else if floor i = i then (if 0 \<le> i then b ^ natfloor i else 1 / b ^ natfloor (- i))
    11.8 +    else if floor i = i then (if 0 \<le> i then b ^ nat(floor i) else 1 / b ^ nat(floor (- i)))
    11.9      else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
   11.10 -  by (auto simp: natfloor_def powr_int)
   11.11 +  by (auto simp: powr_int)
   11.12  
   11.13  lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
   11.14    using powr_realpow [of x 1] by simp