src/HOL/Fields.thy
 changeset 35090 88cc65ae046e parent 35084 e25eedfc15ce child 35216 7641e8d831d2
equal inserted replaced
35086:92a8c9ea5aa7 35090:88cc65ae046e
`  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`