1032 abs x / y = abs (x / y)" |
1032 abs x / y = abs (x / y)" |
1033 apply (subst abs_divide) |
1033 apply (subst abs_divide) |
1034 apply (simp add: order_less_imp_le) |
1034 apply (simp add: order_less_imp_le) |
1035 done |
1035 done |
1036 |
1036 |
1037 |
|
1038 lemma field_le_epsilon: |
1037 lemma field_le_epsilon: |
1039 fixes x y :: "'a :: {division_by_zero,linordered_field}" |
1038 fixes x y :: "'a\<Colon>linordered_field" |
1040 assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e" |
1039 assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e" |
1041 shows "x \<le> y" |
1040 shows "x \<le> y" |
1042 proof (rule ccontr) |
1041 proof (rule dense_le) |
1043 obtain two :: 'a where two: "two = 1 + 1" by simp |
1042 fix t assume "t < x" |
1044 assume "\<not> x \<le> y" |
1043 hence "0 < x - t" by (simp add: less_diff_eq) |
1045 then have yx: "y < x" by simp |
1044 from e[OF this] |
1046 then have "y + - y < x + - y" by (rule add_strict_right_mono) |
1045 show "t \<le> y" by (simp add: field_simps) |
1047 then have "x - y > 0" by (simp add: diff_minus) |
1046 qed |
1048 then have "(x - y) / two > 0" |
1047 |
1049 by (rule divide_pos_pos) (simp add: two) |
1048 lemma field_le_mult_one_interval: |
1050 then have "x \<le> y + (x - y) / two" by (rule e) |
1049 fixes x :: "'a\<Colon>{linordered_field,division_by_zero}" |
1051 also have "... = (x - y + two * y) / two" |
1050 assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y" |
1052 by (simp add: add_divide_distrib two) |
1051 shows "x \<le> y" |
1053 also have "... = (x + y) / two" |
1052 proof (cases "0 < x") |
1054 by (simp add: two algebra_simps) |
1053 assume "0 < x" |
1055 also have "... < x" using yx |
1054 thus ?thesis |
1056 by (simp add: two pos_divide_less_eq algebra_simps) |
1055 using dense_le_bounded[of 0 1 "y/x"] * |
1057 finally have "x < x" . |
1056 unfolding le_divide_eq if_P[OF `0 < x`] by simp |
1058 then show False .. |
1057 next |
1059 qed |
1058 assume "\<not>0 < x" hence "x \<le> 0" by simp |
1060 |
1059 obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto |
|
1060 hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto |
|
1061 also note *[OF s] |
|
1062 finally show ?thesis . |
|
1063 qed |
1061 |
1064 |
1062 code_modulename SML |
1065 code_modulename SML |
1063 Fields Arith |
1066 Fields Arith |
1064 |
1067 |
1065 code_modulename OCaml |
1068 code_modulename OCaml |