src/HOL/Hyperreal/Transcendental.thy
changeset 23176 40a760921d94
parent 23127 56ee8105c002
child 23177 3004310c95b1
     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 21:09:14 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 22:23:50 2007 +0200
     1.3 @@ -580,9 +580,7 @@
     1.4         = (if even n then  
     1.5                   (- 1) ^ (n div 2)/(real (fact n))  
     1.6                else 0)"
     1.7 -by (auto intro!: ext 
     1.8 -         simp add: diffs_def divide_inverse real_of_nat_def
     1.9 -         simp del: mult_Suc of_nat_Suc)
    1.10 +by (simp only: sin_fdiffs)
    1.11  
    1.12  lemma cos_fdiffs: 
    1.13        "diffs(%n. if even n then  
    1.14 @@ -599,9 +597,7 @@
    1.15                   (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
    1.16         = - (if even n then 0  
    1.17             else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
    1.18 -by (auto intro!: ext 
    1.19 -         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
    1.20 -         simp del: mult_Suc of_nat_Suc)
    1.21 +by (simp only: cos_fdiffs)
    1.22  
    1.23  text{*Now at last we can get the derivatives of exp, sin and cos*}
    1.24  
    1.25 @@ -1254,12 +1250,10 @@
    1.26              (if even k then 0
    1.27               else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
    1.28              x ^ k) 
    1.29 -	sums
    1.30 -	(\<Sum>n. (if even n then 0
    1.31 -		     else (- 1) ^ ((n - Suc 0) div 2) / real (fact n)) *
    1.32 -	            x ^ n)" 
    1.33 +	sums sin x"
    1.34 +    unfolding sin_def
    1.35      by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
    1.36 -  thus ?thesis by (simp add: mult_ac sin_def)
    1.37 +  thus ?thesis by (simp add: mult_ac)
    1.38  qed
    1.39  
    1.40  lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
    1.41 @@ -1323,11 +1317,10 @@
    1.42    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
    1.43              (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
    1.44              x ^ k) 
    1.45 -        sums
    1.46 -	(\<Sum>n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) *
    1.47 -	      x ^ n)" 
    1.48 +        sums cos x"
    1.49 +    unfolding cos_def
    1.50      by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) 
    1.51 -  thus ?thesis by (simp add: mult_ac cos_def)
    1.52 +  thus ?thesis by (simp add: mult_ac)
    1.53  qed
    1.54  
    1.55  declare zero_less_power [simp]