author huffman Sun, 20 May 2007 10:13:06 +0200 changeset 23049 11607c283074 parent 23048 5e40f1e9958a child 23050 722f58379538
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
 src/HOL/Hyperreal/NthRoot.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/Transcendental.thy file | annotate | diff | comparison | revisions
```--- 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]```
```--- 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 *}
```