author haftmann Wed, 10 Feb 2010 14:12:02 +0100 changeset 35090 88cc65ae046e parent 35086 92a8c9ea5aa7 child 35091 59b41ba431b5
moved lemma field_le_epsilon from Real.thy to Fields.thy
 src/HOL/Fields.thy file | annotate | diff | comparison | revisions src/HOL/Real.thy file | annotate | diff | comparison | revisions
```--- 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 @@
done

+
+lemma field_le_epsilon:
+  fixes x y :: "'a :: {division_by_zero,linordered_field}"
+  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
+  shows "x \<le> y"
+proof (rule ccontr)
+  obtain two :: 'a where two: "two = 1 + 1" by simp
+  assume "\<not> x \<le> 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 \<le> y + (x - y) / two" by (rule e)
+  also have "... = (x - y + two * y) / 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
```
```--- 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 \<le> y + e)"
-  shows "x \<le> y"
-proof (rule ccontr)
-  assume xy: "\<not> x \<le> y"
-  hence "(x-y)/2 > 0"
-    by simp
-  hence "x \<le> y + (x - y) / 2"
-    by (rule e [of "(x-y)/2"])
-  also have "... = (x - y + 2*y)/2"