# HG changeset patch
# User huffman
# Date 1179158692 -7200
# Node ID bf523cac9a055ada7bfa343d76ea07d69af2d436
# Parent  7134874437acdd2277155bae05da75258fa22d6b
tuned proofs

diff -r 7134874437ac -r bf523cac9a05 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 18:03:25 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 18:04:52 2007 +0200
@@ -1093,14 +1093,12 @@
 
 lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
 apply (cut_tac x = x and y = y in sin_cos_add)
-apply (auto dest!: real_sum_squares_cancel_a 
-            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
+apply (simp del: sin_cos_add)
 done
 
 lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
 apply (cut_tac x = x and y = y in sin_cos_add)
-apply (auto dest!: real_sum_squares_cancel_a
-            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
+apply (simp del: sin_cos_add)
 done
 
 lemma lemma_DERIV_sin_cos_minus:
@@ -1114,33 +1112,27 @@
     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
 apply (cut_tac y = 0 and x = x 
        in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
-apply (auto simp add: numeral_2_eq_2)
+apply simp
 done
 
 lemma sin_minus [simp]: "sin (-x) = -sin(x)"
 apply (cut_tac x = x in sin_cos_minus)
-apply (auto dest!: real_sum_squares_cancel_a 
-       simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)
+apply (simp del: sin_cos_minus)
 done
 
 lemma cos_minus [simp]: "cos (-x) = cos(x)"
 apply (cut_tac x = x in sin_cos_minus)
-apply (auto dest!: real_sum_squares_cancel_a 
-                   simp add: numeral_2_eq_2 simp del: sin_cos_minus)
+apply (simp del: sin_cos_minus)
 done
 
 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
-apply (simp add: diff_minus)
-apply (simp (no_asm) add: sin_add)
-done
+by (simp add: diff_minus sin_add)
 
 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
 by (simp add: sin_diff mult_commute)
 
 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-apply (simp add: diff_minus)
-apply (simp (no_asm) add: cos_add)
-done
+by (simp add: diff_minus cos_add)
 
 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
 by (simp add: cos_diff mult_commute)
@@ -1151,7 +1143,7 @@
 
 lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
 apply (cut_tac x = x and y = x in cos_add)
-apply (auto simp add: numeral_2_eq_2)
+apply (simp add: power2_eq_square)
 done
 
 
@@ -2072,18 +2064,16 @@
       |] ==>  sin xa = y / sqrt (x * x + y * y) |  
               sin xa = - y / sqrt (x * x + y * y)"
 apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong)
-apply (frule_tac y = y in real_sum_square_gt_zero)
+apply (subgoal_tac "0 < x * x + y * y")
 apply (simp add: cos_squared_eq)
 apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2")
 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"
-apply (simp add: divide_inverse)
-apply (frule_tac y3 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym, THEN nonzero_imp_inverse_nonzero])
-apply (auto simp add: power2_eq_square)
-done
+by (simp add: divide_inverse sum_squares_eq_zero_iff)
 
 lemma cos_x_y_disj:
      "[| x \<noteq> 0;  
@@ -2091,18 +2081,16 @@
       |] ==>  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 (frule_tac y = y in real_sum_square_gt_zero)
+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"
-apply (case_tac "x = 0", auto)
-apply (drule_tac y = y in real_sqrt_sum_squares_gt_zero3)
-apply (auto simp add: zero_less_mult_iff divide_inverse power2_eq_square)
-done
+by (simp add: divide_pos_pos sum_squares_gt_zero_iff)
 
 lemma polar_ex1:
      "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
@@ -2124,7 +2112,7 @@
 done
 
 lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
-by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
+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"
@@ -2174,7 +2162,7 @@
 by simp
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
-by (simp add: divide_less_eq mult_compare_simps) 
+by (simp add: divide_less_eq mult_compare_simps)
 
 lemma four_x_squared: 
   fixes x::real