moved lemma field_le_epsilon from Real.thy to Fields.thy
authorhaftmann
Wed Feb 10 14:12:02 2010 +0100 (2010-02-10)
changeset 3509088cc65ae046e
parent 35086 92a8c9ea5aa7
child 35091 59b41ba431b5
moved lemma field_le_epsilon from Real.thy to Fields.thy
src/HOL/Fields.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Fields.thy	Wed Feb 10 08:54:56 2010 +0100
     1.2 +++ b/src/HOL/Fields.thy	Wed Feb 10 14:12:02 2010 +0100
     1.3 @@ -1035,6 +1035,31 @@
     1.4    apply (simp add: order_less_imp_le)
     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 +  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
    1.11 +  shows "x \<le> y"
    1.12 +proof (rule ccontr)
    1.13 +  obtain two :: 'a where two: "two = 1 + 1" by simp
    1.14 +  assume "\<not> x \<le> y"
    1.15 +  then have yx: "y < x" by simp
    1.16 +  then have "y + - y < x + - y" by (rule add_strict_right_mono)
    1.17 +  then have "x - y > 0" by (simp add: diff_minus)
    1.18 +  then have "(x - y) / two > 0"
    1.19 +    by (rule divide_pos_pos) (simp add: two)
    1.20 +  then have "x \<le> y + (x - y) / two" by (rule e)
    1.21 +  also have "... = (x - y + two * y) / two"
    1.22 +    by (simp add: add_divide_distrib two)
    1.23 +  also have "... = (x + y) / two" 
    1.24 +    by (simp add: two algebra_simps)
    1.25 +  also have "... < x" using yx
    1.26 +    by (simp add: two pos_divide_less_eq algebra_simps)
    1.27 +  finally have "x < x" .
    1.28 +  then show False ..
    1.29 +qed
    1.30 +
    1.31 +
    1.32  code_modulename SML
    1.33    Fields Arith
    1.34  
     2.1 --- a/src/HOL/Real.thy	Wed Feb 10 08:54:56 2010 +0100
     2.2 +++ b/src/HOL/Real.thy	Wed Feb 10 14:12:02 2010 +0100
     2.3 @@ -2,25 +2,4 @@
     2.4  imports RComplete RealVector
     2.5  begin
     2.6  
     2.7 -lemma field_le_epsilon:
     2.8 -  fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
     2.9 -  assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
    2.10 -  shows "x \<le> y"
    2.11 -proof (rule ccontr)
    2.12 -  assume xy: "\<not> x \<le> y"
    2.13 -  hence "(x-y)/2 > 0"
    2.14 -    by simp
    2.15 -  hence "x \<le> y + (x - y) / 2"
    2.16 -    by (rule e [of "(x-y)/2"])
    2.17 -  also have "... = (x - y + 2*y)/2"
    2.18 -    by (simp add: diff_divide_distrib)
    2.19 -  also have "... = (x + y) / 2" 
    2.20 -    by simp
    2.21 -  also have "... < x" using xy 
    2.22 -    by simp
    2.23 -  finally have "x<x" .
    2.24 -  thus False
    2.25 -    by simp
    2.26 -qed
    2.27 -
    2.28  end