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
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:
haftmann@35028
     6
  fixes x y :: "'a:: {number_ring,division_by_zero,linordered_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"
haftmann@35066
    12
    by simp
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"
haftmann@35066
    16
    by (simp add: diff_divide_distrib)
paulson@32877
    17
  also have "... = (x + y) / 2" 
haftmann@35066
    18
    by simp
paulson@32877
    19
  also have "... < x" using xy 
haftmann@35066
    20
    by simp
paulson@32877
    21
  finally have "x<x" .
paulson@32877
    22
  thus False
haftmann@35066
    23
    by simp
paulson@32877
    24
qed
paulson@32877
    25
wenzelm@19640
    26
end