author huffman Mon, 14 May 2007 18:04:52 +0200 changeset 22969 bf523cac9a05 parent 22968 7134874437ac child 22970 b5910e3dec4c
tuned proofs
```--- 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
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
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 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
+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"
-done

lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"

lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
-done

lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
@@ -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)
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 (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)
done

lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
-apply (frule_tac y3 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym, THEN nonzero_imp_inverse_nonzero])
-done

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)
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

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)