equal
deleted
inserted
replaced
1033 abs x / y = abs (x / y)" |
1033 abs x / y = abs (x / y)" |
1034 apply (subst abs_divide) |
1034 apply (subst abs_divide) |
1035 apply (simp add: order_less_imp_le) |
1035 apply (simp add: order_less_imp_le) |
1036 done |
1036 done |
1037 |
1037 |
|
1038 |
|
1039 lemma field_le_epsilon: |
|
1040 fixes x y :: "'a :: {division_by_zero,linordered_field}" |
|
1041 assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e" |
|
1042 shows "x \<le> y" |
|
1043 proof (rule ccontr) |
|
1044 obtain two :: 'a where two: "two = 1 + 1" by simp |
|
1045 assume "\<not> x \<le> y" |
|
1046 then have yx: "y < x" by simp |
|
1047 then have "y + - y < x + - y" by (rule add_strict_right_mono) |
|
1048 then have "x - y > 0" by (simp add: diff_minus) |
|
1049 then have "(x - y) / two > 0" |
|
1050 by (rule divide_pos_pos) (simp add: two) |
|
1051 then have "x \<le> y + (x - y) / two" by (rule e) |
|
1052 also have "... = (x - y + two * y) / two" |
|
1053 by (simp add: add_divide_distrib two) |
|
1054 also have "... = (x + y) / two" |
|
1055 by (simp add: two algebra_simps) |
|
1056 also have "... < x" using yx |
|
1057 by (simp add: two pos_divide_less_eq algebra_simps) |
|
1058 finally have "x < x" . |
|
1059 then show False .. |
|
1060 qed |
|
1061 |
|
1062 |
1038 code_modulename SML |
1063 code_modulename SML |
1039 Fields Arith |
1064 Fields Arith |
1040 |
1065 |
1041 code_modulename OCaml |
1066 code_modulename OCaml |
1042 Fields Arith |
1067 Fields Arith |