src/HOL/Real.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 32877 6f09346c7c08
child 35028 108662d50512
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
     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,ordered_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 (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
    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 auto
    17        (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
    18            diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
    19   also have "... = (x + y) / 2" 
    20     by auto
    21   also have "... < x" using xy 
    22     by auto
    23   finally have "x<x" .
    24   thus False
    25     by auto 
    26 qed
    27 
    28 
    29 end