author | haftmann |
Tue, 09 Feb 2010 16:07:09 +0100 | |
changeset 35066 | 894e82be8d05 |
parent 35028 | 108662d50512 |
child 35090 | 88cc65ae046e |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
27964
diff
changeset
|
1 |
theory Real |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29108
diff
changeset
|
2 |
imports RComplete RealVector |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
27964
diff
changeset
|
3 |
begin |
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
4 |
|
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
5 |
lemma field_le_epsilon: |
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
32877
diff
changeset
|
6 |
fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}" |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
7 |
assumes e: "(!!e. 0 < e ==> x \<le> y + e)" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
8 |
shows "x \<le> y" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
9 |
proof (rule ccontr) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
10 |
assume xy: "\<not> x \<le> y" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
11 |
hence "(x-y)/2 > 0" |
35066 | 12 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
13 |
hence "x \<le> y + (x - y) / 2" |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
14 |
by (rule e [of "(x-y)/2"]) |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
15 |
also have "... = (x - y + 2*y)/2" |
35066 | 16 |
by (simp add: diff_divide_distrib) |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
17 |
also have "... = (x + y) / 2" |
35066 | 18 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
19 |
also have "... < x" using xy |
35066 | 20 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
21 |
finally have "x<x" . |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
22 |
thus False |
35066 | 23 |
by simp |
32877
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
24 |
qed |
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset
|
25 |
|
19640
40ec89317425
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset
|
26 |
end |