# HG changeset patch
# User hoelzl
# Date 1267724559 -3600
# Node ID cc9a5a0ab5eaa53dc8e7f7c37ea5aa04685b499a
# Parent  384ad08a1d1b285da60d5111c2a2374b8728f47c
Add dense_le, dense_le_bounded, field_le_mult_one_interval.

diff -r 384ad08a1d1b -r cc9a5a0ab5ea src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Mar 04 17:28:45 2010 +0100
+++ b/src/HOL/Fields.thy	Thu Mar 04 18:42:39 2010 +0100
@@ -1034,30 +1034,33 @@
   apply (simp add: order_less_imp_le)
 done
 
-
 lemma field_le_epsilon:
-  fixes x y :: "'a :: {division_by_zero,linordered_field}"
+  fixes x y :: "'a\<Colon>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"
-    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 ..
+proof (rule dense_le)
+  fix t assume "t < x"
+  hence "0 < x - t" by (simp add: less_diff_eq)
+  from e[OF this]
+  show "t \<le> y" by (simp add: field_simps)
 qed
 
+lemma field_le_mult_one_interval:
+  fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
+  assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
+  shows "x \<le> y"
+proof (cases "0 < x")
+  assume "0 < x"
+  thus ?thesis
+    using dense_le_bounded[of 0 1 "y/x"] *
+    unfolding le_divide_eq if_P[OF `0 < x`] by simp
+next
+  assume "\<not>0 < x" hence "x \<le> 0" by simp
+  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
+  hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
+  also note *[OF s]
+  finally show ?thesis .
+qed
 
 code_modulename SML
   Fields Arith
diff -r 384ad08a1d1b -r cc9a5a0ab5ea src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Mar 04 17:28:45 2010 +0100
+++ b/src/HOL/Orderings.thy	Thu Mar 04 18:42:39 2010 +0100
@@ -1097,7 +1097,43 @@
   assumes gt_ex: "\<exists>y. x < y" 
   and lt_ex: "\<exists>y. y < x"
   and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
+begin
 
+lemma dense_le:
+  fixes y z :: 'a
+  assumes "\<And>x. x < y \<Longrightarrow> x \<le> z"
+  shows "y \<le> z"
+proof (rule ccontr)
+  assume "\<not> ?thesis"
+  hence "z < y" by simp
+  from dense[OF this]
+  obtain x where "x < y" and "z < x" by safe
+  moreover have "x \<le> z" using assms[OF `x < y`] .
+  ultimately show False by auto
+qed
+
+lemma dense_le_bounded:
+  fixes x y z :: 'a
+  assumes "x < y"
+  assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
+  shows "y \<le> z"
+proof (rule dense_le)
+  fix w assume "w < y"
+  from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe
+  from linear[of u w]
+  show "w \<le> z"
+  proof (rule disjE)
+    assume "u \<le> w"
+    from less_le_trans[OF `x < u` `u \<le> w`] `w < y`
+    show "w \<le> z" by (rule *)
+  next
+    assume "w \<le> u"
+    from `w \<le> u` *[OF `x < u` `u < y`]
+    show "w \<le> z" by (rule order_trans)
+  qed
+qed
+
+end
 
 subsection {* Wellorders *}