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.14    by (simp add: ceiling_altdef)
    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