author  haftmann 
Sun, 19 Oct 2014 18:05:26 +0200  
changeset 58709  efdc6c533bd3 
parent 58410  6d46ad54a2ab 
child 58889  5b7a9633cfa8 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
27239
diff
changeset

1 
(* Author : Jacques D. Fleuriot 
12224  2 
Copyright : 2001 University of Edinburgh 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

3 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

4 
Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard HÃ¤upler, 2005 
12224  5 
*) 
6 

15944  7 
header{*MacLaurin Series*} 
8 

15131  9 
theory MacLaurin 
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29803
diff
changeset

10 
imports Transcendental 
15131  11 
begin 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

12 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

13 
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

14 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

15 
text{*This is a very long, messy proof even now that it's been broken down 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

16 
into lemmas.*} 
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: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

19 
"0 < h ==> 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

20 
\<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

21 
(B * ((h^n) / real(fact n)))" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

22 
by (rule exI[where x = "(f h  (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(fact n) / (h^n)"]) simp 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

23 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

24 
lemma eq_diff_eq': "(x = y  z) = (y = x + (z::real))" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

25 
by arith 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

26 

32038  27 
lemma fact_diff_Suc [rule_format]: 
28 
"n < Suc m ==> fact (Suc m  n) = (Suc m  n) * fact (m  n)" 

29 
by (subst fact_reduce_nat, auto) 

30 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

31 
lemma Maclaurin_lemma2: 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

32 
fixes B 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

33 
assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

34 
and INIT : "n = Suc k" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

35 
defines "difg \<equiv> (\<lambda>m t. diff m t  ((\<Sum>p<n  m. diff (m + p) 0 / real (fact p) * t ^ p) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

36 
B * (t ^ (n  m) / real (fact (n  m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t  ?difg m t)") 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

37 
shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (difg m) t :> difg (Suc m) t" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

38 
proof (rule allI impI)+ 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

39 
fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

40 
have "DERIV (difg m) t :> diff (Suc m) t  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

41 
((\<Sum>x<n  m. real x * t ^ (x  Suc 0) * diff (m + x) 0 / real (fact x)) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

42 
real (n  m) * t ^ (n  Suc m) * B / real (fact (n  m)))" unfolding difg_def 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

43 
by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2] 
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

44 
simp: real_of_nat_def[symmetric]) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

45 
moreover 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

46 
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

47 
unfolding atLeast0LessThan[symmetric] by auto 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

48 
have "(\<Sum>x<n  m. real x * t ^ (x  Suc 0) * diff (m + x) 0 / real (fact x)) = 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

49 
(\<Sum>x<n  Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

50 
unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

51 
moreover 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

52 
have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

53 
by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

54 
have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) = 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

55 
diff (Suc m + x) 0 * t^x / real (fact x)" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

56 
by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2]) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

57 
moreover 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

58 
have "real (n  m) * t ^ (n  Suc m) * B / real (fact (n  m)) = 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

59 
B * (t ^ (n  Suc m) / real (fact (n  Suc m)))" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

60 
using `0 < n  m` by (simp add: fact_reduce_nat) 
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" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

62 
unfolding difg_def by simp 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

63 
qed 
32038  64 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

65 
lemma Maclaurin: 
29187  66 
assumes h: "0 < h" 
67 
assumes n: "0 < n" 

68 
assumes diff_0: "diff 0 = f" 

69 
assumes diff_Suc: 

70 
"\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t" 

71 
shows 

72 
"\<exists>t. 0 < t & t < h & 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

73 
f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

74 
setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

75 
(diff n t / real (fact n)) * h ^ n" 
29187  76 
proof  
77 
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

78 
by (cases n) (simp add: n) 
29187  79 

80 
obtain B where f_h: "f h = 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

81 
(\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) + 
29187  82 
B * (h ^ n / real (fact n))" 
83 
using Maclaurin_lemma [OF h] .. 

84 

41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

85 
def g \<equiv> "(\<lambda>t. f t  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

86 
(setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n} 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

87 
+ (B * (t^n / real(fact n)))))" 
29187  88 

89 
have g2: "g 0 = 0 & g h = 0" 

57418  90 
by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex) 
29187  91 

41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

92 
def difg \<equiv> "(%m t. diff m t  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

93 
(setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<nm} 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

94 
+ (B * ((t ^ (n  m)) / real (fact (n  m))))))" 
29187  95 

96 
have difg_0: "difg 0 = g" 

97 
unfolding difg_def g_def by (simp add: diff_0) 

98 

99 
have difg_Suc: "\<forall>(m\<Colon>nat) t\<Colon>real. 

100 
m < n \<and> (0\<Colon>real) \<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

101 
using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2) 
29187  102 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

103 
have difg_eq_0: "\<forall>m<n. difg m 0 = 0" 
57418  104 
by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex) 
29187  105 

106 
have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x" 

107 
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp 

108 

109 
have differentiable_difg: 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
51489
diff
changeset

110 
"\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)" 
29187  111 
by (rule differentiableI [OF difg_Suc [rule_format]]) simp 
112 

113 
have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk> 

114 
\<Longrightarrow> difg (Suc m) t = 0" 

115 
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp 

116 

117 
have "m < n" using m by simp 

118 

119 
have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0" 

120 
using `m < n` 

121 
proof (induct m) 

41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

122 
case 0 
29187  123 
show ?case 
124 
proof (rule Rolle) 

125 
show "0 < h" by fact 

126 
show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2) 

127 
show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0\<Colon>nat)) x" 

128 
by (simp add: isCont_difg n) 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
51489
diff
changeset

129 
show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0\<Colon>nat) differentiable (at x)" 
29187  130 
by (simp add: differentiable_difg n) 
131 
qed 

132 
next 

41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

133 
case (Suc m') 
29187  134 
hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp 
135 
then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast 

136 
have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0" 

137 
proof (rule Rolle) 

138 
show "0 < t" by fact 

139 
show "difg (Suc m') 0 = difg (Suc m') t" 

140 
using t `Suc m' < n` by (simp add: difg_Suc_eq_0 difg_eq_0) 

141 
show "\<forall>x. 0 \<le> x \<and> x \<le> t \<longrightarrow> isCont (difg (Suc m')) x" 

142 
using `t < h` `Suc m' < n` by (simp add: isCont_difg) 

56181
2aa0b19e74f3
unify syntax for has_derivative and differentiable
hoelzl
parents:
51489
diff
changeset

143 
show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)" 
29187  144 
using `t < h` `Suc m' < n` by (simp add: differentiable_difg) 
145 
qed 

146 
thus ?case 

147 
using `t < h` by auto 

148 
qed 

149 

150 
then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast 

151 

152 
hence "difg (Suc m) t = 0" 

153 
using `m < n` by (simp add: difg_Suc_eq_0) 

154 

155 
show ?thesis 

156 
proof (intro exI conjI) 

157 
show "0 < t" by fact 

158 
show "t < h" by fact 

159 
show "f h = 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

160 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
29187  161 
diff n t / real (fact n) * h ^ n" 
162 
using `difg (Suc m) t = 0` 

32047  163 
by (simp add: m f_h difg_def del: fact_Suc) 
29187  164 
qed 
165 
qed 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

166 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

167 
lemma Maclaurin_objl: 
25162  168 
"0 < h & n>0 & diff 0 = f & 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

169 
(\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

170 
> (\<exists>t. 0 < t & t < h & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

171 
f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

172 
diff n t / real (fact n) * h ^ n)" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

173 
by (blast intro: Maclaurin) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

174 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

175 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

176 
lemma Maclaurin2: 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

177 
assumes INIT1: "0 < h " and INIT2: "diff 0 = f" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

178 
and DERIV: "\<forall>m t. 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

179 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

180 
shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

181 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

182 
diff n t / real (fact n) * h ^ n" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

183 
proof (cases "n") 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44319
diff
changeset

184 
case 0 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

185 
next 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

186 
case Suc 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

187 
hence "n > 0" by simp 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

188 
from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and> 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

189 
f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

190 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (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

191 
by (rule Maclaurin) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44319
diff
changeset

192 
thus ?thesis by fastforce 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

193 
qed 
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 Maclaurin2_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

196 
"0 < h & diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

197 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

198 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

199 
> (\<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

200 
t \<le> h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

201 
f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

202 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

203 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

204 
by (blast intro: Maclaurin2) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

205 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

206 
lemma Maclaurin_minus: 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

207 
assumes "h < 0" "0 < n" "diff 0 = f" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

208 
and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t" 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

209 
shows "\<exists>t. h < t & t < 0 & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

210 
f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

211 
diff n t / real (fact n) * h ^ n" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

212 
proof  
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

213 
txt "Transform @{text ABL'} into @{text derivative_intros} format." 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

214 
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong] 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

215 
from assms 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

216 
have "\<exists>t>0. t <  h \<and> 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

217 
f ( ( h)) = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

218 
(\<Sum>m<n. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

219 
( 1) ^ m * diff m ( 0) / real (fact m) * ( h) ^ m) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

220 
( 1) ^ n * diff n ( t) / real (fact n) * ( h) ^ n" 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

221 
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV') 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

222 
then guess t .. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

223 
moreover 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

224 
have "( 1) ^ n * diff n ( t) * ( h) ^ n / real (fact n) = diff n ( t) * h ^ n / real (fact n)" 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

225 
by (auto simp add: power_mult_distrib[symmetric]) 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

226 
moreover 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

227 
have "(SUM m<n. ( 1) ^ m * diff m 0 * ( h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))" 
57418  228 
by (auto intro: setsum.cong simp add: 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

229 
ultimately have " h <  t \<and> 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

230 
 t < 0 \<and> 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

231 
f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

232 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n ( t) / real (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

233 
by auto 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

234 
thus ?thesis .. 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

235 
qed 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

236 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

237 
lemma Maclaurin_minus_objl: 
25162  238 
"(h < 0 & n > 0 & diff 0 = f & 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

239 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

240 
m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

241 
> (\<exists>t. h < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

242 
t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

243 
f h = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

244 
(\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

245 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

246 
by (blast intro: Maclaurin_minus) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

247 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

248 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

249 
subsection{*More Convenient "Bidirectional" Version.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

250 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

251 
(* not good for PVS sin_approx, cos_approx *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

252 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

253 
lemma Maclaurin_bi_le_lemma [rule_format]: 
25162  254 
"n>0 \<longrightarrow> 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

255 
diff 0 0 = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

256 
(\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) + 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

257 
diff n 0 * 0 ^ n / real (fact n)" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

258 
by (induct "n") auto 
14738  259 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

260 
lemma Maclaurin_bi_le: 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

261 
assumes "diff 0 = f" 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

262 
and DERIV : "\<forall>m t. m < n & abs t \<le> abs x > DERIV (diff m) t :> diff (Suc m) t" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

263 
shows "\<exists>t. abs t \<le> abs x & 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

264 
f x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

265 
(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

266 
diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t") 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

267 
proof cases 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

268 
assume "n = 0" with `diff 0 = f` 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

269 
next 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

270 
assume "n \<noteq> 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

271 
show ?thesis 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

272 
proof (cases rule: linorder_cases) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

273 
assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV 
56238
5d147e1e18d1
a few new lemmas and generalisations of old ones
paulson <lp15@cam.ac.uk>
parents:
56193
diff
changeset

274 
have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (auto simp add: Maclaurin_bi_le_lemma) 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

275 
thus ?thesis .. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

276 
next 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

277 
assume "x < 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

278 
with `n \<noteq> 0` DERIV 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

279 
have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" by (intro Maclaurin_minus) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

280 
then guess t .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

281 
with `x < 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

282 
thus ?thesis .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

283 
next 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

284 
assume "x > 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

285 
with `n \<noteq> 0` `diff 0 = f` DERIV 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

286 
have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" by (intro Maclaurin) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

287 
then guess t .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

288 
with `x > 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

289 
thus ?thesis .. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

290 
qed 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

291 
qed 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

292 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

293 
lemma Maclaurin_all_lt: 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

294 
assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

295 
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

296 
shows "\<exists>t. 0 < abs t & abs t < abs x & f x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

297 
(\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

298 
(diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t") 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

299 
proof (cases rule: linorder_cases) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

300 
assume "x = 0" with INIT3 show "?thesis".. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

301 
next 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

302 
assume "x < 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

303 
with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" by (intro Maclaurin_minus) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

304 
then guess t .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

305 
with `x < 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

306 
thus ?thesis .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

307 
next 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

308 
assume "x > 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

309 
with assms have "\<exists>t>0. t < x \<and> f x = ?f x t " by (intro Maclaurin) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

310 
then guess t .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

311 
with `x > 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

312 
thus ?thesis .. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

313 
qed 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

314 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

315 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

316 
lemma Maclaurin_all_lt_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

317 
"diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

318 
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) & 
25162  319 
x ~= 0 & n > 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

320 
> (\<exists>t. 0 < abs t & abs t < abs x & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

321 
f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

322 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

323 
by (blast intro: Maclaurin_all_lt) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

324 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

325 
lemma Maclaurin_zero [rule_format]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

326 
"x = (0::real) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

327 
==> n \<noteq> 0 > 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

328 
(\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) = 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

329 
diff 0 0" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

330 
by (induct n, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

331 

41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

332 

74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

333 
lemma Maclaurin_all_le: 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

334 
assumes INIT: "diff 0 = f" 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

335 
and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

336 
shows "\<exists>t. abs t \<le> abs x & f x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

337 
(\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) + 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

338 
(diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t") 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

339 
proof cases 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

340 
assume "n = 0" with INIT 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

341 
next 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

342 
assume "n \<noteq> 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

343 
show ?thesis 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

344 
proof cases 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

345 
assume "x = 0" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

346 
with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

347 
by (intro Maclaurin_zero) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

348 
with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

349 
thus ?thesis .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

350 
next 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

351 
assume "x \<noteq> 0" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

352 
with INIT `n \<noteq> 0` DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

353 
by (intro Maclaurin_all_lt) auto 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

354 
then guess t .. 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

355 
hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

356 
thus ?thesis .. 
41120
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

357 
qed 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

358 
qed 
74e41b2d48ea
adding an Isar version of the MacLaurin theorem from some students' work in 2005
bulwahn
parents:
36974
diff
changeset

359 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

360 
lemma Maclaurin_all_le_objl: "diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

361 
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

362 
> (\<exists>t. abs t \<le> abs x & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

363 
f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

364 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

365 
by (blast intro: Maclaurin_all_le) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

366 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

367 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

368 
subsection{*Version for Exponential Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

369 

25162  370 
lemma Maclaurin_exp_lt: "[ x ~= 0; n > 0 ] 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

371 
==> (\<exists>t. 0 < abs t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

372 
abs t < abs x & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

373 
exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

374 
(exp t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

375 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

376 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

377 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

378 
lemma Maclaurin_exp_le: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

379 
"\<exists>t. abs t \<le> abs x & 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

380 
exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

381 
(exp t / real (fact n)) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

382 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

383 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

384 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

385 
subsection{*Version for Sine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

386 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

387 
lemma mod_exhaust_less_4: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

388 
"m mod 4 = 0  m mod 4 = 1  m mod 4 = 2  m mod 4 = (3::nat)" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

389 
by auto 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

390 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

391 
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

392 
"n\<noteq>0 > Suc (Suc (2 * n  2)) = 2*n" 
15251  393 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

394 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

395 
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

396 
"n\<noteq>0 > Suc (Suc (4*n  2)) = 4*n" 
15251  397 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

398 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

399 
lemma Suc_mult_two_diff_one [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

400 
"n\<noteq>0 > Suc (2 * n  1) = 2*n" 
15251  401 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

402 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

403 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

404 
text{*It is unclear why so many variant results are needed.*} 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

405 

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

406 
lemma sin_expansion_lemma: 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

407 
"sin (x + real (Suc m) * pi / 2) = 
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

408 
cos (x + real (m) * pi / 2)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44890
diff
changeset

409 
by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib distrib_right, auto) 
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

410 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

411 
lemma Maclaurin_sin_expansion2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

412 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

413 
sin x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

414 
(\<Sum>m<n. sin_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

415 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

416 
apply (cut_tac f = sin and n = n and x = x 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

417 
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

418 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

419 
apply (simp (no_asm)) 
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

420 
apply (simp (no_asm) add: sin_expansion_lemma) 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

421 
apply (force intro!: derivative_eq_intros) 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
57418
diff
changeset

422 
apply (subst (asm) setsum.neutral, auto)[1] 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

423 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

424 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

425 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

426 
apply (rule_tac x = t in exI, simp) 
57418  427 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

428 
apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

429 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

430 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

431 
lemma Maclaurin_sin_expansion: 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

432 
"\<exists>t. sin x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

433 
(\<Sum>m<n. sin_coeff m * x ^ m) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

434 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
41166
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

435 
apply (insert Maclaurin_sin_expansion2 [of x n]) 
4b2a457b17e8
beautify MacLaurin proofs; make better use of DERIV_intros
hoelzl
parents:
41120
diff
changeset

436 
apply (blast intro: elim:) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

437 
done 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

438 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

439 
lemma Maclaurin_sin_expansion3: 
25162  440 
"[ n > 0; 0 < x ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

441 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

442 
sin x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

443 
(\<Sum>m<n. sin_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

444 
+ ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

445 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

446 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

447 
apply simp 
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

448 
apply (simp (no_asm) add: sin_expansion_lemma) 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

449 
apply (force intro!: derivative_eq_intros) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

450 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

451 
apply (rule_tac x = t in exI, simp) 
57418  452 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

453 
apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

454 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

455 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

456 
lemma Maclaurin_sin_expansion4: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

457 
"0 < x ==> 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

458 
\<exists>t. 0 < t & t \<le> x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

459 
sin x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

460 
(\<Sum>m<n. sin_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

461 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

462 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

463 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

464 
apply simp 
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

465 
apply (simp (no_asm) add: sin_expansion_lemma) 
56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

466 
apply (force intro!: derivative_eq_intros) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

467 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

468 
apply (rule_tac x = t in exI, simp) 
57418  469 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

470 
apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

471 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

472 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

473 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

474 
subsection{*Maclaurin Expansion for Cosine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

475 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

476 
lemma sumr_cos_zero_one [simp]: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

477 
"(\<Sum>m<(Suc n). cos_coeff m * 0 ^ m) = 1" 
15251  478 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

479 

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

480 
lemma cos_expansion_lemma: 
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

481 
"cos (x + real(Suc m) * pi / 2) = sin (x + real m * pi / 2)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44890
diff
changeset

482 
by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto) 
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

483 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

484 
lemma Maclaurin_cos_expansion: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

485 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

486 
cos x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

487 
(\<Sum>m<n. cos_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

488 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

489 
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

490 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

491 
apply (simp (no_asm)) 
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

492 
apply (simp (no_asm) add: cos_expansion_lemma) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

493 
apply (case_tac "n", simp) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

494 
apply (simp del: setsum_lessThan_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

495 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

496 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

497 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

498 
apply (rule_tac x = t in exI, simp) 
57418  499 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

500 
apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

501 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

502 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

503 
lemma Maclaurin_cos_expansion2: 
25162  504 
"[ 0 < x; n > 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

505 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

506 
cos x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

507 
(\<Sum>m<n. cos_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

508 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

509 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

510 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

511 
apply simp 
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

512 
apply (simp (no_asm) add: cos_expansion_lemma) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

513 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

514 
apply (rule_tac x = t in exI, simp) 
57418  515 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

516 
apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

517 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

518 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

519 
lemma Maclaurin_minus_cos_expansion: 
25162  520 
"[ x < 0; n > 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

521 
\<exists>t. x < t & t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

522 
cos x = 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

523 
(\<Sum>m<n. cos_coeff m * x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

524 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

525 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

526 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

527 
apply simp 
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

528 
apply (simp (no_asm) add: cos_expansion_lemma) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

529 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

530 
apply (rule_tac x = t in exI, simp) 
57418  531 
apply (rule setsum.cong[OF refl]) 
58709
efdc6c533bd3
prefer generic elimination rules for even/odd over specialized unfold rules for nat
haftmann
parents:
58410
diff
changeset

532 
apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

533 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

534 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

535 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

536 
(* Version for ln(1 +/ x). Where is it?? *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

537 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

538 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

539 
lemma sin_bound_lemma: 
15081  540 
"[x = y; abs u \<le> (v::real) ] ==> \<bar>(x + u)  y\<bar> \<le> v" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

541 
by auto 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

542 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

543 
lemma Maclaurin_sin_bound: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

544 
"abs(sin x  (\<Sum>m<n. sin_coeff m * x ^ m)) 
44306
33572a766836
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
huffman
parents:
41166
diff
changeset

545 
\<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n" 
14738  546 
proof  
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

547 
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" 
14738  548 
by (rule_tac mult_right_mono,simp_all) 
549 
note est = this[simplified] 

22985  550 
let ?diff = "\<lambda>(n::nat) x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then sin(x) else cos(x)" 
551 
have diff_0: "?diff 0 = sin" by simp 

552 
have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x" 

553 
apply (clarify) 

554 
apply (subst (1 2 3) mod_Suc_eq_Suc_mod) 

555 
apply (cut_tac m=m in mod_exhaust_less_4) 

56381
0556204bc230
merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents:
56238
diff
changeset

556 
apply (safe, auto intro!: derivative_eq_intros) 
22985  557 
done 
558 
from Maclaurin_all_le [OF diff_0 DERIV_diff] 

559 
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56181
diff
changeset

560 
t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) + 
22985  561 
?diff n t / real (fact n) * x ^ n" by fast 
562 
have diff_m_0: 

563 
"\<And>m. ?diff m 0 = (if even m then 0 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
57514
diff
changeset

564 
else ( 1) ^ ((m  Suc 0) div 2))" 
22985  565 
apply (subst even_even_mod_4_iff) 
566 
apply (cut_tac m=m in mod_exhaust_less_4) 

567 
apply (elim disjE, simp_all) 

568 
apply (safe dest!: mod_eqD, simp_all) 

569 
done 

14738  570 
show ?thesis 
44306
33572a766836
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
huffman
parents:
41166
diff
changeset

571 
unfolding sin_coeff_def 
22985  572 
apply (subst t2) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

573 
apply (rule sin_bound_lemma) 
57418  574 
apply (rule setsum.cong[OF refl]) 
22985  575 
apply (subst diff_m_0, simp) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

576 
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57492
diff
changeset

577 
simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult) 
14738  578 
done 
579 
qed 

580 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

581 
end 