author huffman Mon May 14 18:04:52 2007 +0200 (2007-05-14) changeset 22969 bf523cac9a05 parent 22968 7134874437ac child 22970 b5910e3dec4c
tuned proofs
```     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 18:03:25 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon May 14 18:04:52 2007 +0200
1.3 @@ -1093,14 +1093,12 @@
1.4
1.5  lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
1.6  apply (cut_tac x = x and y = y in sin_cos_add)
1.7 -apply (auto dest!: real_sum_squares_cancel_a
1.10  done
1.11
1.12  lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
1.13  apply (cut_tac x = x and y = y in sin_cos_add)
1.14 -apply (auto dest!: real_sum_squares_cancel_a
1.17  done
1.18
1.19  lemma lemma_DERIV_sin_cos_minus:
1.20 @@ -1114,33 +1112,27 @@
1.21      "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
1.22  apply (cut_tac y = 0 and x = x
1.23         in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
1.24 -apply (auto simp add: numeral_2_eq_2)
1.25 +apply simp
1.26  done
1.27
1.28  lemma sin_minus [simp]: "sin (-x) = -sin(x)"
1.29  apply (cut_tac x = x in sin_cos_minus)
1.30 -apply (auto dest!: real_sum_squares_cancel_a
1.32 +apply (simp del: sin_cos_minus)
1.33  done
1.34
1.35  lemma cos_minus [simp]: "cos (-x) = cos(x)"
1.36  apply (cut_tac x = x in sin_cos_minus)
1.37 -apply (auto dest!: real_sum_squares_cancel_a
1.38 -                   simp add: numeral_2_eq_2 simp del: sin_cos_minus)
1.39 +apply (simp del: sin_cos_minus)
1.40  done
1.41
1.42  lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
1.45 -done
1.47
1.48  lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
1.49  by (simp add: sin_diff mult_commute)
1.50
1.51  lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
1.54 -done
1.56
1.57  lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
1.58  by (simp add: cos_diff mult_commute)
1.59 @@ -1151,7 +1143,7 @@
1.60
1.61  lemma cos_double: "cos(2* x) = ((cos x)\<twosuperior>) - ((sin x)\<twosuperior>)"
1.62  apply (cut_tac x = x and y = x in cos_add)
1.63 -apply (auto simp add: numeral_2_eq_2)
1.65  done
1.66
1.67
1.68 @@ -2072,18 +2064,16 @@
1.69        |] ==>  sin xa = y / sqrt (x * x + y * y) |
1.70                sin xa = - y / sqrt (x * x + y * y)"
1.71  apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong)
1.72 -apply (frule_tac y = y in real_sum_square_gt_zero)
1.73 +apply (subgoal_tac "0 < x * x + y * y")
1.75  apply (subgoal_tac "(sin xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2")
1.76  apply (rule_tac [2] lemma_cos_sin_eq)
1.77  apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc)
1.78 +apply (auto simp add: sum_squares_gt_zero_iff)
1.79  done
1.80
1.81  lemma lemma_cos_not_eq_zero: "x \<noteq> 0 ==> x / sqrt (x * x + y * y) \<noteq> 0"
1.83 -apply (frule_tac y3 = y in real_sqrt_sum_squares_gt_zero3 [THEN real_not_refl2, THEN not_sym, THEN nonzero_imp_inverse_nonzero])
1.84 -apply (auto simp add: power2_eq_square)
1.85 -done
1.86 +by (simp add: divide_inverse sum_squares_eq_zero_iff)
1.87
1.88  lemma cos_x_y_disj:
1.89       "[| x \<noteq> 0;
1.90 @@ -2091,18 +2081,16 @@
1.91        |] ==>  cos xa = x / sqrt (x * x + y * y) |
1.92                cos xa = - x / sqrt (x * x + y * y)"
1.93  apply (drule_tac f = "%x. x\<twosuperior>" in arg_cong)
1.94 -apply (frule_tac y = y in real_sum_square_gt_zero)
1.95 +apply (subgoal_tac "0 < x * x + y * y")
1.96  apply (simp add: sin_squared_eq del: realpow_Suc)
1.97  apply (subgoal_tac "(cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2")
1.98  apply (rule_tac [2] lemma_sin_cos_eq)
1.99  apply (auto simp add: realpow_two_disj numeral_2_eq_2 simp del: realpow_Suc)
1.100 +apply (auto simp add: sum_squares_gt_zero_iff)
1.101  done
1.102
1.103  lemma real_sqrt_divide_less_zero: "0 < y ==> - y / sqrt (x * x + y * y) < 0"
1.104 -apply (case_tac "x = 0", auto)
1.105 -apply (drule_tac y = y in real_sqrt_sum_squares_gt_zero3)
1.106 -apply (auto simp add: zero_less_mult_iff divide_inverse power2_eq_square)
1.107 -done
1.108 +by (simp add: divide_pos_pos sum_squares_gt_zero_iff)
1.109
1.110  lemma polar_ex1:
1.111       "[| x \<noteq> 0; 0 < y |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
1.112 @@ -2124,7 +2112,7 @@
1.113  done
1.114
1.115  lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
1.116 -by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)