author huffman Thu May 31 22:23:50 2007 +0200 (2007-05-31) changeset 23176 40a760921d94 parent 23175 267ba70e7a9d child 23177 3004310c95b1
simplify some proofs
```     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]
```