--- a/src/HOL/Hyperreal/NthRoot.thy Sun May 20 09:50:56 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy Sun May 20 10:13:06 2007 +0200
@@ -429,6 +429,15 @@
lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
by simp
+lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
+by simp
+
+lemma real_sqrt_two_ge_zero [simp]: "0 \<le> sqrt 2"
+by simp
+
+lemma real_sqrt_two_gt_one [simp]: "1 < sqrt 2"
+by simp
+
lemma sqrt_divide_self_eq:
assumes nneg: "0 \<le> x"
shows "sqrt x / x = inverse (sqrt x)"
@@ -452,6 +461,14 @@
apply (auto simp add: mult_ac)
done
+lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
+by (simp add: divide_less_eq mult_compare_simps)
+
+lemma four_x_squared:
+ fixes x::real
+ shows "4 * x\<twosuperior> = (2 * x)\<twosuperior>"
+by (simp add: power2_eq_square)
+
subsection {* Square Root of Sum of Squares *}
lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
@@ -460,6 +477,8 @@
lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
by simp
+declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
+
lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
"0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
@@ -468,12 +487,27 @@
"sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
by (auto simp add: zero_le_mult_iff)
-lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
+lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<twosuperior> + y\<twosuperior>) = x \<Longrightarrow> y = 0"
+by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
+
+lemma real_sqrt_sum_squares_eq_cancel2: "sqrt (x\<twosuperior> + y\<twosuperior>) = y \<Longrightarrow> x = 0"
+by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
+
+lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
by (rule power2_le_imp_le, simp_all)
-lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
+lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
+by (rule power2_le_imp_le, simp_all)
+
+lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
by (rule power2_le_imp_le, simp_all)
+lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
+by (rule power2_le_imp_le, simp_all)
+
+lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
+by (simp add: power2_eq_square [symmetric])
+
lemma power2_sum:
fixes x y :: "'a::{number_ring,recpower}"
shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
@@ -502,6 +536,19 @@
apply (simp add: add_increasing)
done
+text{*Needed for the infinitely close relation over the nonstandard
+ complex numbers*}
+lemma lemma_sqrt_hcomplex_capprox:
+ "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
+apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
+apply (erule_tac [2] lemma_real_divide_sqrt_less)
+apply (rule power2_le_imp_le)
+apply (auto simp add: real_0_le_divide_iff power_divide)
+apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
+apply (rule add_mono)
+apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
+done
+
text "Legacy theorem names:"
lemmas real_root_pos2 = real_root_power_cancel
lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]