1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy Wed Oct 06 13:59:33 2004 +0200
1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy Thu Oct 07 15:42:30 2004 +0200
1.3 @@ -38,10 +38,11 @@
1.4 "0 < h ==>
1.5 \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
1.6 (B * ((h^n) / real(fact n)))"
1.7 -by (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
1.8 +apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
1.9 real(fact n) / (h^n)"
1.10 - in exI, auto)
1.11 -
1.12 + in exI)
1.13 +apply (simp add: times_divide_eq)
1.14 +done
1.15
1.16 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
1.17 by arith
1.18 @@ -159,12 +160,12 @@
1.19 prefer 2 apply simp
1.20 apply (frule Maclaurin_lemma2, assumption+)
1.21 apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
1.22 -apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
1.23 -apply (erule impE)
1.24 -apply (simp (no_asm_simp))
1.25 -apply (erule exE)
1.26 -apply (rule_tac x = t in exI)
1.27 -apply (simp del: realpow_Suc fact_Suc)
1.28 + apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
1.29 + apply (erule impE)
1.30 + apply (simp (no_asm_simp))
1.31 + apply (erule exE)
1.32 + apply (rule_tac x = t in exI)
1.33 + apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
1.34 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
1.35 prefer 2
1.36 apply clarify
1.37 @@ -254,7 +255,7 @@
1.38 apply (cut_tac f = "%x. f (-x)"
1.39 and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
1.40 and h = "-h" and n = n in Maclaurin_objl)
1.41 -apply simp
1.42 +apply (simp add: times_divide_eq)
1.43 apply safe
1.44 apply (subst minus_mult_right)
1.45 apply (rule DERIV_cmult)
1.46 @@ -303,7 +304,7 @@
1.47 apply (case_tac "n = 0", force)
1.48 apply (case_tac "x = 0")
1.49 apply (rule_tac x = 0 in exI)
1.50 -apply (force simp add: Maclaurin_bi_le_lemma)
1.51 +apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
1.52 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
1.53 txt{*Case 1, where @{term "x < 0"}*}
1.54 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
1.55 @@ -414,27 +415,8 @@
1.56 "0 < n --> Suc (2 * n - 1) = 2*n"
1.57 by (induct_tac "n", auto)
1.58
1.59 -lemma Maclaurin_sin_expansion:
1.60 - "\<exists>t. sin x =
1.61 - (sumr 0 n (%m. (if even m then 0
1.62 - else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.63 - x ^ m))
1.64 - + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.65 -apply (cut_tac f = sin and n = n and x = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
1.66 -apply safe
1.67 -apply (simp (no_asm))
1.68 -apply (simp (no_asm))
1.69 -apply (case_tac "n", clarify, simp)
1.70 -apply (drule_tac x = 0 in spec, simp, simp)
1.71 -apply (rule ccontr, simp)
1.72 -apply (drule_tac x = x in spec, simp)
1.73 -apply (erule ssubst)
1.74 -apply (rule_tac x = t in exI, simp)
1.75 -apply (rule sumr_fun_eq)
1.76 -apply (auto simp add: odd_Suc_mult_two_ex)
1.77 -apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
1.78 -(*Could sin_zero_iff help?*)
1.79 -done
1.80 +
1.81 +text{*It is unclear why so many variant results are needed.*}
1.82
1.83 lemma Maclaurin_sin_expansion2:
1.84 "\<exists>t. abs t \<le> abs x &
1.85 @@ -447,17 +429,28 @@
1.86 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.87 apply safe
1.88 apply (simp (no_asm))
1.89 -apply (simp (no_asm))
1.90 +apply (simp (no_asm) add: times_divide_eq)
1.91 apply (case_tac "n", clarify, simp, simp)
1.92 apply (rule ccontr, simp)
1.93 apply (drule_tac x = x in spec, simp)
1.94 apply (erule ssubst)
1.95 apply (rule_tac x = t in exI, simp)
1.96 apply (rule sumr_fun_eq)
1.97 -apply (auto simp add: odd_Suc_mult_two_ex)
1.98 -apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
1.99 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.100 done
1.101
1.102 +lemma Maclaurin_sin_expansion:
1.103 + "\<exists>t. sin x =
1.104 + (sumr 0 n (%m. (if even m then 0
1.105 + else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
1.106 + x ^ m))
1.107 + + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.108 +apply (insert Maclaurin_sin_expansion2 [of x n])
1.109 +apply (blast intro: elim:);
1.110 +done
1.111 +
1.112 +
1.113 +
1.114 lemma Maclaurin_sin_expansion3:
1.115 "[| 0 < n; 0 < x |] ==>
1.116 \<exists>t. 0 < t & t < x &
1.117 @@ -469,12 +462,11 @@
1.118 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.119 apply safe
1.120 apply simp
1.121 -apply (simp (no_asm))
1.122 +apply (simp (no_asm) add: times_divide_eq)
1.123 apply (erule ssubst)
1.124 apply (rule_tac x = t in exI, simp)
1.125 apply (rule sumr_fun_eq)
1.126 -apply (auto simp add: odd_Suc_mult_two_ex)
1.127 -apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
1.128 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.129 done
1.130
1.131 lemma Maclaurin_sin_expansion4:
1.132 @@ -488,12 +480,11 @@
1.133 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
1.134 apply safe
1.135 apply simp
1.136 -apply (simp (no_asm))
1.137 +apply (simp (no_asm) add: times_divide_eq)
1.138 apply (erule ssubst)
1.139 apply (rule_tac x = t in exI, simp)
1.140 apply (rule sumr_fun_eq)
1.141 -apply (auto simp add: odd_Suc_mult_two_ex)
1.142 -apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
1.143 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
1.144 done
1.145
1.146
1.147 @@ -518,7 +509,7 @@
1.148 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
1.149 apply safe
1.150 apply (simp (no_asm))
1.151 -apply (simp (no_asm))
1.152 +apply (simp (no_asm) add: times_divide_eq)
1.153 apply (case_tac "n", simp)
1.154 apply (simp del: sumr_Suc)
1.155 apply (rule ccontr, simp)
1.156 @@ -526,9 +517,7 @@
1.157 apply (erule ssubst)
1.158 apply (rule_tac x = t in exI, simp)
1.159 apply (rule sumr_fun_eq)
1.160 -apply (auto simp add: odd_Suc_mult_two_ex)
1.161 -apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
1.162 -apply (simp add: mult_commute [of _ pi])
1.163 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.164 done
1.165
1.166 lemma Maclaurin_cos_expansion2:
1.167 @@ -543,16 +532,15 @@
1.168 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.169 apply safe
1.170 apply simp
1.171 -apply (simp (no_asm))
1.172 +apply (simp (no_asm) add: times_divide_eq)
1.173 apply (erule ssubst)
1.174 apply (rule_tac x = t in exI, simp)
1.175 apply (rule sumr_fun_eq)
1.176 -apply (auto simp add: odd_Suc_mult_two_ex)
1.177 -apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
1.178 -apply (simp add: mult_commute [of _ pi])
1.179 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.180 done
1.181
1.182 -lemma Maclaurin_minus_cos_expansion: "[| x < 0; 0 < n |] ==>
1.183 +lemma Maclaurin_minus_cos_expansion:
1.184 + "[| x < 0; 0 < n |] ==>
1.185 \<exists>t. x < t & t < 0 &
1.186 cos x =
1.187 (sumr 0 n (%m. (if even m
1.188 @@ -563,13 +551,11 @@
1.189 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
1.190 apply safe
1.191 apply simp
1.192 -apply (simp (no_asm))
1.193 +apply (simp (no_asm) add: times_divide_eq)
1.194 apply (erule ssubst)
1.195 apply (rule_tac x = t in exI, simp)
1.196 apply (rule sumr_fun_eq)
1.197 -apply (auto simp add: odd_Suc_mult_two_ex)
1.198 -apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
1.199 -apply (simp add: mult_commute [of _ pi])
1.200 +apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.201 done
1.202
1.203 (* ------------------------------------------------------------------------- *)