simple proofs make life faster and easier
authorhaftmann
Tue Feb 09 16:07:09 2010 +0100 (2010-02-09)
changeset 35066894e82be8d05
parent 35065 698f0bfb560e
child 35067 af4c18c30593
child 35080 342888d802d8
child 35082 96a21dd3b349
simple proofs make life faster and easier
src/HOL/Real.thy
     1.1 --- a/src/HOL/Real.thy	Tue Feb 09 14:32:16 2010 +0100
     1.2 +++ b/src/HOL/Real.thy	Tue Feb 09 16:07:09 2010 +0100
     1.3 @@ -9,21 +9,18 @@
     1.4  proof (rule ccontr)
     1.5    assume xy: "\<not> x \<le> y"
     1.6    hence "(x-y)/2 > 0"
     1.7 -    by (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
     1.8 +    by simp
     1.9    hence "x \<le> y + (x - y) / 2"
    1.10      by (rule e [of "(x-y)/2"])
    1.11    also have "... = (x - y + 2*y)/2"
    1.12 -    by auto
    1.13 -       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
    1.14 -           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
    1.15 +    by (simp add: diff_divide_distrib)
    1.16    also have "... = (x + y) / 2" 
    1.17 -    by auto
    1.18 +    by simp
    1.19    also have "... < x" using xy 
    1.20 -    by auto
    1.21 +    by simp
    1.22    finally have "x<x" .
    1.23    thus False
    1.24 -    by auto 
    1.25 +    by simp
    1.26  qed
    1.27  
    1.28 -
    1.29  end