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
```