equal
deleted
inserted
replaced
428 apply (cut_tac f = sin and n = n and x = x |
428 apply (cut_tac f = sin and n = n and x = x |
429 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) |
429 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) |
430 apply safe |
430 apply safe |
431 apply (simp (no_asm)) |
431 apply (simp (no_asm)) |
432 apply (simp (no_asm) add: sin_expansion_lemma) |
432 apply (simp (no_asm) add: sin_expansion_lemma) |
|
433 apply (force intro!: DERIV_intros) |
433 apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp) |
434 apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp) |
434 apply (cases n, simp, simp) |
435 apply (cases n, simp, simp) |
435 apply (rule ccontr, simp) |
436 apply (rule ccontr, simp) |
436 apply (drule_tac x = x in spec, simp) |
437 apply (drule_tac x = x in spec, simp) |
437 apply (erule ssubst) |
438 apply (erule ssubst) |
456 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" |
457 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" |
457 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) |
458 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) |
458 apply safe |
459 apply safe |
459 apply simp |
460 apply simp |
460 apply (simp (no_asm) add: sin_expansion_lemma) |
461 apply (simp (no_asm) add: sin_expansion_lemma) |
|
462 apply (force intro!: DERIV_intros) |
461 apply (erule ssubst) |
463 apply (erule ssubst) |
462 apply (rule_tac x = t in exI, simp) |
464 apply (rule_tac x = t in exI, simp) |
463 apply (rule setsum_cong[OF refl]) |
465 apply (rule setsum_cong[OF refl]) |
464 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
466 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
465 done |
467 done |
472 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
474 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
473 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) |
475 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) |
474 apply safe |
476 apply safe |
475 apply simp |
477 apply simp |
476 apply (simp (no_asm) add: sin_expansion_lemma) |
478 apply (simp (no_asm) add: sin_expansion_lemma) |
|
479 apply (force intro!: DERIV_intros) |
477 apply (erule ssubst) |
480 apply (erule ssubst) |
478 apply (rule_tac x = t in exI, simp) |
481 apply (rule_tac x = t in exI, simp) |
479 apply (rule setsum_cong[OF refl]) |
482 apply (rule setsum_cong[OF refl]) |
480 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
483 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
481 done |
484 done |