src/HOL/Hyperreal/MacLaurin.thy
changeset 15234 ec91a90c604e
parent 15229 1eb23f805c06
child 15251 bb6f072c8d10
     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  (* ------------------------------------------------------------------------- *)