# 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