author  haftmann 
Fri, 05 Feb 2010 14:33:50 +0100  
changeset 35028  108662d50512 
parent 32877  6f09346c7c08 
child 35066  894e82be8d05 
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" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

12 
by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy) 
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" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

16 
by auto 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

17 
(metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

18 
diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls) 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

19 
also have "... = (x + y) / 2" 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

20 
by auto 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

21 
also have "... < x" using xy 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

22 
by auto 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

23 
finally have "x<x" . 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

24 
thus False 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

25 
by auto 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

26 
qed 
6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

27 

6f09346c7c08
New lemmas connected with the reals and infinite series
paulson
parents:
29197
diff
changeset

28 

19640
40ec89317425
added Ferrante and Rackoff Algorithm  by Amine Chaieb;
wenzelm
parents:
19023
diff
changeset

29 
end 