src/HOL/Real.thy
author haftmann
Tue Feb 09 16:07:09 2010 +0100 (2010-02-09)
changeset 35066 894e82be8d05
parent 35028 108662d50512
child 35090 88cc65ae046e
permissions -rw-r--r--
simple proofs make life faster and easier
     1 theory Real
     2 imports RComplete RealVector
     3 begin
     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