diff -r 6b76a5d1b7a5 -r deabce3ccf1f src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Sun Oct 08 16:50:37 2017 +0200 +++ b/src/HOL/Archimedean_Field.thy Mon Oct 09 15:34:23 2017 +0100 @@ -526,7 +526,8 @@ shows "finite {k \ \. \k\ \ a}" using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff) -text \Ceiling with numerals.\ + +subsubsection \Ceiling with numerals.\ lemma ceiling_zero [simp]: "\0\ = 0" using ceiling_of_int [of 0] by simp @@ -595,7 +596,7 @@ by (simp add: ceiling_altdef) -text \Addition and subtraction of integers.\ +subsubsection \Addition and subtraction of integers.\ lemma ceiling_add_of_int [simp]: "\x + of_int z\ = \x\ + z" using ceiling_correct [of x] by (simp add: ceiling_def) @@ -630,6 +631,24 @@ unfolding of_int_less_iff by simp qed +lemma nat_approx_posE: + fixes e:: "'a::{archimedean_field,floor_ceiling}" + assumes "0 < e" + obtains n :: nat where "1 / of_nat(Suc n) < e" +proof + have "(1::'a) / of_nat (Suc (nat \1/e\)) < 1 / of_int (\1/e\)" + proof (rule divide_strict_left_mono) + show "(of_int \1 / e\::'a) < of_nat (Suc (nat \1 / e\))" + using assms by (simp add: field_simps) + show "(0::'a) < of_nat (Suc (nat \1 / e\)) * of_int \1 / e\" + using assms by (auto simp: zero_less_mult_iff pos_add_strict) + qed auto + also have "1 / of_int (\1/e\) \ 1 / (1/e)" + by (rule divide_left_mono) (auto simp: \0 < e\ ceiling_correct) + also have "\ = e" by simp + finally show "1 / of_nat (Suc (nat \1 / e\)) < e" + by metis +qed subsection \Negation\