src/HOL/Hyperreal/MacLaurin.thy
changeset 15234 ec91a90c604e
parent 15229 1eb23f805c06
child 15251 bb6f072c8d10
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -38,10 +38,11 @@
     "0 < h ==>
      \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
                (B * ((h^n) / real(fact n)))"
-by (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
+apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
                  real(fact n) / (h^n)"
-       in exI, auto)
-
+       in exI)
+apply (simp add: times_divide_eq) 
+done
 
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
@@ -159,12 +160,12 @@
  prefer 2 apply simp
 apply (frule Maclaurin_lemma2, assumption+)
 apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
-apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
-apply (erule impE)
-apply (simp (no_asm_simp))
-apply (erule exE)
-apply (rule_tac x = t in exI)
-apply (simp del: realpow_Suc fact_Suc)
+ apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
+ apply (erule impE)
+  apply (simp (no_asm_simp))
+ apply (erule exE)
+ apply (rule_tac x = t in exI)
+ apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
  prefer 2
  apply clarify
@@ -254,7 +255,7 @@
 apply (cut_tac f = "%x. f (-x)"
         and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
         and h = "-h" and n = n in Maclaurin_objl)
-apply simp
+apply (simp add: times_divide_eq) 
 apply safe
 apply (subst minus_mult_right)
 apply (rule DERIV_cmult)
@@ -303,7 +304,7 @@
 apply (case_tac "n = 0", force)
 apply (case_tac "x = 0")
 apply (rule_tac x = 0 in exI)
-apply (force simp add: Maclaurin_bi_le_lemma)
+apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
 txt{*Case 1, where @{term "x < 0"}*}
 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
@@ -414,27 +415,8 @@
       "0 < n --> Suc (2 * n - 1) = 2*n"
 by (induct_tac "n", auto)
 
-lemma Maclaurin_sin_expansion:
-     "\<exists>t. sin x =
-       (sumr 0 n (%m. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
-      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
-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)
-apply safe
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (case_tac "n", clarify, simp)
-apply (drule_tac x = 0 in spec, simp, simp)
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
-(*Could sin_zero_iff help?*)
-done
+
+text{*It is unclear why so many variant results are needed.*}
 
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
@@ -447,17 +429,28 @@
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (case_tac "n", clarify, simp, simp)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
+lemma Maclaurin_sin_expansion:
+     "\<exists>t. sin x =
+       (sumr 0 n (%m. (if even m then 0
+                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       x ^ m))
+      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+apply (insert Maclaurin_sin_expansion2 [of x n]) 
+apply (blast intro: elim:); 
+done
+
+
+
 lemma Maclaurin_sin_expansion3:
      "[| 0 < n; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
@@ -469,12 +462,11 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
 lemma Maclaurin_sin_expansion4:
@@ -488,12 +480,11 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
 
@@ -518,7 +509,7 @@
 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)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (case_tac "n", simp)
 apply (simp del: sumr_Suc)
 apply (rule ccontr, simp)
@@ -526,9 +517,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
 lemma Maclaurin_cos_expansion2:
@@ -543,16 +532,15 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
-lemma Maclaurin_minus_cos_expansion: "[| x < 0; 0 < n |] ==>
+lemma Maclaurin_minus_cos_expansion:
+     "[| x < 0; 0 < n |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
        (sumr 0 n (%m. (if even m
@@ -563,13 +551,11 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
 (* ------------------------------------------------------------------------- *)