author huffman Tue, 15 May 2007 07:28:08 +0200 changeset 22978 1cd8cc21a7c3 parent 22977 04fd6cc1c4a9 child 22979 d95580341be5
clean up polar_Ex proofs; remove unnecessary lemmas
```--- a/src/HOL/Hyperreal/Transcendental.thy	Tue May 15 05:09:01 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue May 15 07:28:08 2007 +0200
@@ -1902,118 +1902,22 @@
by (cut_tac x = x in sin_cos_squared_add3, auto)

-subsection{*Theorems About Sqrt, Transcendental Functions for Complex*}
-
-lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
-
-lemma minus_le_real_sqrt_sumsq [simp]: "-x \<le> sqrt (x * x + y * y)"
-apply (rule power2_le_imp_le, simp_all)
-done
-
-lemma lemma_real_divide_sqrt_ge_minus_one:
-     "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))"
-by (simp add: divide_const_simps linorder_not_le [symmetric]
-         del: real_sqrt_le_0_iff real_sqrt_ge_0_iff)
-
-lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)"
-
-lemma real_sqrt_sum_squares_gt_zero2: "0 < x ==> 0 < sqrt (x * x + y * y)"
+subsection {* Existence of Polar Coordinates *}

-lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
-
-lemma real_sqrt_sum_squares_gt_zero3a: "y \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
-
-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 lemma_real_divide_sqrt_le_one: "x < 0 ==> x/(sqrt (x * x + y * y)) \<le> 1"
-
-lemma lemma_real_divide_sqrt_ge_minus_one2:
-     "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
-            del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff)
-apply (insert minus_le_real_sqrt_sumsq [of x y], arith)
+lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<twosuperior> + y\<twosuperior>)\<bar> \<le> 1"
+apply (rule power2_le_imp_le [OF _ zero_le_one])
+apply (simp add: abs_divide power_divide divide_le_eq not_sum_power2_lt_zero)
done

-lemma lemma_real_divide_sqrt_le_one2: "0 < x ==> x/(sqrt (x * x + y * y)) \<le> 1"
-
-lemma minus_sqrt_le: "- sqrt (x * x + y * y) \<le> x"
-by (insert minus_le_real_sqrt_sumsq [of x y], arith)
-
-lemma minus_sqrt_le2: "- sqrt (x * x + y * y) \<le> y"
-
-lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
-
-lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
-by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps
-         del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff)
-
-lemma cos_x_y_ge_minus_one1a (*[simp]*): "-1 \<le> y / sqrt (x * x + y * y)"
-
-lemma cos_x_y_le_one (*[simp]*): "x / sqrt (x * x + y * y) \<le> 1"
-
-lemma cos_x_y_le_one2 (*[simp]*): "y / sqrt (x * x + y * y) \<le> 1"
-apply (cut_tac x = y and y = x in cos_x_y_le_one)
-done
-
-lemmas cos_arccos_lemma1 = (* used by polar_ex1 *)
-  cos_arccos [OF cos_x_y_ge_minus_one cos_x_y_le_one]
-
-lemmas arccos_bounded_lemma1 =
-  arccos_bounded [OF cos_x_y_ge_minus_one cos_x_y_le_one]
+lemma cos_arccos_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> cos (arccos y) = y"

-lemmas cos_arccos_lemma2 =
-  cos_arccos [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]
-
-lemmas arccos_bounded_lemma2 =
-  arccos_bounded [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2]
-
-lemma cos_abs_x_y_ge_minus_one (*[simp]*):
-     "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
-by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]
-         simp del: real_sqrt_ge_0_iff real_sqrt_le_0_iff)
-
-lemma cos_abs_x_y_le_one (*[simp]*): "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1"
-apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y])
-apply (auto simp add: divide_const_simps abs_if linorder_neq_iff
-            simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
-done
+lemma cos_total_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> \<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = y"

-lemmas cos_arccos_lemma3 =
-  cos_arccos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one]
-
-lemmas arccos_bounded_lemma3 =
-  arccos_bounded [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one]
-
-lemma minus_pi_less_zero (*[simp]*): "-pi < 0"
-by simp
+lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]

-lemma minus_pi_le_zero (*[simp]*): "-pi \<le> 0"
-by simp
-
-lemma arccos_ge_minus_pi: "[| -1 \<le> y; y \<le> 1 |] ==> -pi \<le> arccos y"
-apply (rule real_le_trans)
-apply (rule_tac [2] arccos_lbound, auto)
-done
-
-lemmas arccos_ge_minus_pi_lemma =
-  arccos_ge_minus_pi [OF cos_x_y_ge_minus_one cos_x_y_le_one, simp]
+lemmas cos_total_lemma1 = cos_total_abs [OF cos_x_y_le_one]

(* How tedious! *)
lemma lemma_divide_rearrange:
@@ -2033,112 +1937,68 @@
done

lemma lemma_cos_sin_eq:
-     "[| 0 < x * x + y * y;
-         1 - (sin xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2 |]
-      ==> (sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2"
-by (auto intro: lemma_divide_rearrange
-         simp add: power_divide power2_eq_square [symmetric])
-
-
-lemma lemma_sin_cos_eq:
-     "[| 0 < x * x + y * y;
-         1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
-      ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"
-apply (auto simp add: power_divide power2_eq_square [symmetric])
-done
+     "[| 0 < x\<twosuperior> + y\<twosuperior>;
+         1 - (sin xa)\<twosuperior> = (x / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior> |]
+      ==> (sin xa)\<twosuperior> = (y / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior>"
+by (auto intro: lemma_divide_rearrange simp add: power_divide)

lemma sin_x_y_disj:
-     "[| x \<noteq> 0;
-         cos xa = x / sqrt (x * x + y * y)
-      |] ==>  sin xa = y / sqrt (x * x + y * y) |
-              sin xa = - y / sqrt (x * x + y * y)"
+     "[| 0 < y;
+         cos xa = x / sqrt (x\<twosuperior> + y\<twosuperior>)
+      |] ==>  sin xa = y / sqrt (x\<twosuperior> + y\<twosuperior>) |
+              sin xa = - y / sqrt (x\<twosuperior> + y\<twosuperior>)"
apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong)
-apply (subgoal_tac "0 < x * x + y * y")
+apply (subgoal_tac "0 < x\<twosuperior> + y\<twosuperior>")
-apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2")
+apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior>")
apply (rule_tac [2] lemma_cos_sin_eq)
apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc)
done

-lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
-
-lemma cos_x_y_disj:
-     "[| x \<noteq> 0;
-         sin xa = y / sqrt (x * x + y * y)
-      |] ==>  cos xa = x / sqrt (x * x + y * y) |
-              cos xa = - x / sqrt (x * x + y * y)"
-apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong)
-apply (subgoal_tac "0 < x * x + y * y")
-apply (simp add: sin_squared_eq del: realpow_Suc)
-apply (subgoal_tac "(cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2")
-apply (rule_tac [2] lemma_sin_cos_eq)
-apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc)
-done
-
-lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0"
+lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x\<twosuperior> + y\<twosuperior>) < 0"

lemma polar_ex1:
-     "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
+     "0 < y ==> \<exists>r a. x = r * cos a & y = r * sin a"
apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
-apply (rule_tac x = "arccos (x / sqrt (x * x + y * y))" in exI)
-apply auto
-apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
-apply (auto simp add: power2_eq_square cos_arccos_lemma1)
+apply (rule_tac x = "arccos (x / sqrt (x\<twosuperior> + y\<twosuperior>))" in exI)
-apply (cut_tac x1 = x and y1 = y
-       in cos_total [OF cos_x_y_ge_minus_one cos_x_y_le_one])
+apply (cut_tac x1 = x and y1 = y in cos_total_lemma1)
apply (rule someI2_ex, blast)
-apply (erule_tac V = "EX! xa. 0 \<le> xa & xa \<le> pi & cos xa = x / sqrt (x * x + y * y)" in thin_rl)
+apply (erule_tac V = "Ex1 ?P" in thin_rl)
apply (frule sin_x_y_disj, blast)
-apply (drule_tac y2 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym])
+apply (auto)
apply (drule sin_ge_zero, assumption)
apply (drule_tac x = x in real_sqrt_divide_less_zero, auto)
done

-lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
-
lemma polar_ex2:
-     "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
-apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
-apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>)" in exI)
-apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
-apply (subst sin_arcsin [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
-apply (auto dest: real_sum_squares_cancel2a
-apply (unfold arcsin_def)
-apply (cut_tac x1 = x and y1 = y
-       in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
-apply (rule someI2_ex, blast)
-apply (erule_tac V = "EX! v. ?P v" in thin_rl)
-apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast)
-apply (drule cos_ge_zero, force)
-apply (drule_tac x = y in real_sqrt_divide_less_zero)
-apply (insert polar_ex1 [of x "-y"], simp, clarify)
+     "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
+apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify)
apply (rule_tac x = r in exI)
-apply (rule_tac x = "-a" in exI, simp)
+apply (rule_tac x = "-a" in exI, simp)
done

lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
-apply (case_tac "x = 0", auto)
-apply (rule_tac x = y in exI)
-apply (rule_tac x = "pi/2" in exI, auto)
-apply (cut_tac x = 0 and y = y in linorder_less_linear, auto)
-apply (rule_tac [2] x = x in exI)
-apply (rule_tac [2] x = 0 in exI, auto)
-apply (blast intro: polar_ex1 polar_ex2)+
+apply (rule_tac x=0 and y=y in linorder_cases)
+apply (erule polar_ex1)
+apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
+apply (erule polar_ex2)
done

+subsection {* Theorems About Sqrt *}
+
+lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"