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,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 |
5 end |