src/HOL/Fields.thy
changeset 35090 88cc65ae046e
parent 35084 e25eedfc15ce
child 35216 7641e8d831d2
equal deleted 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