tuned proofs
authorhuffman
Mon May 14 18:04:52 2007 +0200 (2007-05-14)
changeset 22969bf523cac9a05
parent 22968 7134874437ac
child 22970 b5910e3dec4c
tuned proofs
src/HOL/Hyperreal/Transcendental.thy
     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.8 -            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
     1.9 +apply (simp del: sin_cos_add)
    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.15 -            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
    1.16 +apply (simp del: sin_cos_add)
    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.31 -       simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)
    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.43 -apply (simp add: diff_minus)
    1.44 -apply (simp (no_asm) add: sin_add)
    1.45 -done
    1.46 +by (simp add: diff_minus sin_add)
    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.52 -apply (simp add: diff_minus)
    1.53 -apply (simp (no_asm) add: cos_add)
    1.54 -done
    1.55 +by (simp add: diff_minus cos_add)
    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.64 +apply (simp add: power2_eq_square)
    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.74  apply (simp add: cos_squared_eq)
    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.82 -apply (simp add: divide_inverse)
    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)
   1.117 +by (simp add: real_add_eq_0_iff [symmetric] sum_squares_eq_zero_iff)
   1.118  
   1.119  lemma polar_ex2:
   1.120       "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
   1.121 @@ -2174,7 +2162,7 @@
   1.122  by simp
   1.123  
   1.124  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
   1.125 -by (simp add: divide_less_eq mult_compare_simps) 
   1.126 +by (simp add: divide_less_eq mult_compare_simps)
   1.127  
   1.128  lemma four_x_squared: 
   1.129    fixes x::real