src/HOL/Real.thy
changeset 35090 88cc65ae046e
parent 35066 894e82be8d05
child 36899 bcd6fce5bf06
equal deleted inserted replaced
35086:92a8c9ea5aa7 35090:88cc65ae046e
     1 theory Real
     1 theory Real
     2 imports RComplete RealVector
     2 imports RComplete RealVector
     3 begin
     3 begin
     4 
     4 
     5 lemma field_le_epsilon:
       
     6   fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
       
     7   assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
       
     8   shows "x \<le> y"
       
     9 proof (rule ccontr)
       
    10   assume xy: "\<not> x \<le> y"
       
    11   hence "(x-y)/2 > 0"
       
    12     by simp
       
    13   hence "x \<le> y + (x - y) / 2"
       
    14     by (rule e [of "(x-y)/2"])
       
    15   also have "... = (x - y + 2*y)/2"
       
    16     by (simp add: diff_divide_distrib)
       
    17   also have "... = (x + y) / 2" 
       
    18     by simp
       
    19   also have "... < x" using xy 
       
    20     by simp
       
    21   finally have "x<x" .
       
    22   thus False
       
    23     by simp
       
    24 qed
       
    25 
       
    26 end
     5 end