# HG changeset patch # User haftmann # Date 1265807522 -3600 # Node ID 88cc65ae046e347fec3cae137b06283af7fb32bb # Parent 92a8c9ea5aa7c961053e586caaadc5e64647c4c7 moved lemma field_le_epsilon from Real.thy to Fields.thy diff -r 92a8c9ea5aa7 -r 88cc65ae046e src/HOL/Fields.thy --- a/src/HOL/Fields.thy Wed Feb 10 08:54:56 2010 +0100 +++ b/src/HOL/Fields.thy Wed Feb 10 14:12:02 2010 +0100 @@ -1035,6 +1035,31 @@ apply (simp add: order_less_imp_le) done + +lemma field_le_epsilon: + fixes x y :: "'a :: {division_by_zero,linordered_field}" + assumes e: "\e. 0 < e \ x \ y + e" + shows "x \ y" +proof (rule ccontr) + obtain two :: 'a where two: "two = 1 + 1" by simp + assume "\ x \ y" + then have yx: "y < x" by simp + then have "y + - y < x + - y" by (rule add_strict_right_mono) + then have "x - y > 0" by (simp add: diff_minus) + then have "(x - y) / two > 0" + by (rule divide_pos_pos) (simp add: two) + then have "x \ y + (x - y) / two" by (rule e) + also have "... = (x - y + two * y) / two" + by (simp add: add_divide_distrib two) + also have "... = (x + y) / two" + by (simp add: two algebra_simps) + also have "... < x" using yx + by (simp add: two pos_divide_less_eq algebra_simps) + finally have "x < x" . + then show False .. +qed + + code_modulename SML Fields Arith diff -r 92a8c9ea5aa7 -r 88cc65ae046e src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Feb 10 08:54:56 2010 +0100 +++ b/src/HOL/Real.thy Wed Feb 10 14:12:02 2010 +0100 @@ -2,25 +2,4 @@ imports RComplete RealVector begin -lemma field_le_epsilon: - fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}" - assumes e: "(!!e. 0 < e ==> x \ y + e)" - shows "x \ y" -proof (rule ccontr) - assume xy: "\ x \ y" - hence "(x-y)/2 > 0" - by simp - hence "x \ y + (x - y) / 2" - by (rule e [of "(x-y)/2"]) - also have "... = (x - y + 2*y)/2" - by (simp add: diff_divide_distrib) - also have "... = (x + y) / 2" - by simp - also have "... < x" using xy - by simp - finally have "x