equal
deleted
inserted
replaced
7 assumes e: "(!!e. 0 < e ==> x \<le> y + e)" |
7 assumes e: "(!!e. 0 < e ==> x \<le> y + e)" |
8 shows "x \<le> y" |
8 shows "x \<le> y" |
9 proof (rule ccontr) |
9 proof (rule ccontr) |
10 assume xy: "\<not> x \<le> y" |
10 assume xy: "\<not> x \<le> y" |
11 hence "(x-y)/2 > 0" |
11 hence "(x-y)/2 > 0" |
12 by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy) |
12 by simp |
13 hence "x \<le> y + (x - y) / 2" |
13 hence "x \<le> y + (x - y) / 2" |
14 by (rule e [of "(x-y)/2"]) |
14 by (rule e [of "(x-y)/2"]) |
15 also have "... = (x - y + 2*y)/2" |
15 also have "... = (x - y + 2*y)/2" |
16 by auto |
16 by (simp add: diff_divide_distrib) |
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" |
17 also have "... = (x + y) / 2" |
20 by auto |
18 by simp |
21 also have "... < x" using xy |
19 also have "... < x" using xy |
22 by auto |
20 by simp |
23 finally have "x<x" . |
21 finally have "x<x" . |
24 thus False |
22 thus False |
25 by auto |
23 by simp |
26 qed |
24 qed |
27 |
25 |
28 |
|
29 end |
26 end |