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