author  huffman 
Tue, 12 Dec 2006 04:37:25 +0100  
changeset 21784  e76faa6e65fd 
parent 21404  eb85850d3eb7 
child 21785  885667874dfc 
permissions  rwrr 
21164  1 
(* Title : Deriv.thy 
2 
ID : $Id$ 

3 
Author : Jacques D. Fleuriot 

4 
Copyright : 1998 University of Cambridge 

5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 

6 
GMVT by Benjamin Porter, 2005 

7 
*) 

8 

9 
header{* Differentiation *} 

10 

11 
theory Deriv 

12 
imports Lim 

13 
begin 

14 

15 
text{*Standard and Nonstandard Definitions*} 

16 

17 
definition 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

18 
deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" 
21164  19 
{*Differentiation: D is derivative of function f at x*} 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

20 
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

21 
"DERIV f x :> D = ((%h. (f(x + h)  f x) / h)  0 > D)" 
21164  22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

23 
definition 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

24 
nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

25 
("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where 
21164  26 
"NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal  {0}. 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

27 
(( *f* f)(star_of x + h) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

28 
 star_of (f x))/h @= star_of D)" 
21164  29 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

30 
definition 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

31 
differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

32 
(infixl "differentiable" 60) where 
21164  33 
"f differentiable x = (\<exists>D. DERIV f x :> D)" 
34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

35 
definition 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

36 
NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

37 
(infixl "NSdifferentiable" 60) where 
21164  38 
"f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)" 
39 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

40 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21239
diff
changeset

41 
increment :: "[real=>real,real,hypreal] => hypreal" where 
21164  42 
"increment f x h = (@inc. f NSdifferentiable x & 
43 
inc = ( *f* f)(hypreal_of_real x + h)  hypreal_of_real (f x))" 

44 

45 

46 
consts 

47 
Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" 

48 
primrec 

49 
"Bolzano_bisect P a b 0 = (a,b)" 

50 
"Bolzano_bisect P a b (Suc n) = 

51 
(let (x,y) = Bolzano_bisect P a b n 

52 
in if P(x, (x+y)/2) then ((x+y)/2, y) 

53 
else (x, (x+y)/2))" 

54 

55 

56 
subsection {* Derivatives *} 

57 

58 
subsubsection {* Purely standard proofs *} 

59 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

60 
lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 > D)" 
21164  61 
by (simp add: deriv_def) 
62 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

63 
lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h)  f(x))/h)  0 > D" 
21164  64 
by (simp add: deriv_def) 
65 

66 
lemma DERIV_const [simp]: "DERIV (\<lambda>x. k) x :> 0" 

67 
by (simp add: deriv_def) 

68 

69 
lemma DERIV_Id [simp]: "DERIV (\<lambda>x. x) x :> 1" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

70 
by (simp add: deriv_def divide_self cong: LIM_cong) 
21164  71 

72 
lemma add_diff_add: 

73 
fixes a b c d :: "'a::ab_group_add" 

74 
shows "(a + c)  (b + d) = (a  b) + (c  d)" 

75 
by simp 

76 

77 
lemma DERIV_add: 

78 
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

79 
by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add) 
21164  80 

81 
lemma DERIV_minus: 

82 
"DERIV f x :> D \<Longrightarrow> DERIV (\<lambda>x.  f x) x :>  D" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

83 
by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus) 
21164  84 

85 
lemma DERIV_diff: 

86 
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x  g x) x :> D  E" 

87 
by (simp only: diff_def DERIV_add DERIV_minus) 

88 

89 
lemma DERIV_add_minus: 

90 
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x +  g x) x :> D +  E" 

91 
by (simp only: DERIV_add DERIV_minus) 

92 

93 
lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x" 

94 
proof (unfold isCont_iff) 

95 
assume "DERIV f x :> D" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

96 
hence "(\<lambda>h. (f(x+h)  f(x)) / h)  0 > D" 
21164  97 
by (rule DERIV_D) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

98 
hence "(\<lambda>h. (f(x+h)  f(x)) / h * h)  0 > D * 0" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

99 
by (intro LIM_mult LIM_self) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

100 
hence "(\<lambda>h. (f(x+h)  f(x)) * (h / h))  0 > 0" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

101 
by simp 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

102 
hence "(\<lambda>h. f(x+h)  f(x))  0 > 0" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

103 
by (simp cong: LIM_cong add: divide_self) 
21164  104 
thus "(\<lambda>h. f(x+h))  0 > f(x)" 
105 
by (simp add: LIM_def) 

106 
qed 

107 

108 
lemma DERIV_mult_lemma: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

109 
fixes a b c d :: "'a::real_field" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

110 
shows "(a * b  c * d) / h = a * ((b  d) / h) + ((a  c) / h) * d" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

111 
by (simp add: diff_minus add_divide_distrib [symmetric] ring_distrib) 
21164  112 

113 
lemma DERIV_mult': 

114 
assumes f: "DERIV f x :> D" 

115 
assumes g: "DERIV g x :> E" 

116 
shows "DERIV (\<lambda>x. f x * g x) x :> f x * E + D * g x" 

117 
proof (unfold deriv_def) 

118 
from f have "isCont f x" 

119 
by (rule DERIV_isCont) 

120 
hence "(\<lambda>h. f(x+h))  0 > f x" 

121 
by (simp only: isCont_iff) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

122 
hence "(\<lambda>h. f(x+h) * ((g(x+h)  g x) / h) + 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

123 
((f(x+h)  f x) / h) * g x) 
21164  124 
 0 > f x * E + D * g x" 
125 
by (intro LIM_add LIM_mult2 LIM_const DERIV_D f g) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

126 
thus "(\<lambda>h. (f(x+h) * g(x+h)  f x * g x) / h) 
21164  127 
 0 > f x * E + D * g x" 
128 
by (simp only: DERIV_mult_lemma) 

129 
qed 

130 

131 
lemma DERIV_mult: 

132 
"[ DERIV f x :> Da; DERIV g x :> Db ] 

133 
==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" 

134 
by (drule (1) DERIV_mult', simp only: mult_commute add_commute) 

135 

136 
lemma DERIV_unique: 

137 
"[ DERIV f x :> D; DERIV f x :> E ] ==> D = E" 

138 
apply (simp add: deriv_def) 

139 
apply (blast intro: LIM_unique) 

140 
done 

141 

142 
text{*Differentiation of finite sum*} 

143 

144 
lemma DERIV_sumr [rule_format (no_asm)]: 

145 
"(\<forall>r. m \<le> r & r < (m + n) > DERIV (%x. f r x) x :> (f' r x)) 

146 
> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)" 

147 
apply (induct "n") 

148 
apply (auto intro: DERIV_add) 

149 
done 

150 

151 
text{*Alternative definition for differentiability*} 

152 

153 
lemma DERIV_LIM_iff: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

154 
"((%h. (f(a + h)  f(a)) / h)  0 > D) = 
21164  155 
((%x. (f(x)f(a)) / (xa))  a > D)" 
156 
apply (rule iffI) 

157 
apply (drule_tac k=" a" in LIM_offset) 

158 
apply (simp add: diff_minus) 

159 
apply (drule_tac k="a" in LIM_offset) 

160 
apply (simp add: add_commute) 

161 
done 

162 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

163 
lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z)  f(x)) / (zx))  x > D)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

164 
by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) 
21164  165 

166 
lemma inverse_diff_inverse: 

167 
"\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk> 

168 
\<Longrightarrow> inverse a  inverse b =  (inverse a * (a  b) * inverse b)" 

169 
by (simp add: right_diff_distrib left_diff_distrib mult_assoc) 

170 

171 
lemma DERIV_inverse_lemma: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

172 
"\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk> 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

173 
\<Longrightarrow> (inverse a  inverse b) / h 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

174 
=  (inverse a * ((a  b) / h) * inverse b)" 
21164  175 
by (simp add: inverse_diff_inverse) 
176 

177 
lemma DERIV_inverse': 

178 
assumes der: "DERIV f x :> D" 

179 
assumes neq: "f x \<noteq> 0" 

180 
shows "DERIV (\<lambda>x. inverse (f x)) x :>  (inverse (f x) * D * inverse (f x))" 

181 
(is "DERIV _ _ :> ?E") 

182 
proof (unfold DERIV_iff2) 

183 
from der have lim_f: "f  x > f x" 

184 
by (rule DERIV_isCont [unfolded isCont_def]) 

185 

186 
from neq have "0 < norm (f x)" by simp 

187 
with LIM_D [OF lim_f] obtain s 

188 
where s: "0 < s" 

189 
and less_fx: "\<And>z. \<lbrakk>z \<noteq> x; norm (z  x) < s\<rbrakk> 

190 
\<Longrightarrow> norm (f z  f x) < norm (f x)" 

191 
by fast 

192 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

193 
show "(\<lambda>z. (inverse (f z)  inverse (f x)) / (z  x))  x > ?E" 
21164  194 
proof (rule LIM_equal2 [OF s]) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

195 
fix z 
21164  196 
assume "z \<noteq> x" "norm (z  x) < s" 
197 
hence "norm (f z  f x) < norm (f x)" by (rule less_fx) 

198 
hence "f z \<noteq> 0" by auto 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

199 
thus "(inverse (f z)  inverse (f x)) / (z  x) = 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

200 
 (inverse (f z) * ((f z  f x) / (z  x)) * inverse (f x))" 
21164  201 
using neq by (rule DERIV_inverse_lemma) 
202 
next 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

203 
from der have "(\<lambda>z. (f z  f x) / (z  x))  x > D" 
21164  204 
by (unfold DERIV_iff2) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

205 
thus "(\<lambda>z.  (inverse (f z) * ((f z  f x) / (z  x)) * inverse (f x))) 
21164  206 
 x > ?E" 
207 
by (intro LIM_mult2 LIM_inverse LIM_minus LIM_const lim_f neq) 

208 
qed 

209 
qed 

210 

211 
lemma DERIV_divide: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

212 
"\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk> 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

213 
\<Longrightarrow> DERIV (\<lambda>x. f x / g x) x :> (D * g x  f x * E) / (g x * g x)" 
21164  214 
apply (subgoal_tac "f x *  (inverse (g x) * E * inverse (g x)) + 
215 
D * inverse (g x) = (D * g x  f x * E) / (g x * g x)") 

216 
apply (erule subst) 

217 
apply (unfold divide_inverse) 

218 
apply (erule DERIV_mult') 

219 
apply (erule (1) DERIV_inverse') 

220 
apply (simp add: left_diff_distrib nonzero_inverse_mult_distrib) 

221 
apply (simp add: mult_ac) 

222 
done 

223 

224 
lemma DERIV_power_Suc: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

225 
fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" 
21164  226 
assumes f: "DERIV f x :> D" 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

227 
shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) * (D * f x ^ n)" 
21164  228 
proof (induct n) 
229 
case 0 

230 
show ?case by (simp add: power_Suc f) 

231 
case (Suc k) 

232 
from DERIV_mult' [OF f Suc] show ?case 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

233 
apply (simp only: of_nat_Suc left_distrib mult_1_left) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

234 
apply (simp only: power_Suc right_distrib mult_ac) 
21164  235 
done 
236 
qed 

237 

238 
lemma DERIV_power: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

239 
fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" 
21164  240 
assumes f: "DERIV f x :> D" 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

241 
shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n  Suc 0))" 
21164  242 
by (cases "n", simp, simp add: DERIV_power_Suc f) 
243 

244 

245 
(*  *) 

246 
(* Caratheodory formulation of derivative at a point: standard proof *) 

247 
(*  *) 

248 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

249 
lemma nonzero_mult_divide_cancel_right: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

250 
"b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

251 
proof  
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

252 
assume b: "b \<noteq> 0" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

253 
have "a * b / b = a * (b / b)" by simp 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

254 
also have "\<dots> = a" by (simp add: divide_self b) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

255 
finally show "a * b / b = a" . 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

256 
qed 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

257 

21164  258 
lemma CARAT_DERIV: 
259 
"(DERIV f x :> l) = 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

260 
(\<exists>g. (\<forall>z. f z  f x = g z * (zx)) & isCont g x & g x = l)" 
21164  261 
(is "?lhs = ?rhs") 
262 
proof 

263 
assume der: "DERIV f x :> l" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

264 
show "\<exists>g. (\<forall>z. f z  f x = g z * (zx)) \<and> isCont g x \<and> g x = l" 
21164  265 
proof (intro exI conjI) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

266 
let ?g = "(%z. if z = x then l else (f z  f x) / (zx))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

267 
show "\<forall>z. f z  f x = ?g z * (zx)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

268 
by (simp add: nonzero_mult_divide_cancel_right) 
21164  269 
show "isCont ?g x" using der 
270 
by (simp add: isCont_iff DERIV_iff diff_minus 

271 
cong: LIM_equal [rule_format]) 

272 
show "?g x = l" by simp 

273 
qed 

274 
next 

275 
assume "?rhs" 

276 
then obtain g where 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

277 
"(\<forall>z. f z  f x = g z * (zx))" and "isCont g x" and "g x = l" by blast 
21164  278 
thus "(DERIV f x :> l)" 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

279 
by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

280 
cong: LIM_cong) 
21164  281 
qed 
282 

283 
lemma DERIV_chain': 

284 
assumes f: "DERIV f x :> D" 

285 
assumes g: "DERIV g (f x) :> E" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

286 
shows "DERIV (\<lambda>x. g (f x)) x :> E * D" 
21164  287 
proof (unfold DERIV_iff2) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

288 
obtain d where d: "\<forall>y. g y  g (f x) = d y * (y  f x)" 
21164  289 
and cont_d: "isCont d (f x)" and dfx: "d (f x) = E" 
290 
using CARAT_DERIV [THEN iffD1, OF g] by fast 

291 
from f have "f  x > f x" 

292 
by (rule DERIV_isCont [unfolded isCont_def]) 

293 
with cont_d have "(\<lambda>z. d (f z))  x > d (f x)" 

21239  294 
by (rule isCont_LIM_compose) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

295 
hence "(\<lambda>z. d (f z) * ((f z  f x) / (z  x))) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

296 
 x > d (f x) * D" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

297 
by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

298 
thus "(\<lambda>z. (g (f z)  g (f x)) / (z  x))  x > E * D" 
21164  299 
by (simp add: d dfx real_scaleR_def) 
300 
qed 

301 

302 

303 
subsubsection {* Nonstandard proofs *} 

304 

305 
lemma DERIV_NS_iff: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

306 
"(DERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 NS> D)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

307 
by (simp add: deriv_def LIM_NSLIM_iff) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

308 

e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

309 
lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h)  f(x))/h)  0 NS> D" 
21164  310 
by (simp add: deriv_def LIM_NSLIM_iff) 
311 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

312 
lemma hnorm_of_hypreal: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

313 
"\<And>r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = \<bar>r\<bar>" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

314 
by transfer (rule norm_of_real) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

315 

e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

316 
lemma Infinitesimal_of_hypreal: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

317 
"x \<in> Infinitesimal \<Longrightarrow> 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

318 
(( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

319 
apply (rule InfinitesimalI2) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

320 
apply (drule (1) InfinitesimalD2) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

321 
apply (simp add: hnorm_of_hypreal) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

322 
done 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

323 

e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

324 
lemma of_hypreal_eq_0_iff: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

325 
"\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

326 
by transfer (rule of_real_eq_0_iff) 
21164  327 

328 
lemma NSDeriv_unique: 

329 
"[ NSDERIV f x :> D; NSDERIV f x :> E ] ==> D = E" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

330 
apply (subgoal_tac "( *f* of_real) epsilon \<in> Infinitesimal  {0::'a star}") 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

331 
apply (simp only: nsderiv_def) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

332 
apply (drule (1) bspec)+ 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

333 
apply (drule (1) approx_trans3) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

334 
apply simp 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

335 
apply (simp add: Infinitesimal_of_hypreal Infinitesimal_epsilon) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

336 
apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero) 
21164  337 
done 
338 

339 
text {*First NSDERIV in terms of NSLIM*} 

340 

341 
text{*first equivalence *} 

342 
lemma NSDERIV_NSLIM_iff: 

343 
"(NSDERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 NS> D)" 

344 
apply (simp add: nsderiv_def NSLIM_def, auto) 

345 
apply (drule_tac x = xa in bspec) 

346 
apply (rule_tac [3] ccontr) 

347 
apply (drule_tac [3] x = h in spec) 

348 
apply (auto simp add: mem_infmal_iff starfun_lambda_cancel) 

349 
done 

350 

351 
text{*second equivalence *} 

352 
lemma NSDERIV_NSLIM_iff2: 

353 
"(NSDERIV f x :> D) = ((%z. (f(z)  f(x)) / (zx))  x NS> D)" 

354 
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff diff_minus [symmetric] 

355 
LIM_NSLIM_iff [symmetric]) 

356 

357 
(* while we're at it! *) 

358 
lemma NSDERIV_iff2: 

359 
"(NSDERIV f x :> D) = 

360 
(\<forall>w. 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

361 
w \<noteq> star_of x & w \<approx> star_of x > 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

362 
( *f* (%z. (f z  f x) / (zx))) w \<approx> star_of D)" 
21164  363 
by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 
364 

365 
(*FIXME DELETE*) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

366 
lemma hypreal_not_eq_minus_iff: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

367 
"(x \<noteq> a) = (x  a \<noteq> (0::'a::ab_group_add))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

368 
by auto 
21164  369 

370 
lemma NSDERIVD5: 

371 
"(NSDERIV f x :> D) ==> 

372 
(\<forall>u. u \<approx> hypreal_of_real x > 

373 
( *f* (%z. f z  f x)) u \<approx> hypreal_of_real D * (u  hypreal_of_real x))" 

374 
apply (auto simp add: NSDERIV_iff2) 

375 
apply (case_tac "u = hypreal_of_real x", auto) 

376 
apply (drule_tac x = u in spec, auto) 

377 
apply (drule_tac c = "u  hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1) 

378 
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1]) 

379 
apply (subgoal_tac [2] "( *f* (%z. zx)) u \<noteq> (0::hypreal) ") 

380 
apply (auto simp add: 

381 
approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] 

382 
Infinitesimal_subset_HFinite [THEN subsetD]) 

383 
done 

384 

385 
lemma NSDERIVD4: 

386 
"(NSDERIV f x :> D) ==> 

387 
(\<forall>h \<in> Infinitesimal. 

388 
(( *f* f)(hypreal_of_real x + h)  

389 
hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" 

390 
apply (auto simp add: nsderiv_def) 

391 
apply (case_tac "h = (0::hypreal) ") 

392 
apply (auto simp add: diff_minus) 

393 
apply (drule_tac x = h in bspec) 

394 
apply (drule_tac [2] c = h in approx_mult1) 

395 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 

396 
simp add: diff_minus) 

397 
done 

398 

399 
lemma NSDERIVD3: 

400 
"(NSDERIV f x :> D) ==> 

401 
(\<forall>h \<in> Infinitesimal  {0}. 

402 
(( *f* f)(hypreal_of_real x + h)  

403 
hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" 

404 
apply (auto simp add: nsderiv_def) 

405 
apply (rule ccontr, drule_tac x = h in bspec) 

406 
apply (drule_tac [2] c = h in approx_mult1) 

407 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 

408 
simp add: mult_assoc diff_minus) 

409 
done 

410 

411 
text{*Differentiability implies continuity 

412 
nice and simple "algebraic" proof*} 

413 
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x" 

414 
apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def) 

415 
apply (drule approx_minus_iff [THEN iffD1]) 

416 
apply (drule hypreal_not_eq_minus_iff [THEN iffD1]) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

417 
apply (drule_tac x = "xa  star_of x" in bspec) 
21164  418 
prefer 2 apply (simp add: add_assoc [symmetric]) 
419 
apply (auto simp add: mem_infmal_iff [symmetric] add_commute) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

420 
apply (drule_tac c = "xa  star_of x" in approx_mult1) 
21164  421 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

422 
simp add: mult_assoc nonzero_mult_divide_cancel_right) 
21164  423 
apply (drule_tac x3=D in 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

424 
HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, 
21164  425 
THEN mem_infmal_iff [THEN iffD1]]) 
426 
apply (auto simp add: mult_commute 

427 
intro: approx_trans approx_minus_iff [THEN iffD2]) 

428 
done 

429 

430 
text{*Differentiation rules for combinations of functions 

431 
follow from clear, straightforard, algebraic 

432 
manipulations*} 

433 
text{*Constant function*} 

434 

435 
(* use simple constant nslimit theorem *) 

436 
lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)" 

437 
by (simp add: NSDERIV_NSLIM_iff) 

438 

439 
text{*Sum of functions proved easily*} 

440 

441 
lemma NSDERIV_add: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

442 
==> NSDERIV (%x. f x + g x) x :> Da + Db" 

443 
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) 

444 
apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

445 
apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add) 
21164  446 
apply (auto simp add: diff_def add_ac) 
447 
done 

448 

449 
text{*Product of functions  Proof is trivial but tedious 

450 
and long due to rearrangement of terms*} 

451 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

452 
lemma lemma_nsderiv1: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

453 
fixes a b c d :: "'a::comm_ring star" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

454 
shows "(a*b)  (c*d) = (b*(a  c)) + (c*(b  d))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

455 
by (simp add: right_diff_distrib mult_ac) 
21164  456 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

457 
lemma lemma_nsderiv2: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

458 
fixes x y z :: "'a::real_normed_field star" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

459 
shows "[ (x  y) / z = star_of D + yb; z \<noteq> 0; 
21164  460 
z \<in> Infinitesimal; yb \<in> Infinitesimal ] 
461 
==> x  y \<approx> 0" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

462 
apply (simp add: nonzero_divide_eq_eq) 
21164  463 
apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add 
464 
simp add: mult_assoc mem_infmal_iff [symmetric]) 

465 
apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) 

466 
done 

467 

468 
lemma NSDERIV_mult: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

469 
==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" 

470 
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) 

471 
apply (auto dest!: spec 

472 
simp add: starfun_lambda_cancel lemma_nsderiv1) 

473 
apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib) 

474 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ 

475 
apply (auto simp add: times_divide_eq_right [symmetric] 

476 
simp del: times_divide_eq) 

477 
apply (drule_tac D = Db in lemma_nsderiv2, assumption+) 

478 
apply (drule_tac 

479 
approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) 

480 
apply (auto intro!: approx_add_mono1 

481 
simp add: left_distrib right_distrib mult_commute add_assoc) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

482 
apply (rule_tac b1 = "star_of Db * star_of (f x)" 
21164  483 
in add_commute [THEN subst]) 
484 
apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] 

485 
Infinitesimal_add Infinitesimal_mult 

486 
Infinitesimal_hypreal_of_real_mult 

487 
Infinitesimal_hypreal_of_real_mult2 

488 
simp add: add_assoc [symmetric]) 

489 
done 

490 

491 
text{*Multiplying by a constant*} 

492 
lemma NSDERIV_cmult: "NSDERIV f x :> D 

493 
==> NSDERIV (%x. c * f x) x :> c*D" 

494 
apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 

495 
minus_mult_right right_diff_distrib [symmetric]) 

496 
apply (erule NSLIM_const [THEN NSLIM_mult]) 

497 
done 

498 

499 
text{*Negation of function*} 

500 
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. (f x)) x :> D" 

501 
proof (simp add: NSDERIV_NSLIM_iff) 

502 
assume "(\<lambda>h. (f (x + h)  f x) / h)  0 NS> D" 

503 
hence deriv: "(\<lambda>h.  ((f(x+h)  f x) / h))  0 NS>  D" 

504 
by (rule NSLIM_minus) 

505 
have "\<forall>h.  ((f (x + h)  f x) / h) = ( f (x + h) + f x) / h" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

506 
by (simp add: minus_divide_left diff_def) 
21164  507 
with deriv 
508 
show "(\<lambda>h. ( f (x + h) + f x) / h)  0 NS>  D" by simp 

509 
qed 

510 

511 
text{*Subtraction*} 

512 
lemma NSDERIV_add_minus: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] ==> NSDERIV (%x. f x + g x) x :> Da + Db" 

513 
by (blast dest: NSDERIV_add NSDERIV_minus) 

514 

515 
lemma NSDERIV_diff: 

516 
"[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

517 
==> NSDERIV (%x. f x  g x) x :> DaDb" 

518 
apply (simp add: diff_minus) 

519 
apply (blast intro: NSDERIV_add_minus) 

520 
done 

521 

522 
text{* Similarly to the above, the chain rule admits an entirely 

523 
straightforward derivation. Compare this with Harrison's 

524 
HOL proof of the chain rule, which proved to be trickier and 

525 
required an alternative characterisation of differentiability 

526 
the socalled Carathedory derivative. Our main problem is 

527 
manipulation of terms.*} 

528 

529 

530 
(* lemmas *) 

531 
lemma NSDERIV_zero: 

532 
"[ NSDERIV g x :> D; 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

533 
( *f* g) (star_of x + xa) = star_of (g x); 
21164  534 
xa \<in> Infinitesimal; 
535 
xa \<noteq> 0 

536 
] ==> D = 0" 

537 
apply (simp add: nsderiv_def) 

538 
apply (drule bspec, auto) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

539 
apply (rule star_of_approx_iff [THEN iffD1], simp) 
21164  540 
done 
541 

542 
(* can be proved differently using NSLIM_isCont_iff *) 

543 
lemma NSDERIV_approx: 

544 
"[ NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 ] 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

545 
==> ( *f* f) (star_of x + h)  star_of (f x) \<approx> 0" 
21164  546 
apply (simp add: nsderiv_def) 
547 
apply (simp add: mem_infmal_iff [symmetric]) 

548 
apply (rule Infinitesimal_ratio) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

549 
apply (rule_tac [3] approx_star_of_HFinite, auto) 
21164  550 
done 
551 

552 
(* 

553 
from one version of differentiability 

554 

555 
f(x)  f(a) 

556 
 \<approx> Db 

557 
x  a 

558 
*) 

559 
lemma NSDERIVD1: "[ NSDERIV f (g x) :> Da; 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

560 
( *f* g) (star_of(x) + xa) \<noteq> star_of (g x); 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

561 
( *f* g) (star_of(x) + xa) \<approx> star_of (g x) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

562 
] ==> (( *f* f) (( *f* g) (star_of(x) + xa)) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

563 
 star_of (f (g x))) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

564 
/ (( *f* g) (star_of(x) + xa)  star_of (g x)) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

565 
\<approx> star_of(Da)" 
21164  566 
by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric]) 
567 

568 
(* 

569 
from other version of differentiability 

570 

571 
f(x + h)  f(x) 

572 
 \<approx> Db 

573 
h 

574 
*) 

575 
lemma NSDERIVD2: "[ NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 ] 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

576 
==> (( *f* g) (star_of(x) + xa)  star_of(g x)) / xa 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

577 
\<approx> star_of(Db)" 
21164  578 
by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) 
579 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

580 
lemma lemma_chain: "(z::'a::real_normed_field star) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

581 
proof  
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

582 
assume z: "z \<noteq> 0" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

583 
have "x * y = x * (inverse z * z) * y" by (simp add: z) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

584 
thus ?thesis by (simp add: mult_assoc) 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

585 
qed 
21164  586 

587 
text{*This proof uses both definitions of differentiability.*} 

588 
lemma NSDERIV_chain: "[ NSDERIV f (g x) :> Da; NSDERIV g x :> Db ] 

589 
==> NSDERIV (f o g) x :> Da * Db" 

590 
apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def 

591 
mem_infmal_iff [symmetric]) 

592 
apply clarify 

593 
apply (frule_tac f = g in NSDERIV_approx) 

594 
apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric]) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

595 
apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ") 
21164  596 
apply (drule_tac g = g in NSDERIV_zero) 
597 
apply (auto simp add: divide_inverse) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

598 
apply (rule_tac z1 = "( *f* g) (star_of (x) + xa)  star_of (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) 
21164  599 
apply (erule hypreal_not_eq_minus_iff [THEN iffD1]) 
21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

600 
apply (rule approx_mult_star_of) 
21164  601 
apply (simp_all add: divide_inverse [symmetric]) 
602 
apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2]) 

603 
apply (blast intro: NSDERIVD2) 

604 
done 

605 

606 
text{*Differentiation of natural number powers*} 

607 
lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1" 

608 
by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if) 

609 

610 
lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c" 

611 
by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp) 

612 

613 
(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*) 

614 
lemma NSDERIV_inverse: 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

615 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

616 
shows "x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> ( (inverse x ^ Suc (Suc 0)))" 
21164  617 
apply (simp add: nsderiv_def) 
618 
apply (rule ballI, simp, clarify) 

619 
apply (frule (1) Infinitesimal_add_not_zero) 

620 
apply (simp add: add_commute) 

621 
(*apply (auto simp add: starfun_inverse_inverse realpow_two 

622 
simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

623 
apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

624 
nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_def 
21164  625 
del: inverse_mult_distrib inverse_minus_eq 
626 
minus_mult_left [symmetric] minus_mult_right [symmetric]) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

627 
apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right) 
21164  628 
apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib 
629 
del: minus_mult_left [symmetric] minus_mult_right [symmetric]) 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

630 
apply (rule_tac y = "inverse ( (star_of x * star_of x))" in approx_trans) 
21164  631 
apply (rule inverse_add_Infinitesimal_approx2) 
632 
apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal 

633 
simp add: inverse_minus_eq [symmetric] HFinite_minus_iff) 

634 
apply (rule Infinitesimal_HFinite_mult2, auto) 

635 
done 

636 

637 
subsubsection {* Equivalence of NS and Standard definitions *} 

638 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

639 
lemma divideR_eq_divide: "x /# y = x / y" 
21164  640 
by (simp add: real_scaleR_def divide_inverse mult_commute) 
641 

642 
text{*Now equivalence between NSDERIV and DERIV*} 

643 
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)" 

644 
by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) 

645 

646 
(* let's do the standard proof though theorem *) 

647 
(* LIM_mult2 follows from a NS proof *) 

648 

649 
lemma DERIV_cmult: 

650 
"DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" 

651 
by (drule DERIV_mult' [OF DERIV_const], simp) 

652 

653 
(* standard version *) 

654 
lemma DERIV_chain: "[ DERIV f (g x) :> Da; DERIV g x :> Db ] ==> DERIV (f o g) x :> Da * Db" 

655 
by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute) 

656 

657 
lemma DERIV_chain2: "[ DERIV f (g x) :> Da; DERIV g x :> Db ] ==> DERIV (%x. f (g x)) x :> Da * Db" 

658 
by (auto dest: DERIV_chain simp add: o_def) 

659 

660 
(*derivative of linear multiplication*) 

661 
lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" 

662 
by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp) 

663 

664 
lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n  Suc 0))" 

665 
apply (cut_tac DERIV_power [OF DERIV_Id]) 

666 
apply (simp add: real_scaleR_def real_of_nat_def) 

667 
done 

668 

669 
(* NS version *) 

670 
lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n  Suc 0))" 

671 
by (simp add: NSDERIV_DERIV_iff DERIV_pow) 

672 

673 
text{*Power of 1*} 

674 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

675 
lemma DERIV_inverse: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

676 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

677 
shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> ((inverse x ^ Suc (Suc 0)))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

678 
by (drule DERIV_inverse' [OF DERIV_Id]) (simp add: power_Suc) 
21164  679 

680 
text{*Derivative of inverse*} 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

681 
lemma DERIV_inverse_fun: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

682 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

683 
shows "[ DERIV f x :> d; f(x) \<noteq> 0 ] 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

684 
==> DERIV (%x. inverse(f x)) x :> ( (d * inverse(f(x) ^ Suc (Suc 0))))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

685 
by (drule (1) DERIV_inverse') (simp add: mult_ac power_Suc nonzero_inverse_mult_distrib) 
21164  686 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

687 
lemma NSDERIV_inverse_fun: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

688 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

689 
shows "[ NSDERIV f x :> d; f(x) \<noteq> 0 ] 
21164  690 
==> NSDERIV (%x. inverse(f x)) x :> ( (d * inverse(f(x) ^ Suc (Suc 0))))" 
691 
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc) 

692 

693 
text{*Derivative of quotient*} 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

694 
lemma DERIV_quotient: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

695 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

696 
shows "[ DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 ] 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

697 
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x)  (e*f(x))) / (g(x) ^ Suc (Suc 0))" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

698 
by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc) 
21164  699 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

700 
lemma NSDERIV_quotient: 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

701 
fixes x :: "'a::{real_normed_field,recpower}" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

702 
shows "[ NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 ] 
21164  703 
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) 
704 
 (e*f(x))) / (g(x) ^ Suc (Suc 0))" 

705 
by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc) 

706 

707 
lemma CARAT_NSDERIV: "NSDERIV f x :> l ==> 

708 
\<exists>g. (\<forall>z. f z  f x = g z * (zx)) & isNSCont g x & g x = l" 

709 
by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

710 
mult_commute) 
21164  711 

712 
lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + z = (y::hypreal))" 

713 
by auto 

714 

715 
lemma CARAT_DERIVD: 

716 
assumes all: "\<forall>z. f z  f x = g z * (zx)" 

717 
and nsc: "isNSCont g x" 

718 
shows "NSDERIV f x :> g x" 

719 
proof  

720 
from nsc 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

721 
have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

722 
( *f* g) w * (w  star_of x) / (w  star_of x) \<approx> 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

723 
star_of (g x)" 
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

724 
by (simp add: isNSCont_def nonzero_mult_divide_cancel_right) 
21164  725 
thus ?thesis using all 
726 
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) 

727 
qed 

728 

729 
subsubsection {* Differentiability predicate *} 

730 

731 
lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D" 

732 
by (simp add: differentiable_def) 

733 

734 
lemma differentiableI: "DERIV f x :> D ==> f differentiable x" 

735 
by (force simp add: differentiable_def) 

736 

737 
lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D" 

738 
by (simp add: NSdifferentiable_def) 

739 

740 
lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x" 

741 
by (force simp add: NSdifferentiable_def) 

742 

743 
lemma differentiable_const: "(\<lambda>z. a) differentiable x" 

744 
apply (unfold differentiable_def) 

745 
apply (rule_tac x=0 in exI) 

746 
apply simp 

747 
done 

748 

749 
lemma differentiable_sum: 

750 
assumes "f differentiable x" 

751 
and "g differentiable x" 

752 
shows "(\<lambda>x. f x + g x) differentiable x" 

753 
proof  

754 
from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) 

755 
then obtain df where "DERIV f x :> df" .. 

756 
moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 

757 
then obtain dg where "DERIV g x :> dg" .. 

758 
ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add) 

759 
hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto 

760 
thus ?thesis by (fold differentiable_def) 

761 
qed 

762 

763 
lemma differentiable_diff: 

764 
assumes "f differentiable x" 

765 
and "g differentiable x" 

766 
shows "(\<lambda>x. f x  g x) differentiable x" 

767 
proof  

768 
from prems have "f differentiable x" by simp 

769 
moreover 

770 
from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 

771 
then obtain dg where "DERIV g x :> dg" .. 

772 
then have "DERIV (\<lambda>x.  g x) x :> dg" by (rule DERIV_minus) 

773 
hence "\<exists>D. DERIV (\<lambda>x.  g x) x :> D" by auto 

774 
hence "(\<lambda>x.  g x) differentiable x" by (fold differentiable_def) 

775 
ultimately 

776 
show ?thesis 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

777 
by (auto simp: diff_def dest: differentiable_sum) 
21164  778 
qed 
779 

780 
lemma differentiable_mult: 

781 
assumes "f differentiable x" 

782 
and "g differentiable x" 

783 
shows "(\<lambda>x. f x * g x) differentiable x" 

784 
proof  

785 
from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) 

786 
then obtain df where "DERIV f x :> df" .. 

787 
moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 

788 
then obtain dg where "DERIV g x :> dg" .. 

789 
ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult) 

790 
hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto 

791 
thus ?thesis by (fold differentiable_def) 

792 
qed 

793 

794 
subsection {*(NS) Increment*} 

795 
lemma incrementI: 

796 
"f NSdifferentiable x ==> 

797 
increment f x h = ( *f* f) (hypreal_of_real(x) + h)  

798 
hypreal_of_real (f x)" 

799 
by (simp add: increment_def) 

800 

801 
lemma incrementI2: "NSDERIV f x :> D ==> 

802 
increment f x h = ( *f* f) (hypreal_of_real(x) + h)  

803 
hypreal_of_real (f x)" 

804 
apply (erule NSdifferentiableI [THEN incrementI]) 

805 
done 

806 

807 
(* The Increment theorem  Keisler p. 65 *) 

808 
lemma increment_thm: "[ NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 ] 

809 
==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h" 

810 
apply (frule_tac h = h in incrementI2, simp add: nsderiv_def) 

811 
apply (drule bspec, auto) 

812 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) 

813 
apply (frule_tac b1 = "hypreal_of_real (D) + y" 

814 
in hypreal_mult_right_cancel [THEN iffD2]) 

815 
apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h)  hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) 

816 
apply assumption 

817 
apply (simp add: times_divide_eq_right [symmetric]) 

818 
apply (auto simp add: left_distrib) 

819 
done 

820 

821 
lemma increment_thm2: 

822 
"[ NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 ] 

823 
==> \<exists>e \<in> Infinitesimal. increment f x h = 

824 
hypreal_of_real(D)*h + e*h" 

825 
by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm) 

826 

827 

828 
lemma increment_approx_zero: "[ NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 ] 

829 
==> increment f x h \<approx> 0" 

830 
apply (drule increment_thm2, 

831 
auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric]) 

832 
apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) 

833 
done 

834 

835 
subsection {* Nested Intervals and Bisection *} 

836 

837 
text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). 

838 
All considerably tidied by lcp.*} 

839 

840 
lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) > f m \<le> f(m + no)" 

841 
apply (induct "no") 

842 
apply (auto intro: order_trans) 

843 
done 

844 

845 
lemma f_inc_g_dec_Beq_f: "[ \<forall>n. f(n) \<le> f(Suc n); 

846 
\<forall>n. g(Suc n) \<le> g(n); 

847 
\<forall>n. f(n) \<le> g(n) ] 

848 
==> Bseq (f :: nat \<Rightarrow> real)" 

849 
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI) 

850 
apply (induct_tac "n") 

851 
apply (auto intro: order_trans) 

852 
apply (rule_tac y = "g (Suc na)" in order_trans) 

853 
apply (induct_tac [2] "na") 

854 
apply (auto intro: order_trans) 

855 
done 

856 

857 
lemma f_inc_g_dec_Beq_g: "[ \<forall>n. f(n) \<le> f(Suc n); 

858 
\<forall>n. g(Suc n) \<le> g(n); 

859 
\<forall>n. f(n) \<le> g(n) ] 

860 
==> Bseq (g :: nat \<Rightarrow> real)" 

861 
apply (subst Bseq_minus_iff [symmetric]) 

862 
apply (rule_tac g = "%x.  (f x)" in f_inc_g_dec_Beq_f) 

863 
apply auto 

864 
done 

865 

866 
lemma f_inc_imp_le_lim: 

867 
fixes f :: "nat \<Rightarrow> real" 

868 
shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f" 

869 
apply (rule linorder_not_less [THEN iffD1]) 

870 
apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc) 

871 
apply (drule real_less_sum_gt_zero) 

872 
apply (drule_tac x = "f n +  lim f" in spec, safe) 

873 
apply (drule_tac P = "%na. no\<le>na > ?Q na" and x = "no + n" in spec, auto) 

874 
apply (subgoal_tac "lim f \<le> f (no + n) ") 

875 
apply (drule_tac no=no and m=n in lemma_f_mono_add) 

876 
apply (auto simp add: add_commute) 

877 
apply (induct_tac "no") 

878 
apply simp 

879 
apply (auto intro: order_trans simp add: diff_minus abs_if) 

880 
done 

881 

882 
lemma lim_uminus: "convergent g ==> lim (%x.  g x) =  (lim g)" 

883 
apply (rule LIMSEQ_minus [THEN limI]) 

884 
apply (simp add: convergent_LIMSEQ_iff) 

885 
done 

886 

887 
lemma g_dec_imp_lim_le: 

888 
fixes g :: "nat \<Rightarrow> real" 

889 
shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n" 

890 
apply (subgoal_tac " (g n) \<le>  (lim g) ") 

891 
apply (cut_tac [2] f = "%x.  (g x)" in f_inc_imp_le_lim) 

892 
apply (auto simp add: lim_uminus convergent_minus_iff [symmetric]) 

893 
done 

894 

895 
lemma lemma_nest: "[ \<forall>n. f(n) \<le> f(Suc n); 

896 
\<forall>n. g(Suc n) \<le> g(n); 

897 
\<forall>n. f(n) \<le> g(n) ] 

898 
==> \<exists>l m :: real. l \<le> m & ((\<forall>n. f(n) \<le> l) & f > l) & 

899 
((\<forall>n. m \<le> g(n)) & g > m)" 

900 
apply (subgoal_tac "monoseq f & monoseq g") 

901 
prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc) 

902 
apply (subgoal_tac "Bseq f & Bseq g") 

903 
prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g) 

904 
apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff) 

905 
apply (rule_tac x = "lim f" in exI) 

906 
apply (rule_tac x = "lim g" in exI) 

907 
apply (auto intro: LIMSEQ_le) 

908 
apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff) 

909 
done 

910 

911 
lemma lemma_nest_unique: "[ \<forall>n. f(n) \<le> f(Suc n); 

912 
\<forall>n. g(Suc n) \<le> g(n); 

913 
\<forall>n. f(n) \<le> g(n); 

914 
(%n. f(n)  g(n)) > 0 ] 

915 
==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f > l) & 

916 
((\<forall>n. l \<le> g(n)) & g > l)" 

917 
apply (drule lemma_nest, auto) 

918 
apply (subgoal_tac "l = m") 

919 
apply (drule_tac [2] X = f in LIMSEQ_diff) 

920 
apply (auto intro: LIMSEQ_unique) 

921 
done 

922 

923 
text{*The universal quantifiers below are required for the declaration 

924 
of @{text Bolzano_nest_unique} below.*} 

925 

926 
lemma Bolzano_bisect_le: 

927 
"a \<le> b ==> \<forall>n. fst (Bolzano_bisect P a b n) \<le> snd (Bolzano_bisect P a b n)" 

928 
apply (rule allI) 

929 
apply (induct_tac "n") 

930 
apply (auto simp add: Let_def split_def) 

931 
done 

932 

933 
lemma Bolzano_bisect_fst_le_Suc: "a \<le> b ==> 

934 
\<forall>n. fst(Bolzano_bisect P a b n) \<le> fst (Bolzano_bisect P a b (Suc n))" 

935 
apply (rule allI) 

936 
apply (induct_tac "n") 

937 
apply (auto simp add: Bolzano_bisect_le Let_def split_def) 

938 
done 

939 

940 
lemma Bolzano_bisect_Suc_le_snd: "a \<le> b ==> 

941 
\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)" 

942 
apply (rule allI) 

943 
apply (induct_tac "n") 

944 
apply (auto simp add: Bolzano_bisect_le Let_def split_def) 

945 
done 

946 

947 
lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" 

948 
apply (auto) 

949 
apply (drule_tac f = "%u. (1/2) *u" in arg_cong) 

950 
apply (simp) 

951 
done 

952 

953 
lemma Bolzano_bisect_diff: 

954 
"a \<le> b ==> 

955 
snd(Bolzano_bisect P a b n)  fst(Bolzano_bisect P a b n) = 

956 
(ba) / (2 ^ n)" 

957 
apply (induct "n") 

958 
apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def) 

959 
done 

960 

961 
lemmas Bolzano_nest_unique = 

962 
lemma_nest_unique 

963 
[OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le] 

964 

965 

966 
lemma not_P_Bolzano_bisect: 

967 
assumes P: "!!a b c. [ P(a,b); P(b,c); a \<le> b; b \<le> c] ==> P(a,c)" 

968 
and notP: "~ P(a,b)" 

969 
and le: "a \<le> b" 

970 
shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" 

971 
proof (induct n) 

972 
case 0 thus ?case by simp 

973 
next 

974 
case (Suc n) 

975 
thus ?case 

976 
by (auto simp del: surjective_pairing [symmetric] 

977 
simp add: Let_def split_def Bolzano_bisect_le [OF le] 

978 
P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"]) 

979 
qed 

980 

981 
(*Now we repackage P_prem as a formula*) 

982 
lemma not_P_Bolzano_bisect': 

983 
"[ \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c > P(a,c); 

984 
~ P(a,b); a \<le> b ] ==> 

985 
\<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" 

986 
by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE]) 

987 

988 

989 

990 
lemma lemma_BOLZANO: 

991 
"[ \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c > P(a,c); 

992 
\<forall>x. \<exists>d::real. 0 < d & 

993 
(\<forall>a b. a \<le> x & x \<le> b & (ba) < d > P(a,b)); 

994 
a \<le> b ] 

995 
==> P(a,b)" 

996 
apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+) 

997 
apply (rule LIMSEQ_minus_cancel) 

998 
apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero) 

999 
apply (rule ccontr) 

1000 
apply (drule not_P_Bolzano_bisect', assumption+) 

1001 
apply (rename_tac "l") 

1002 
apply (drule_tac x = l in spec, clarify) 

1003 
apply (simp add: LIMSEQ_def) 

1004 
apply (drule_tac P = "%r. 0<r > ?Q r" and x = "d/2" in spec) 

1005 
apply (drule_tac P = "%r. 0<r > ?Q r" and x = "d/2" in spec) 

1006 
apply (drule real_less_half_sum, auto) 

1007 
apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec) 

1008 
apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec) 

1009 
apply safe 

1010 
apply (simp_all (no_asm_simp)) 

1011 
apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa))  l) + abs (snd (Bolzano_bisect P a b (no + noa))  l)" in order_le_less_trans) 

1012 
apply (simp (no_asm_simp) add: abs_if) 

1013 
apply (rule real_sum_of_halves [THEN subst]) 

1014 
apply (rule add_strict_mono) 

1015 
apply (simp_all add: diff_minus [symmetric]) 

1016 
done 

1017 

1018 

1019 
lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) > P(a,c)) & 

1020 
(\<forall>x. \<exists>d::real. 0 < d & 

1021 
(\<forall>a b. a \<le> x & x \<le> b & (ba) < d > P(a,b)))) 

1022 
> (\<forall>a b. a \<le> b > P(a,b))" 

1023 
apply clarify 

1024 
apply (blast intro: lemma_BOLZANO) 

1025 
done 

1026 

1027 

1028 
subsection {* Intermediate Value Theorem *} 

1029 

1030 
text {*Prove Contrapositive by Bisection*} 

1031 

1032 
lemma IVT: "[ f(a::real) \<le> (y::real); y \<le> f(b); 

1033 
a \<le> b; 

1034 
(\<forall>x. a \<le> x & x \<le> b > isCont f x) ] 

1035 
==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" 

1036 
apply (rule contrapos_pp, assumption) 

1037 
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b > ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2) 

1038 
apply safe 

1039 
apply simp_all 

1040 
apply (simp add: isCont_iff LIM_def) 

1041 
apply (rule ccontr) 

1042 
apply (subgoal_tac "a \<le> x & x \<le> b") 

1043 
prefer 2 

1044 
apply simp 

1045 
apply (drule_tac P = "%d. 0<d > ?P d" and x = 1 in spec, arith) 

1046 
apply (drule_tac x = x in spec)+ 

1047 
apply simp 

1048 
apply (drule_tac P = "%r. ?P r > (\<exists>s>0. ?Q r s) " and x = "\<bar>y  f x\<bar>" in spec) 

1049 
apply safe 

1050 
apply simp 

1051 
apply (drule_tac x = s in spec, clarify) 

1052 
apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe) 

1053 
apply (drule_tac x = "bax" in spec) 

1054 
apply (simp_all add: abs_if) 

1055 
apply (drule_tac x = "aax" in spec) 

1056 
apply (case_tac "x \<le> aa", simp_all) 

1057 
done 

1058 

1059 
lemma IVT2: "[ f(b::real) \<le> (y::real); y \<le> f(a); 

1060 
a \<le> b; 

1061 
(\<forall>x. a \<le> x & x \<le> b > isCont f x) 

1062 
] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y" 

1063 
apply (subgoal_tac " f a \<le> y & y \<le>  f b", clarify) 

1064 
apply (drule IVT [where f = "%x.  f x"], assumption) 

1065 
apply (auto intro: isCont_minus) 

1066 
done 

1067 

1068 
(*HOL style here: objectlevel formulations*) 

1069 
lemma IVT_objl: "(f(a::real) \<le> (y::real) & y \<le> f(b) & a \<le> b & 

1070 
(\<forall>x. a \<le> x & x \<le> b > isCont f x)) 

1071 
> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" 

1072 
apply (blast intro: IVT) 

1073 
done 

1074 

1075 
lemma IVT2_objl: "(f(b::real) \<le> (y::real) & y \<le> f(a) & a \<le> b & 

1076 
(\<forall>x. a \<le> x & x \<le> b > isCont f x)) 

1077 
> (\<exists>x. a \<le> x & x \<le> b & f(x) = y)" 

1078 
apply (blast intro: IVT2) 

1079 
done 

1080 

1081 
text{*By bisection, function continuous on closed interval is bounded above*} 

1082 

1083 
lemma isCont_bounded: 

1084 
"[ a \<le> b; \<forall>x. a \<le> x & x \<le> b > isCont f x ] 

1085 
==> \<exists>M::real. \<forall>x::real. a \<le> x & x \<le> b > f(x) \<le> M" 

1086 
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b > (\<exists>M. \<forall>x. u \<le> x & x \<le> v > f x \<le> M)" in lemma_BOLZANO2) 

1087 
apply safe 

1088 
apply simp_all 

1089 
apply (rename_tac x xa ya M Ma) 

1090 
apply (cut_tac x = M and y = Ma in linorder_linear, safe) 

1091 
apply (rule_tac x = Ma in exI, clarify) 

1092 
apply (cut_tac x = xb and y = xa in linorder_linear, force) 

1093 
apply (rule_tac x = M in exI, clarify) 

1094 
apply (cut_tac x = xb and y = xa in linorder_linear, force) 

1095 
apply (case_tac "a \<le> x & x \<le> b") 

1096 
apply (rule_tac [2] x = 1 in exI) 

1097 
prefer 2 apply force 

1098 
apply (simp add: LIM_def isCont_iff) 

1099 
apply (drule_tac x = x in spec, auto) 

1100 
apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl) 

1101 
apply (drule_tac x = 1 in spec, auto) 

1102 
apply (rule_tac x = s in exI, clarify) 

1103 
apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify) 

1104 
apply (drule_tac x = "xax" in spec) 

1105 
apply (auto simp add: abs_ge_self) 

1106 
done 

1107 

1108 
text{*Refine the above to existence of least upper bound*} 

1109 

1110 
lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) > 

1111 
(\<exists>t. isLub UNIV S t)" 

1112 
by (blast intro: reals_complete) 

1113 

1114 
lemma isCont_has_Ub: "[ a \<le> b; \<forall>x. a \<le> x & x \<le> b > isCont f x ] 

1115 
==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b > f(x) \<le> M) & 

1116 
(\<forall>N. N < M > (\<exists>x. a \<le> x & x \<le> b & N < f(x)))" 

1117 
apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)" 

1118 
in lemma_reals_complete) 

1119 
apply auto 

1120 
apply (drule isCont_bounded, assumption) 

1121 
apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def) 

1122 
apply (rule exI, auto) 

1123 
apply (auto dest!: spec simp add: linorder_not_less) 

1124 
done 

1125 

1126 
text{*Now show that it attains its upper bound*} 

1127 

1128 
lemma isCont_eq_Ub: 

1129 
assumes le: "a \<le> b" 

1130 
and con: "\<forall>x::real. a \<le> x & x \<le> b > isCont f x" 

1131 
shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b > f(x) \<le> M) & 

1132 
(\<exists>x. a \<le> x & x \<le> b & f(x) = M)" 

1133 
proof  

1134 
from isCont_has_Ub [OF le con] 

1135 
obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" 

1136 
and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x" by blast 

1137 
show ?thesis 

1138 
proof (intro exI, intro conjI) 

1139 
show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1) 

1140 
show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M" 

1141 
proof (rule ccontr) 

1142 
assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)" 

1143 
with M1 have M3: "\<forall>x. a \<le> x & x \<le> b > f x < M" 

1144 
by (fastsimp simp add: linorder_not_le [symmetric]) 

1145 
hence "\<forall>x. a \<le> x & x \<le> b > isCont (%x. inverse (M  f x)) x" 

1146 
by (auto simp add: isCont_inverse isCont_diff con) 

1147 
from isCont_bounded [OF le this] 

1148 
obtain k where k: "!!x. a \<le> x & x \<le> b > inverse (M  f x) \<le> k" by auto 

1149 
have Minv: "!!x. a \<le> x & x \<le> b > 0 < inverse (M  f (x))" 

1150 
by (simp add: M3 compare_rls) 

1151 
have "!!x. a \<le> x & x \<le> b > inverse (M  f x) < k+1" using k 

1152 
by (auto intro: order_le_less_trans [of _ k]) 

1153 
with Minv 

1154 
have "!!x. a \<le> x & x \<le> b > inverse(k+1) < inverse(inverse(M  f x))" 

1155 
by (intro strip less_imp_inverse_less, simp_all) 

1156 
hence invlt: "!!x. a \<le> x & x \<le> b > inverse(k+1) < M  f x" 

1157 
by simp 

1158 
have "M  inverse (k+1) < M" using k [of a] Minv [of a] le 

1159 
by (simp, arith) 

1160 
from M2 [OF this] 

1161 
obtain x where ax: "a \<le> x & x \<le> b & M  inverse(k+1) < f x" .. 

1162 
thus False using invlt [of x] by force 

1163 
qed 

1164 
qed 

1165 
qed 

1166 

1167 

1168 
text{*Same theorem for lower bound*} 

1169 

1170 
lemma isCont_eq_Lb: "[ a \<le> b; \<forall>x. a \<le> x & x \<le> b > isCont f x ] 

1171 
==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b > M \<le> f(x)) & 

1172 
(\<exists>x. a \<le> x & x \<le> b & f(x) = M)" 

1173 
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b > isCont (%x.  (f x)) x") 

1174 
prefer 2 apply (blast intro: isCont_minus) 

1175 
apply (drule_tac f = "(%x.  (f x))" in isCont_eq_Ub) 

1176 
apply safe 

1177 
apply auto 

1178 
done 

1179 

1180 

1181 
text{*Another version.*} 

1182 

1183 
lemma isCont_Lb_Ub: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > isCont f x ] 

1184 
==> \<exists>L M::real. (\<forall>x::real. a \<le> x & x \<le> b > L \<le> f(x) & f(x) \<le> M) & 

1185 
(\<forall>y. L \<le> y & y \<le> M > (\<exists>x. a \<le> x & x \<le> b & (f(x) = y)))" 

1186 
apply (frule isCont_eq_Lb) 

1187 
apply (frule_tac [2] isCont_eq_Ub) 

1188 
apply (assumption+, safe) 

1189 
apply (rule_tac x = "f x" in exI) 

1190 
apply (rule_tac x = "f xa" in exI, simp, safe) 

1191 
apply (cut_tac x = x and y = xa in linorder_linear, safe) 

1192 
apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl) 

1193 
apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe) 

1194 
apply (rule_tac [2] x = xb in exI) 

1195 
apply (rule_tac [4] x = xb in exI, simp_all) 

1196 
done 

1197 

1198 

1199 
text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} 

1200 

1201 
lemma DERIV_left_inc: 

1202 
fixes f :: "real => real" 

1203 
assumes der: "DERIV f x :> l" 

1204 
and l: "0 < l" 

1205 
shows "\<exists>d > 0. \<forall>h > 0. h < d > f(x) < f(x + h)" 

1206 
proof  

1207 
from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] 

1208 
have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z)  f x) / z  l\<bar> < l)" 

1209 
by (simp add: diff_minus) 

1210 
then obtain s 

1211 
where s: "0 < s" 

1212 
and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z)  f x) / z  l\<bar> < l" 

1213 
by auto 

1214 
thus ?thesis 

1215 
proof (intro exI conjI strip) 

1216 
show "0<s" . 

1217 
fix h::real 

1218 
assume "0 < h" "h < s" 

1219 
with all [of h] show "f x < f (x+h)" 

1220 
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 

1221 
split add: split_if_asm) 

1222 
assume "~ (f (x+h)  f x) / h < l" and h: "0 < h" 

1223 
with l 

1224 
have "0 < (f (x+h)  f x) / h" by arith 

1225 
thus "f x < f (x+h)" 

1226 
by (simp add: pos_less_divide_eq h) 

1227 
qed 

1228 
qed 

1229 
qed 

1230 

1231 
lemma DERIV_left_dec: 

1232 
fixes f :: "real => real" 

1233 
assumes der: "DERIV f x :> l" 

1234 
and l: "l < 0" 

1235 
shows "\<exists>d > 0. \<forall>h > 0. h < d > f(x) < f(xh)" 

1236 
proof  

1237 
from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] 

1238 
have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z)  f x) / z  l\<bar> < l)" 

1239 
by (simp add: diff_minus) 

1240 
then obtain s 

1241 
where s: "0 < s" 

1242 
and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z)  f x) / z  l\<bar> < l" 

1243 
by auto 

1244 
thus ?thesis 

1245 
proof (intro exI conjI strip) 

1246 
show "0<s" . 

1247 
fix h::real 

1248 
assume "0 < h" "h < s" 

1249 
with all [of "h"] show "f x < f (xh)" 

1250 
proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 

1251 
split add: split_if_asm) 

1252 
assume "  ((f (xh)  f x) / h) < l" and h: "0 < h" 

1253 
with l 

1254 
have "0 < (f (xh)  f x) / h" by arith 

1255 
thus "f x < f (xh)" 

1256 
by (simp add: pos_less_divide_eq h) 

1257 
qed 

1258 
qed 

1259 
qed 

1260 

1261 
lemma DERIV_local_max: 

1262 
fixes f :: "real => real" 

1263 
assumes der: "DERIV f x :> l" 

1264 
and d: "0 < d" 

1265 
and le: "\<forall>y. \<bar>xy\<bar> < d > f(y) \<le> f(x)" 

1266 
shows "l = 0" 

1267 
proof (cases rule: linorder_cases [of l 0]) 

1268 
case equal show ?thesis . 

1269 
next 

1270 
case less 

1271 
from DERIV_left_dec [OF der less] 

1272 
obtain d' where d': "0 < d'" 

1273 
and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (xh)" by blast 

1274 
from real_lbound_gt_zero [OF d d'] 

1275 
obtain e where "0 < e \<and> e < d \<and> e < d'" .. 

1276 
with lt le [THEN spec [where x="xe"]] 

1277 
show ?thesis by (auto simp add: abs_if) 

1278 
next 

1279 
case greater 

1280 
from DERIV_left_inc [OF der greater] 

1281 
obtain d' where d': "0 < d'" 

1282 
and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast 

1283 
from real_lbound_gt_zero [OF d d'] 

1284 
obtain e where "0 < e \<and> e < d \<and> e < d'" .. 

1285 
with lt le [THEN spec [where x="x+e"]] 

1286 
show ?thesis by (auto simp add: abs_if) 

1287 
qed 

1288 

1289 

1290 
text{*Similar theorem for a local minimum*} 

1291 
lemma DERIV_local_min: 

1292 
fixes f :: "real => real" 

1293 
shows "[ DERIV f x :> l; 0 < d; \<forall>y. \<bar>xy\<bar> < d > f(x) \<le> f(y) ] ==> l = 0" 

1294 
by (drule DERIV_minus [THEN DERIV_local_max], auto) 

1295 

1296 

1297 
text{*In particular, if a function is locally flat*} 

1298 
lemma DERIV_local_const: 

1299 
fixes f :: "real => real" 

1300 
shows "[ DERIV f x :> l; 0 < d; \<forall>y. \<bar>xy\<bar> < d > f(x) = f(y) ] ==> l = 0" 

1301 
by (auto dest!: DERIV_local_max) 

1302 

1303 
text{*Lemma about introducing open ball in open interval*} 

1304 
lemma lemma_interval_lt: 

1305 
"[ a < x; x < b ] 

1306 
==> \<exists>d::real. 0 < d & (\<forall>y. \<bar>xy\<bar> < d > a < y & y < b)" 

1307 
apply (simp add: abs_interval_iff) 

1308 
apply (insert linorder_linear [of "xa" "bx"], safe) 

1309 
apply (rule_tac x = "xa" in exI) 

1310 
apply (rule_tac [2] x = "bx" in exI, auto) 

1311 
done 

1312 

1313 
lemma lemma_interval: "[ a < x; x < b ] ==> 

1314 
\<exists>d::real. 0 < d & (\<forall>y. \<bar>xy\<bar> < d > a \<le> y & y \<le> b)" 

1315 
apply (drule lemma_interval_lt, auto) 

1316 
apply (auto intro!: exI) 

1317 
done 

1318 

1319 
text{*Rolle's Theorem. 

1320 
If @{term f} is defined and continuous on the closed interval 

1321 
@{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, 

1322 
and @{term "f(a) = f(b)"}, 

1323 
then there exists @{text "x0 \<in> (a,b)"} such that @{term "f'(x0) = 0"}*} 

1324 
theorem Rolle: 

1325 
assumes lt: "a < b" 

1326 
and eq: "f(a) = f(b)" 

1327 
and con: "\<forall>x. a \<le> x & x \<le> b > isCont f x" 

1328 
and dif [rule_format]: "\<forall>x. a < x & x < b > f differentiable x" 

21784
e76faa6e65fd
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
huffman
parents:
21404
diff
changeset

1329 
shows "\<exists>z::real. a < z & z < b & DERIV f z :> 0" 
21164  1330 
proof  
1331 
have le: "a \<le> b" using lt by simp 

1332 
from isCont_eq_Ub [OF le con] 

1333 
obtain x where x_max: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f z \<le> f x" 

1334 
and alex: "a \<le> x" and xleb: "x \<le> b" 

1335 
by blast 

1336 
from isCont_eq_Lb [OF le con] 

1337 
obtain x' where x'_min: "\<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> f x' \<le> f z" 

1338 
and alex': "a \<le> x'" and x'leb: "x' \<le> b" 

1339 
by blast 

1340 
show ?thesis 

1341 
proof cases 

1342 
assume axb: "a < x & x < b" 

1343 
{*@{term f} attains its maximum within the interval*} 

1344 
hence ax: "a<x" and xb: "x<b" by auto 

1345 
from lemma_interval [OF ax xb] 

1346 
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>xy\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 

1347 
by blast 

1348 
hence bound': "\<forall>y. \<bar>xy\<bar> < d \<longrightarrow> f y \<le> f x" using x_max 

1349 
by blast 

1350 
from differentiableD [OF dif [OF axb]] 

1351 
obtain l where der: "DERIV f x :> l" .. 

1352 
have "l=0" by (rule DERIV_local_max [OF der d bound']) 

1353 
{*the derivative at a local maximum is zero*} 

1354 
thus ?thesis using ax xb der by auto 

1355 
next 

1356 
assume notaxb: "~ (a < x & x < b)" 

1357 
hence xeqab: "x=a  x=b" using alex xleb by arith 

1358 
hence fb_eq_fx: "f b = f x" by (auto simp add: eq) 

1359 
show ?thesis 

1360 
proof cases 

1361 
assume ax'b: "a < x' & x' < b" 

1362 
{*@{term f} attains its minimum within the interval*} 

1363 
hence ax': "a<x'" and x'b: "x'<b" by auto 

1364 
from lemma_interval [OF ax' x'b] 

1365 
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>x'y\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 

1366 
by blast 

1367 
hence bound': "\<forall>y. \<bar>x'y\<bar> < d \<longrightarrow> f x' \<le> f y" using x'_min 

1368 
by blast 

1369 
from differentiableD [OF dif [OF ax'b]] 

1370 
obtain l where der: "DERIV f x' :> l" .. 

1371 
have "l=0" by (rule DERIV_local_min [OF der d bound']) 

1372 
{*the derivative at a local minimum is zero*} 

1373 
thus ?thesis using ax' x'b der by auto 

1374 
next 

1375 
assume notax'b: "~ (a < x' & x' < b)" 

1376 
{*@{term f} is constant througout the interval*} 

1377 
hence x'eqab: "x'=a  x'=b" using alex' x'leb by arith 

1378 
hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) 

1379 
from dense [OF lt] 

1380 
obtain r where ar: "a < r" and rb: "r < b" by blast 

1381 
from lemma_interval [OF ar rb] 

1382 
obtain d where d: "0<d" and bound: "\<forall>y. \<bar>ry\<bar> < d \<longrightarrow> a \<le> y \<and> y \<le> b" 

1383 
by blast 

1384 
have eq_fb: "\<forall>z. a \<le> z > z \<le> b > f z = f b" 

1385 
proof (clarify) 

1386 
fix z::real 

1387 
assume az: "a \<le> z" and zb: "z \<le> b" 

1388 
show "f z = f b" 

1389 
proof (rule order_antisym) 

1390 
show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb) 

1391 
show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb) 

1392 
qed 

1393 
qed 

1394 
have bound': "\<forall>y. \<bar>ry\<bar> < d \<longrightarrow> f r = f y" 

1395 
proof (intro strip) 

1396 
fix y::real 

1397 
assume lt: "\<bar>ry\<bar> < d" 

1398 
hence "f y = f b" by (simp add: eq_fb bound) 

1399 
thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le) 

1400 
qed 

1401 
from differentiableD [OF dif [OF conjI [OF ar rb]]] 

1402 
obtain l where der: "DERIV f r :> l" .. 

1403 
have "l=0" by (rule DERIV_local_const [OF der d bound']) 

1404 
{*the derivative of a constant function is zero*} 

1405 
thus ?thesis using ar rb der by auto 

1406 
qed 

1407 
qed 

1408 
qed 

1409 

1410 

1411 
subsection{*Mean Value Theorem*} 

1412 

1413 
lemma lemma_MVT: 

1414 
"f a  (f b  f a)/(ba) * a = f b  (f b  f a)/(ba) * (b::real)" 

1415 
proof cases 

1416 
assume "a=b" thus ?thesis by simp 

1417 
next 

1418 
assume "a\<noteq>b" 

1419 
hence ba: "ba \<noteq> 0" by arith 

1420 
show ?thesis 

1421 
by (rule real_mult_left_cancel [OF ba, THEN iffD1], 
