src/HOL/Archimedean_Field.thy
 changeset 66793 deabce3ccf1f parent 66515 85c505c98332 child 68499 d4312962161a
```     1.1 --- a/src/HOL/Archimedean_Field.thy	Sun Oct 08 16:50:37 2017 +0200
1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Oct 09 15:34:23 2017 +0100
1.3 @@ -526,7 +526,8 @@
1.4    shows "finite {k \<in> \<int>. \<bar>k\<bar> \<le> a}"
1.5    using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff)
1.6
1.7 -text \<open>Ceiling with numerals.\<close>
1.8 +
1.9 +subsubsection \<open>Ceiling with numerals.\<close>
1.10
1.11  lemma ceiling_zero [simp]: "\<lceil>0\<rceil> = 0"
1.12    using ceiling_of_int [of 0] by simp
1.13 @@ -595,7 +596,7 @@
1.15
1.16
1.17 -text \<open>Addition and subtraction of integers.\<close>
1.18 +subsubsection \<open>Addition and subtraction of integers.\<close>
1.19
1.20  lemma ceiling_add_of_int [simp]: "\<lceil>x + of_int z\<rceil> = \<lceil>x\<rceil> + z"
1.21    using ceiling_correct [of x] by (simp add: ceiling_def)
1.22 @@ -630,6 +631,24 @@
1.23      unfolding of_int_less_iff by simp
1.24  qed
1.25
1.26 +lemma nat_approx_posE:
1.27 +  fixes e:: "'a::{archimedean_field,floor_ceiling}"
1.28 +  assumes "0 < e"
1.29 +  obtains n :: nat where "1 / of_nat(Suc n) < e"
1.30 +proof
1.31 +  have "(1::'a) / of_nat (Suc (nat \<lceil>1/e\<rceil>)) < 1 / of_int (\<lceil>1/e\<rceil>)"
1.32 +  proof (rule divide_strict_left_mono)
1.33 +    show "(of_int \<lceil>1 / e\<rceil>::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>))"
1.34 +      using assms by (simp add: field_simps)
1.35 +    show "(0::'a) < of_nat (Suc (nat \<lceil>1 / e\<rceil>)) * of_int \<lceil>1 / e\<rceil>"
1.36 +      using assms by (auto simp: zero_less_mult_iff pos_add_strict)
1.37 +  qed auto
1.38 +  also have "1 / of_int (\<lceil>1/e\<rceil>) \<le> 1 / (1/e)"
1.39 +    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
1.40 +  also have "\<dots> = e" by simp
1.41 +  finally show  "1 / of_nat (Suc (nat \<lceil>1 / e\<rceil>)) < e"
1.42 +    by metis
1.43 +qed
1.44
1.45  subsection \<open>Negation\<close>
1.46
```