src/HOL/MacLaurin.thy
author wenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70067 9b34dbeb1103
parent 69529 4ab9657b3257
child 70817 dd675800469d
permissions -rw-r--r--
auxiliary operation for common uses of 'compile_generated_files';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
     1
(*  Title:      HOL/MacLaurin.thy
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
     2
    Author:     Jacques D. Fleuriot, 2001 University of Edinburgh
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
     3
    Author:     Lawrence C Paulson, 2004
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
     4
    Author:     Lukas Bulwahn and Bernhard Häupler, 2005
12224
02df7cbe7d25 even more theories from Jacques
paulson
parents:
diff changeset
     5
*)
02df7cbe7d25 even more theories from Jacques
paulson
parents:
diff changeset
     6
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
     7
section \<open>MacLaurin and Taylor Series\<close>
15944
9b00875e21f7 from simplesubst to new subst
paulson
parents: 15561
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15081
diff changeset
     9
theory MacLaurin
29811
026b0f9f579f fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieb-laptop
parents: 29803
diff changeset
    10
imports Transcendental
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15081
diff changeset
    11
begin
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    12
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    13
subsection \<open>Maclaurin's Theorem with Lagrange Form of Remainder\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    14
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    15
text \<open>This is a very long, messy proof even now that it's been broken down
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    16
  into lemmas.\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    17
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    18
lemma Maclaurin_lemma:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    19
  "0 < h \<Longrightarrow>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    20
    \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) + (B * ((h^n) /(fact n)))"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    21
  by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    22
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    23
lemma eq_diff_eq': "x = y - z \<longleftrightarrow> y = x + z"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    24
  for x y z :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    25
  by arith
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    26
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    27
lemma fact_diff_Suc: "n < Suc m \<Longrightarrow> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    28
  by (subst fact_reduce) auto
32038
4127b89f48ab Repaired uses of factorial.
avigad
parents: 31882
diff changeset
    29
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    30
lemma Maclaurin_lemma2:
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    31
  fixes B
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    32
  assumes DERIV: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    33
    and INIT: "n = Suc k"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61284
diff changeset
    34
  defines "difg \<equiv>
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    35
    (\<lambda>m t::real. diff m t -
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    36
      ((\<Sum>p<n - m. diff (m + p) 0 / fact p * t ^ p) + B * (t ^ (n - m) / fact (n - m))))"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    37
    (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    38
  shows "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    39
proof (rule allI impI)+
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    40
  fix m t
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    41
  assume INIT2: "m < n \<and> 0 \<le> t \<and> t \<le> h"
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    42
  have "DERIV (difg m) t :> diff (Suc m) t -
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    43
    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) +
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    44
     real (n - m) * t ^ (n - Suc m) * B / fact (n - m))"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    45
    by (auto simp: difg_def intro!: derivative_eq_intros DERIV[rule_format, OF INIT2])
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    46
  moreover
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    47
  from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    48
    unfolding atLeast0LessThan[symmetric] by auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    49
  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) =
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    50
      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x))"
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
    51
    unfolding intvl by (subst sum.insert) (auto simp: sum.reindex)
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    52
  moreover
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
    53
  have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    54
    by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    55
        less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    56
  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
    57
    by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    58
  moreover
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    59
  have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    60
    using \<open>0 < n - m\<close> by (simp add: divide_simps fact_reduce)
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    61
  ultimately show "DERIV (difg m) t :> difg (Suc m) t"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 61284
diff changeset
    62
    unfolding difg_def  by (simp add: mult.commute)
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
    63
qed
32038
4127b89f48ab Repaired uses of factorial.
avigad
parents: 31882
diff changeset
    64
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
    65
lemma Maclaurin:
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    66
  assumes h: "0 < h"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    67
    and n: "0 < n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    68
    and diff_0: "diff 0 = f"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    69
    and diff_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    70
  shows
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    71
    "\<exists>t::real. 0 < t \<and> t < h \<and>
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
    72
      f h = sum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n"
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    73
proof -
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    74
  from n obtain m where m: "n = Suc m"
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
    75
    by (cases n) (simp add: n)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    76
  from m have "m < n" by simp
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    77
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    78
  obtain B where f_h: "f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + B * (h ^ n / fact n)"
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    79
    using Maclaurin_lemma [OF h] ..
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    80
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 61954
diff changeset
    81
  define g where [abs_def]: "g t =
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
    82
    f t - (sum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    83
  have g2: "g 0 = 0" "g h = 0"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
    84
    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex)
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    85
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 61954
diff changeset
    86
  define difg where [abs_def]: "difg m t =
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
    87
    diff m t - (sum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} +
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    88
      B * ((t ^ (n - m)) / fact (n - m)))" for m t
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    89
  have difg_0: "difg 0 = g"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    90
    by (simp add: difg_def g_def diff_0)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    91
  have difg_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 61954
diff changeset
    92
    using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    93
  have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
    94
    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    95
  have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x"
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
    96
    by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    97
  have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)"
69022
e2858770997a removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents: 69020
diff changeset
    98
    using difg_Suc real_differentiable_def by auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
    99
  have difg_Suc_eq_0:
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   100
    "\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0"
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   101
    by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   102
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   103
  have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   104
  using \<open>m < n\<close>
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   105
  proof (induct m)
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   106
    case 0
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   107
    show ?case
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   108
    proof (rule Rolle)
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   109
      show "0 < h" by fact
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   110
      show "difg 0 0 = difg 0 h"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   111
        by (simp add: difg_0 g2)
69020
4f94e262976d elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents: 68671
diff changeset
   112
      show "continuous_on {0..h} (difg 0)"
4f94e262976d elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents: 68671
diff changeset
   113
        by (simp add: continuous_at_imp_continuous_on isCont_difg n)
69022
e2858770997a removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents: 69020
diff changeset
   114
    qed (simp add: differentiable_difg n)
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   115
  next
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   116
    case (Suc m')
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   117
    then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   118
      by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   119
    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   120
      by fast
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   121
    have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   122
    proof (rule Rolle)
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   123
      show "0 < t" by fact
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   124
      show "difg (Suc m') 0 = difg (Suc m') t"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   125
        using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0)
69020
4f94e262976d elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents: 68671
diff changeset
   126
      have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   127
        using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg)
69020
4f94e262976d elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents: 68671
diff changeset
   128
      then show "continuous_on {0..t} (difg (Suc m'))"
4f94e262976d elimination of near duplication involving Rolle's theorem and the MVT
paulson <lp15@cam.ac.uk>
parents: 68671
diff changeset
   129
        by (simp add: continuous_at_imp_continuous_on)
69022
e2858770997a removal of more redundancies, and fixes
paulson <lp15@cam.ac.uk>
parents: 69020
diff changeset
   130
    qed (use \<open>t < h\<close> \<open>Suc m' < n\<close> in \<open>simp add: differentiable_difg\<close>)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   131
    with \<open>t < h\<close> show ?case
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   132
      by auto
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   133
  qed
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   134
  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   135
    by fast
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   136
  with \<open>m < n\<close> have "difg (Suc m) t = 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   137
    by (simp add: difg_Suc_eq_0)
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   138
  show ?thesis
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   139
  proof (intro exI conjI)
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   140
    show "0 < t" by fact
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   141
    show "t < h" by fact
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   142
    show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   143
      using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def)
29187
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   144
  qed
7b09385234f9 clean up proofs of lemma Maclaurin
huffman
parents: 29168
diff changeset
   145
qed
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   146
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   147
lemma Maclaurin2:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   148
  fixes n :: nat
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   149
    and h :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   150
  assumes INIT1: "0 < h"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   151
    and INIT2: "diff 0 = f"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   152
    and DERIV: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   153
  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   154
proof (cases n)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   155
  case 0
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   156
  with INIT1 INIT2 show ?thesis by fastforce
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   157
next
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   158
  case Suc
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   159
  then have "n > 0" by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   160
  from INIT1 this INIT2 DERIV
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   161
  have "\<exists>t>0. t < h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   162
    by (rule Maclaurin)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   163
  then show ?thesis by fastforce
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   164
qed
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   165
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   166
lemma Maclaurin_minus:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   167
  fixes n :: nat and h :: real
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   168
  assumes "h < 0" "0 < n" "diff 0 = f"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   169
    and DERIV: "\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   170
  shows "\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   171
proof -
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   172
  txt \<open>Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format.\<close>
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   173
  note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   174
  let ?sum = "\<lambda>t.
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   175
    (\<Sum>m<n. (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   176
    (- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   177
  from assms have "\<exists>t>0. t < - h \<and> f (- (- h)) = ?sum t"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56238
diff changeset
   178
    by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   179
  then obtain t where "0 < t" "t < - h" "f (- (- h)) = ?sum t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   180
    by blast
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   181
  moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   182
    by (auto simp: power_mult_distrib[symmetric])
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   183
  moreover
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   184
    have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / fact m) = (\<Sum>m<n. diff m 0 * h ^ m / fact m)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
   185
    by (auto intro: sum.cong simp add: power_mult_distrib[symmetric])
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   186
  ultimately have "h < - t \<and> - t < 0 \<and>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   187
    f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   188
    by auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   189
  then show ?thesis ..
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   190
qed
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   191
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   192
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   193
subsection \<open>More Convenient "Bidirectional" Version.\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   194
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   195
lemma Maclaurin_bi_le:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   196
  fixes n :: nat and x :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   197
  assumes "diff 0 = f"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   198
    and DERIV : "\<forall>m t. m < n \<and> \<bar>t\<bar> \<le> \<bar>x\<bar> \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   199
  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) + diff n t / (fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   200
    (is "\<exists>t. _ \<and> f x = ?f x t")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   201
proof (cases "n = 0")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   202
  case True
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   203
  with \<open>diff 0 = f\<close> show ?thesis by force
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   204
next
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   205
  case False
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   206
  show ?thesis
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   207
  proof (cases rule: linorder_cases)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   208
    assume "x = 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   209
    with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   210
      by auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   211
    then show ?thesis ..
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   212
  next
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   213
    assume "x < 0"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   214
    with \<open>n \<noteq> 0\<close> DERIV have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   215
      by (intro Maclaurin_minus) auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   216
    then obtain t where "x < t" "t < 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   217
      "diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   218
      by blast
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   219
    with \<open>x < 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   220
      by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   221
    then show ?thesis ..
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   222
  next
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   223
    assume "x > 0"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   224
    with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   225
      by (intro Maclaurin) auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   226
    then obtain t where "0 < t" "t < x"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   227
      "diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   228
      by blast
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   229
    with \<open>x > 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   230
    then show ?thesis ..
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   231
  qed
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   232
qed
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   233
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   234
lemma Maclaurin_all_lt:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   235
  fixes x :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   236
  assumes INIT1: "diff 0 = f"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   237
    and INIT2: "0 < n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   238
    and INIT3: "x \<noteq> 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   239
    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   240
  shows "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x =
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   241
      (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   242
    (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   243
proof (cases rule: linorder_cases)
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   244
  assume "x = 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   245
  with INIT3 show ?thesis ..
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   246
next
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   247
  assume "x < 0"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   248
  with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   249
    by (intro Maclaurin_minus) auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   250
  then obtain t where "t > x" "t < 0" "f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   251
    by blast
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   252
  with \<open>x < 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   253
    by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   254
  then show ?thesis ..
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   255
next
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   256
  assume "x > 0"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   257
  with assms have "\<exists>t>0. t < x \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   258
    by (intro Maclaurin) auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   259
  then obtain t where "t > 0" "t < x" "f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   260
    by blast
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   261
  with \<open>x > 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   262
    by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   263
  then show ?thesis ..
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   264
qed
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   265
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   266
lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   267
  for x :: real and n :: nat
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   268
  by simp
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   269
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   270
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   271
lemma Maclaurin_all_le:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   272
  fixes x :: real and n :: nat
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   273
  assumes INIT: "diff 0 = f"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   274
    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   275
  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   276
    (is "\<exists>t. _ \<and> f x = ?f x t")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   277
proof (cases "n = 0")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   278
  case True
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   279
  with INIT show ?thesis by force
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   280
next
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   281
  case False
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   282
  show ?thesis
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   283
  proof (cases "x = 0")
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   284
    case True
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   285
    with \<open>n \<noteq> 0\<close> have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   286
      by (intro Maclaurin_zero) auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   287
    with INIT \<open>x = 0\<close> \<open>n \<noteq> 0\<close> have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   288
      by force
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   289
    then show ?thesis ..
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   290
  next
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   291
    case False
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60017
diff changeset
   292
    with INIT \<open>n \<noteq> 0\<close> DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
41166
4b2a457b17e8 beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents: 41120
diff changeset
   293
      by (intro Maclaurin_all_lt) auto
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   294
    then obtain t where "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" ..
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   295
    then have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   296
      by simp
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   297
    then show ?thesis ..
41120
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   298
  qed
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   299
qed
74e41b2d48ea adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents: 36974
diff changeset
   300
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   301
lemma Maclaurin_all_le_objl:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   302
  "diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<longrightarrow>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   303
    (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n)"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   304
  for x :: real and n :: nat
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   305
  by (blast intro: Maclaurin_all_le)
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   306
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   307
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   308
subsection \<open>Version for Exponential Function\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   309
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   310
lemma Maclaurin_exp_lt:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   311
  fixes x :: real and n :: nat
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   312
  shows
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   313
    "x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   314
      (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n)"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   315
 using Maclaurin_all_lt [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   316
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   317
lemma Maclaurin_exp_le:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   318
  fixes x :: real and n :: nat
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   319
  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   320
  using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   321
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   322
corollary exp_lower_Taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   323
  for x :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   324
  using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   325
65273
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   326
corollary ln_2_less_1: "ln 2 < (1::real)"
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   327
proof -
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   328
  have "2 < 5/(2::real)" by simp
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   329
  also have "5/2 \<le> exp (1::real)" using exp_lower_Taylor_quadratic[of 1, simplified] by simp
65273
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   330
  finally have "exp (ln 2) < exp (1::real)" by simp
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   331
  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
917ae0ba03a2 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   332
qed
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   333
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   334
subsection \<open>Version for Sine Function\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   335
67091
1393c2340eec more symbols;
wenzelm
parents: 65273
diff changeset
   336
lemma mod_exhaust_less_4: "m mod 4 = 0 \<or> m mod 4 = 1 \<or> m mod 4 = 2 \<or> m mod 4 = 3"
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   337
  for m :: nat
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   338
  by auto
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   339
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   340
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   341
text \<open>It is unclear why so many variant results are needed.\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   342
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   343
lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   344
  by (auto simp: cos_add sin_add add_divide_distrib distrib_right)
36974
b877866b5b00 remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
huffman
parents: 32047
diff changeset
   345
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   346
lemma Maclaurin_sin_expansion2:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   347
  "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   348
    sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   349
proof (cases "n = 0 \<or> x = 0")
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   350
  case False
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   351
  let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   352
  have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> sin x =
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   353
      (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   354
  proof (rule Maclaurin_all_lt)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   355
    show "\<forall>m x. ((\<lambda>t. sin (t + 1/2 * real m * pi)) has_real_derivative
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   356
           sin (x + 1/2 * real (Suc m) * pi)) (at x)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   357
      by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   358
  qed (use False in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   359
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   360
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   361
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   362
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   363
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   364
qed auto
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   365
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   366
lemma Maclaurin_sin_expansion:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   367
  "\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   368
  using Maclaurin_sin_expansion2 [of x n] by blast
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   369
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   370
lemma Maclaurin_sin_expansion3:
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   371
  assumes "n > 0" "x > 0"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   372
    shows "\<exists>t. 0 < t \<and> t < x \<and>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   373
          sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   374
proof -
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   375
  let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   376
  have "\<exists>t. 0 < t \<and> t < x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   377
  proof (rule Maclaurin)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   378
    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   379
                ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   380
                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   381
      apply (simp add: sin_expansion_lemma del: of_nat_Suc)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   382
      apply (force intro!: derivative_eq_intros)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   383
      done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   384
  qed (use assms in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   385
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   386
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   387
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   388
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   389
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   390
qed
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   391
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   392
lemma Maclaurin_sin_expansion4:
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   393
  assumes "0 < x"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   394
  shows "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   395
proof -
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   396
  let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   397
  have "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   398
  proof (rule Maclaurin2)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   399
    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   400
                ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   401
                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   402
      apply (simp add: sin_expansion_lemma del: of_nat_Suc)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   403
      apply (force intro!: derivative_eq_intros)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   404
      done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   405
  qed (use assms in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   406
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   407
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   408
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   409
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   410
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   411
qed
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   412
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   413
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   414
subsection \<open>Maclaurin Expansion for Cosine Function\<close>
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   415
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   416
lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   417
  by (induct n) auto
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   418
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   419
lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   420
  by (auto simp: cos_add sin_add distrib_right add_divide_distrib)
36974
b877866b5b00 remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
huffman
parents: 32047
diff changeset
   421
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   422
lemma Maclaurin_cos_expansion:
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   423
  "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   424
    cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   425
proof (cases "n = 0 \<or> x = 0")
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   426
  case False
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   427
  let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   428
  have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> cos x =
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   429
      (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   430
  proof (rule Maclaurin_all_lt)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   431
    show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   432
           cos (x + 1/2 * real (Suc m) * pi)) (at x)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   433
      apply (rule allI derivative_eq_intros | simp)+
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   434
      using cos_expansion_lemma by force
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   435
  qed (use False in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   436
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   437
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   438
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   439
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   440
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   441
qed auto
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   442
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   443
lemma Maclaurin_cos_expansion2:
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   444
  assumes "x > 0" "n > 0"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   445
  shows "\<exists>t. 0 < t \<and> t < x \<and>
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   446
      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n"
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   447
proof -
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   448
  let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   449
  have "\<exists>t. 0 < t \<and> t < x \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   450
  proof (rule Maclaurin)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   451
    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   452
              ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative 
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   453
               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   454
      by (simp add: cos_expansion_lemma del: of_nat_Suc)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   455
  qed (use assms in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   456
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   457
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   458
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   459
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   460
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   461
qed
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   462
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   463
lemma Maclaurin_minus_cos_expansion:
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   464
  assumes "n > 0" "x < 0"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   465
  shows "\<exists>t. x < t \<and> t < 0 \<and>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   466
         cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   467
proof -
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   468
  let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   469
  have "\<exists>t. x < t \<and> t < 0 \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   470
  proof (rule Maclaurin_minus)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   471
    show "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow>
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   472
              ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative 
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   473
               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   474
      by (simp add: cos_expansion_lemma del: of_nat_Suc)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   475
  qed (use assms in auto)
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   476
  then show ?thesis
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   477
    apply (rule ex_forward, simp)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   478
    apply (rule sum.cong[OF refl])
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   479
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
68669
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   480
    done
7ddf297cfcde de-applying and removing junk
paulson <lp15@cam.ac.uk>
parents: 68157
diff changeset
   481
qed
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   482
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   483
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   484
(* Version for ln(1 +/- x). Where is it?? *)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   485
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   486
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   487
lemma sin_bound_lemma: "x = y \<Longrightarrow> \<bar>u\<bar> \<le> v \<Longrightarrow> \<bar>(x + u) - y\<bar> \<le> v"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   488
  for x y u v :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   489
  by auto
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   490
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   491
lemma Maclaurin_sin_bound: "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse (fact n) * \<bar>x\<bar> ^ n"
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 12224
diff changeset
   492
proof -
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   493
  have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   494
    by (rule mult_right_mono) simp_all
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   495
  let ?diff = "\<lambda>(n::nat) (x::real).
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   496
    if n mod 4 = 0 then sin x
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   497
    else if n mod 4 = 1 then cos x
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   498
    else if n mod 4 = 2 then - sin x
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   499
    else - cos x"
22985
501e6dfe4e5a cleaned up proof of Maclaurin_sin_bound
huffman
parents: 22983
diff changeset
   500
  have diff_0: "?diff 0 = sin" by simp
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   501
  have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   502
    using mod_exhaust_less_4 [of m]
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   503
    by (auto simp: mod_Suc intro!: derivative_eq_intros)
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   504
  then have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   505
    by blast
22985
501e6dfe4e5a cleaned up proof of Maclaurin_sin_bound
huffman
parents: 22983
diff changeset
   506
  from Maclaurin_all_le [OF diff_0 DERIV_diff]
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   507
  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   508
    and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n"
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   509
    by fast
68157
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   510
  have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m
057d5b4ce47e removed some non-essential rules
haftmann
parents: 67091
diff changeset
   511
    using mod_exhaust_less_4 [of m]
68671
205749fba102 fixing a theorem statement, etc.
paulson <lp15@cam.ac.uk>
parents: 68669
diff changeset
   512
    by (auto simp: minus_one_power_iff even_even_mod_4_iff [of m] dest: even_mod_4_div_2 odd_mod_4_div_2)
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 12224
diff changeset
   513
  show ?thesis
44306
33572a766836 fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
huffman
parents: 41166
diff changeset
   514
    unfolding sin_coeff_def
22985
501e6dfe4e5a cleaned up proof of Maclaurin_sin_bound
huffman
parents: 22983
diff changeset
   515
    apply (subst t2)
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   516
    apply (rule sin_bound_lemma)
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63570
diff changeset
   517
     apply (rule sum.cong[OF refl])
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   518
     apply (subst diff_m_0, simp)
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   519
    using est
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   520
    apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
63569
7e0b0db5e9ac misc tuning and modernization;
wenzelm
parents: 63365
diff changeset
   521
        simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 12224
diff changeset
   522
    done
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 12224
diff changeset
   523
qed
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 12224
diff changeset
   524
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   525
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   526
section \<open>Taylor series\<close>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   527
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   528
text \<open>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   529
  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   530
  to prove Taylor's theorem.
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   531
\<close>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   532
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   533
lemma Taylor_up:
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   534
  assumes INIT: "n > 0" "diff 0 = f"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   535
    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   536
    and INTERV: "a \<le> c" "c < b"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   537
  shows "\<exists>t::real. c < t \<and> t < b \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   538
    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   539
proof -
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   540
  from INTERV have "0 < b - c" by arith
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   541
  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   542
    by auto
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   543
  moreover
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   544
  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   545
  proof (intro strip)
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   546
    fix m t
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   547
    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   548
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   549
      by auto
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   550
    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   551
      by (rule DERIV_add)
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   552
    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   553
      by (rule DERIV_chain2)
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   554
    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   555
      by simp
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   556
  qed
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   557
  ultimately obtain x where
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   558
    "0 < x \<and> x < b - c \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   559
      f (b - c + c) =
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   560
        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   561
     by (rule Maclaurin [THEN exE])
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   562
   then have "c < x + c \<and> x + c < b \<and> f b =
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   563
     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   564
    by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   565
  then show ?thesis by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   566
qed
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   567
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   568
lemma Taylor_down:
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   569
  fixes a :: real and n :: nat
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   570
  assumes INIT: "n > 0" "diff 0 = f"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   571
    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   572
    and INTERV: "a < c" "c \<le> b"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   573
  shows "\<exists>t. a < t \<and> t < c \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   574
    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   575
proof -
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   576
  from INTERV have "a-c < 0" by arith
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   577
  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   578
    by auto
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   579
  moreover
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   580
  have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   581
  proof (rule allI impI)+
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   582
    fix m t
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   583
    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   584
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   585
      by auto
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   586
    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   587
      by (rule DERIV_add)
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   588
    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   589
      by (rule DERIV_chain2)
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   590
    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   591
      by simp
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   592
  qed
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   593
  ultimately obtain x where
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   594
    "a - c < x \<and> x < 0 \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   595
      f (a - c + c) =
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   596
        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   597
    by (rule Maclaurin_minus [THEN exE])
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   598
  then have "a < x + c \<and> x + c < c \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   599
    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   600
    by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   601
  then show ?thesis by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   602
qed
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   603
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   604
theorem Taylor:
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   605
  fixes a :: real and n :: nat
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   606
  assumes INIT: "n > 0" "diff 0 = f"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   607
    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   608
    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   609
  shows "\<exists>t.
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   610
    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   611
    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   612
proof (cases "x < c")
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   613
  case True
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   614
  note INIT
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   615
  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   616
    using DERIV and INTERV by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   617
  moreover note True
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   618
  moreover from INTERV have "c \<le> b"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   619
    by simp
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   620
  ultimately have "\<exists>t>x. t < c \<and> f x =
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   621
    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   622
    by (rule Taylor_down)
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   623
  with True show ?thesis by simp
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   624
next
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   625
  case False
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   626
  note INIT
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   627
  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   628
    using DERIV and INTERV by fastforce
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   629
  moreover from INTERV have "a \<le> c"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   630
    by arith
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   631
  moreover from False and INTERV have "c < x"
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   632
    by arith
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   633
  ultimately have "\<exists>t>c. t < x \<and> f x =
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   634
    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69022
diff changeset
   635
    by (rule Taylor_up)
63570
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   636
  with False show ?thesis by simp
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   637
qed
1826a90b9cbc simplified theory structure;
wenzelm
parents: 63569
diff changeset
   638
15079
2ef899e4526d conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents: 14738
diff changeset
   639
end