equal
deleted
inserted
replaced
1 theory Real |
1 theory Real |
2 imports RComplete RealVector |
2 imports RComplete RealVector |
3 begin |
3 begin |
4 |
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 |
5 end |
29 end |