author  haftmann 
Tue, 09 Feb 2010 16:07:09 +0100  
changeset 35066  894e82be8d05 
parent 35028  108662d50512 
child 35090  88cc65ae046e 
permissions  rwrr 
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 "(xy)/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 "(xy)/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 