src/HOL/Fields.thy
 changeset 35579 cc9a5a0ab5ea parent 35216 7641e8d831d2 child 35828 46cfc4b8112e
```     1.1 --- a/src/HOL/Fields.thy	Thu Mar 04 17:28:45 2010 +0100
1.2 +++ b/src/HOL/Fields.thy	Thu Mar 04 18:42:39 2010 +0100
1.3 @@ -1034,30 +1034,33 @@
1.5  done
1.6
1.7 -
1.8  lemma field_le_epsilon:
1.9 -  fixes x y :: "'a :: {division_by_zero,linordered_field}"
1.10 +  fixes x y :: "'a\<Colon>linordered_field"
1.11    assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
1.12    shows "x \<le> y"
1.13 -proof (rule ccontr)
1.14 -  obtain two :: 'a where two: "two = 1 + 1" by simp
1.15 -  assume "\<not> x \<le> y"
1.16 -  then have yx: "y < x" by simp
1.17 -  then have "y + - y < x + - y" by (rule add_strict_right_mono)
1.18 -  then have "x - y > 0" by (simp add: diff_minus)
1.19 -  then have "(x - y) / two > 0"
1.20 -    by (rule divide_pos_pos) (simp add: two)
1.21 -  then have "x \<le> y + (x - y) / two" by (rule e)
1.22 -  also have "... = (x - y + two * y) / two"
1.24 -  also have "... = (x + y) / two"
1.25 -    by (simp add: two algebra_simps)
1.26 -  also have "... < x" using yx
1.27 -    by (simp add: two pos_divide_less_eq algebra_simps)
1.28 -  finally have "x < x" .
1.29 -  then show False ..
1.30 +proof (rule dense_le)
1.31 +  fix t assume "t < x"
1.32 +  hence "0 < x - t" by (simp add: less_diff_eq)
1.33 +  from e[OF this]
1.34 +  show "t \<le> y" by (simp add: field_simps)
1.35  qed
1.36
1.37 +lemma field_le_mult_one_interval:
1.38 +  fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
1.39 +  assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
1.40 +  shows "x \<le> y"
1.41 +proof (cases "0 < x")
1.42 +  assume "0 < x"
1.43 +  thus ?thesis
1.44 +    using dense_le_bounded[of 0 1 "y/x"] *
1.45 +    unfolding le_divide_eq if_P[OF `0 < x`] by simp
1.46 +next
1.47 +  assume "\<not>0 < x" hence "x \<le> 0" by simp
1.48 +  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
1.49 +  hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
1.50 +  also note *[OF s]
1.51 +  finally show ?thesis .
1.52 +qed
1.53
1.54  code_modulename SML
1.55    Fields Arith
```