src/HOL/Real.thy
author paulson
Mon Oct 05 17:27:46 2009 +0100 (2009-10-05)
changeset 32877 6f09346c7c08
parent 29197 6d4cb27ed19c
child 35028 108662d50512
permissions -rw-r--r--
New lemmas connected with the reals and infinite series
haftmann@28952
     1
theory Real
haftmann@29197
     2
imports RComplete RealVector
haftmann@28952
     3
begin
wenzelm@19640
     4
paulson@32877
     5
lemma field_le_epsilon:
paulson@32877
     6
  fixes x y :: "'a:: {number_ring,division_by_zero,ordered_field}"
paulson@32877
     7
  assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
paulson@32877
     8
  shows "x \<le> y"
paulson@32877
     9
proof (rule ccontr)
paulson@32877
    10
  assume xy: "\<not> x \<le> y"
paulson@32877
    11
  hence "(x-y)/2 > 0"
paulson@32877
    12
    by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
paulson@32877
    13
  hence "x \<le> y + (x - y) / 2"
paulson@32877
    14
    by (rule e [of "(x-y)/2"])
paulson@32877
    15
  also have "... = (x - y + 2*y)/2"
paulson@32877
    16
    by auto
paulson@32877
    17
       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
paulson@32877
    18
           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
paulson@32877
    19
  also have "... = (x + y) / 2" 
paulson@32877
    20
    by auto
paulson@32877
    21
  also have "... < x" using xy 
paulson@32877
    22
    by auto
paulson@32877
    23
  finally have "x<x" .
paulson@32877
    24
  thus False
paulson@32877
    25
    by auto 
paulson@32877
    26
qed
paulson@32877
    27
paulson@32877
    28
wenzelm@19640
    29
end