1.1 --- a/src/HOL/NthRoot.thy	Tue Nov 12 19:28:53 2013 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Tue Nov 12 19:28:54 2013 +0100
     1.3 @@ -410,6 +410,27 @@
     1.4  lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
     1.5  unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
     1.6  
     1.7 +lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
     1.8 +  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
     1.9 +
    1.10 +lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
    1.11 +  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
    1.12 +
    1.13 +lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
    1.14 +  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
    1.15 +
    1.16 +lemma sqrt_even_pow2:
    1.17 +  assumes n: "even n"
    1.18 +  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
    1.19 +proof -
    1.20 +  from n obtain m where m: "n = 2 * m"
    1.21 +    unfolding even_mult_two_ex ..
    1.22 +  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    1.23 +    by (simp only: power_mult[symmetric] mult_commute)
    1.24 +  then show ?thesis
    1.25 +    using m by simp
    1.26 +qed
    1.27 +
    1.28  lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
    1.29  lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
    1.30  lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
    1.31 @@ -490,6 +511,13 @@
    1.32    qed
    1.33  qed
    1.34  
    1.35 +lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
    1.36 +  apply (cases "x = 0")
    1.37 +  apply simp_all
    1.38 +  using sqrt_divide_self_eq[of x]
    1.39 +  apply (simp add: inverse_eq_divide field_simps)
    1.40 +  done
    1.41 +
    1.42  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
    1.43  apply (simp add: divide_inverse)
    1.44  apply (case_tac "r=0")