# HG changeset patch
# User huffman
# Date 1179648786 -7200
# Node ID 11607c283074d278ade249c8bec1f12af7fc078e
# Parent  5e40f1e9958a4c1219a5cb15b57f00b9cf9506e9
moved sqrt lemmas from Transcendental.thy to NthRoot.thy

diff -r 5e40f1e9958a -r 11607c283074 src/HOL/Hyperreal/NthRoot.thy
--- 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]
diff -r 5e40f1e9958a -r 11607c283074 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 09:50:56 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 10:13:06 2007 +0200
@@ -2064,56 +2064,6 @@
 apply (erule polar_ex2)
 done
 
-subsection {* Theorems About Sqrt *}
-
-lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
-by (simp add: power2_eq_square [symmetric])
-
-lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> 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 ==> x = 0"
-by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
-
-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 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 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)
-
-
-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
-
-declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
-
 
 subsection {* Theorems about Limits *}