src/HOL/NthRoot.thy
changeset 59741 5b762cd73a8e
parent 58889 5b7a9633cfa8
child 60141 833adf7db7d8
     1.1 --- a/src/HOL/NthRoot.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -626,19 +626,24 @@
     1.4  apply (simp add: zero_less_divide_iff)
     1.5  done
     1.6  
     1.7 +lemma sqrt2_less_2: "sqrt 2 < (2::real)"
     1.8 +  by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
     1.9 +
    1.10 +
    1.11  text{*Needed for the infinitely close relation over the nonstandard
    1.12      complex numbers*}
    1.13  lemma lemma_sqrt_hcomplex_capprox:
    1.14       "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
    1.15 -apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
    1.16 -apply (erule_tac [2] lemma_real_divide_sqrt_less)
    1.17 -apply (rule power2_le_imp_le)
    1.18 -apply (auto simp add: zero_le_divide_iff power_divide)
    1.19 -apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
    1.20 -apply (rule add_mono)
    1.21 -apply (auto simp add: four_x_squared intro: power_mono)
    1.22 -done
    1.23 -
    1.24 +  apply (rule real_sqrt_sum_squares_less)
    1.25 +  apply (auto simp add: abs_if field_simps)
    1.26 +  apply (rule le_less_trans [where y = "x*2"])
    1.27 +  using less_eq_real_def sqrt2_less_2 apply force
    1.28 +  apply assumption
    1.29 +  apply (rule le_less_trans [where y = "y*2"])
    1.30 +  using less_eq_real_def sqrt2_less_2 mult_le_cancel_left 
    1.31 +  apply auto 
    1.32 +  done
    1.33 +  
    1.34  text "Legacy theorem names:"
    1.35  lemmas real_root_pos2 = real_root_power_cancel
    1.36  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]