--- a/src/HOL/NthRoot.thy Tue Nov 12 19:28:53 2013 +0100
+++ b/src/HOL/NthRoot.thy Tue Nov 12 19:28:54 2013 +0100
@@ -410,6 +410,27 @@
lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
+lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
+ using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
+
+lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
+ using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
+
+lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
+ using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
+
+lemma sqrt_even_pow2:
+ assumes n: "even n"
+ shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
+proof -
+ from n obtain m where m: "n = 2 * m"
+ unfolding even_mult_two_ex ..
+ from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
+ by (simp only: power_mult[symmetric] mult_commute)
+ then show ?thesis
+ using m by simp
+qed
+
lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
@@ -490,6 +511,13 @@
qed
qed
+lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
+ apply (cases "x = 0")
+ apply simp_all
+ using sqrt_divide_self_eq[of x]
+ apply (simp add: inverse_eq_divide field_simps)
+ done
+
lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
apply (simp add: divide_inverse)
apply (case_tac "r=0")