# HG changeset patch
# User huffman
# Date 1179206888 -7200
# Node ID 1cd8cc21a7c312894fd0e3b329a5a98e78e27b9e
# Parent  04fd6cc1c4a9c942bda0dae777fbe080e9c22a07
clean up polar_Ex proofs; remove unnecessary lemmas

diff -r 04fd6cc1c4a9 -r 1cd8cc21a7c3 src/HOL/Hyperreal/Transcendental.thy
--- 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)"
-by (simp add: power2_eq_square [symmetric])
-
-lemma minus_le_real_sqrt_sumsq [simp]: "-x \<le> sqrt (x * x + y * y)"
-apply (simp add: power2_eq_square [symmetric])
-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)"
-by (simp add: sum_squares_gt_zero_iff)
-
-lemma real_sqrt_sum_squares_gt_zero2: "0 < x ==> 0 < sqrt (x * x + y * y)"
-by (simp add: sum_squares_gt_zero_iff)
+subsection {* Existence of Polar Coordinates *}
 
-lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
-by (simp add: add_pos_nonneg)
-
-lemma real_sqrt_sum_squares_gt_zero3a: "y \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
-by (simp add: add_nonneg_pos)
-
-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"
-by (simp add: divide_le_eq not_sum_squares_lt_zero)
-
-lemma lemma_real_divide_sqrt_ge_minus_one2:
-     "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
-apply (simp add: divide_const_simps
-            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"
-by (simp add: divide_le_eq not_sum_squares_lt_zero)
-
-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"
-by (subst add_commute, simp add: minus_sqrt_le) 
-
-lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
-by (simp add: not_sum_squares_lt_zero)
-
-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)"
-by (subst add_commute, simp add: cos_x_y_ge_minus_one)
-
-lemma cos_x_y_le_one (*[simp]*): "x / sqrt (x * x + y * y) \<le> 1" 
-by (simp add: divide_le_eq not_sum_squares_lt_zero)
-
-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)
-apply (simp add: real_add_commute)
-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"
+by (simp add: abs_le_iff)
 
-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"
+by (simp add: abs_le_iff cos_total)
 
-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])
-apply (subst add_commute)
-apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff)
-apply (simp add: add_commute)
-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 (simp add: cos_squared_eq)
-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)
 apply (auto simp add: sum_squares_gt_zero_iff)
 done
 
-lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
-by (simp add: divide_inverse sum_squares_eq_zero_iff)
-
-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)
-apply (auto simp add: sum_squares_gt_zero_iff)
-done
-
-lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0"
-by (simp add: divide_pos_pos sum_squares_gt_zero_iff)
+lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x\<twosuperior> + y\<twosuperior>) < 0"
+by (simp add: divide_pos_pos sum_power2_gt_zero_iff)
 
 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 (simp add: cos_arccos_lemma1)
 apply (simp add: arccos_def)
-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 simp add: power2_eq_square)
+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)"
-by (simp add: real_add_eq_0_iff [symmetric] sum_squares_eq_zero_iff)
-
 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 
-            simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)
-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 (auto simp add: real_0_le_add_iff real_add_eq_0_iff)
-apply (drule cos_ge_zero, force)
-apply (drule_tac x = y in real_sqrt_divide_less_zero)
-apply (auto simp add: add_commute)
-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)"
+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)