2 Author : Jacques D. Fleuriot
3 Copyright : 2001 University of Edinburgh
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
7 header{*Limits, Continuity and Differentiation for Complex Functions*}
12 declare hypreal_epsilon_not_zero [simp]
15 lemma lemma_complex_mult_inverse_squared [simp]:
16 "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
17 by (simp add: numeral_2_eq_2)
19 text{*Changing the quantified variable. Install earlier?*}
20 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
22 apply (drule_tac x="x+a" in spec)
23 apply (simp add: diff_minus add_assoc)
26 lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
27 by (simp add: diff_eq_eq diff_minus [symmetric])
29 lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
31 apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
36 CLIM :: "[complex=>complex,complex,complex] => bool"
37 ("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
40 (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
41 --> cmod(f x - L) < r)))"
43 NSCLIM :: "[complex=>complex,complex,complex] => bool"
44 ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
45 "f -- a --NSC> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
46 x @c= hcomplex_of_complex a
47 --> ( *fc* f) x @c= hcomplex_of_complex L))"
50 CRLIM :: "[complex=>real,complex,real] => bool"
51 ("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
54 (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
55 --> abs(f x - L) < r)))"
57 NSCRLIM :: "[complex=>real,complex,real] => bool"
58 ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
59 "f -- a --NSCR> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
60 x @c= hcomplex_of_complex a
61 --> ( *fcR* f) x @= hypreal_of_real L))"
64 isContc :: "[complex=>complex,complex] => bool"
65 "isContc f a == (f -- a --C> (f a))"
67 (* NS definition dispenses with limit notions *)
68 isNSContc :: "[complex=>complex,complex] => bool"
69 "isNSContc f a == (\<forall>y. y @c= hcomplex_of_complex a -->
70 ( *fc* f) y @c= hcomplex_of_complex (f a))"
72 isContCR :: "[complex=>real,complex] => bool"
73 "isContCR f a == (f -- a --CR> (f a))"
75 (* NS definition dispenses with limit notions *)
76 isNSContCR :: "[complex=>real,complex] => bool"
77 "isNSContCR f a == (\<forall>y. y @c= hcomplex_of_complex a -->
78 ( *fcR* f) y @= hypreal_of_real (f a))"
80 (* differentiation: D is derivative of function f at x *)
81 cderiv:: "[complex=>complex,complex,complex] => bool"
82 ("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
83 "CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
85 nscderiv :: "[complex=>complex,complex,complex] => bool"
86 ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
87 "NSCDERIV f x :> D == (\<forall>h \<in> CInfinitesimal - {0}.
88 (( *fc* f)(hcomplex_of_complex x + h)
89 - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)"
91 cdifferentiable :: "[complex=>complex,complex] => bool"
92 (infixl "cdifferentiable" 60)
93 "f cdifferentiable x == (\<exists>D. CDERIV f x :> D)"
95 NSCdifferentiable :: "[complex=>complex,complex] => bool"
96 (infixl "NSCdifferentiable" 60)
97 "f NSCdifferentiable x == (\<exists>D. NSCDERIV f x :> D)"
100 isUContc :: "(complex=>complex) => bool"
101 "isUContc f == (\<forall>r. 0 < r -->
102 (\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
103 --> cmod(f x - f y) < r)))"
105 isNSUContc :: "(complex=>complex) => bool"
106 "isNSUContc f == (\<forall>x y. x @c= y --> ( *fc* f) x @c= ( *fc* f) y)"
110 subsection{*Limit of Complex to Complex Function*}
112 lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
113 by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff
114 hRe_hcomplex_of_complex)
117 lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
118 by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff
119 hIm_hcomplex_of_complex)
122 "f -- x --C> L ==> f -- x --NSC> L"
123 apply (simp add: CLIM_def NSCLIM_def capprox_def, auto)
124 apply (rule_tac z = xa in eq_Abs_hcomplex)
125 apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff
126 CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
127 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
128 apply (drule_tac x = u in spec, auto)
129 apply (drule_tac x = s in spec, auto, ultra)
130 apply (drule sym, auto)
133 lemma eq_Abs_hcomplex_ALL:
134 "(\<forall>t. P t) = (\<forall>X. P (Abs_hcomplex(hcomplexrel `` {X})))"
136 apply (rule_tac z = t in eq_Abs_hcomplex, auto)
140 "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
141 cmod (xa - x) < s & r \<le> cmod (f xa - L))
142 ==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x &
143 cmod(xa - x) < inverse(real(Suc n)) & r \<le> cmod(f xa - L)"
145 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
149 lemma lemma_skolemize_CLIM2:
150 "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
151 cmod (xa - x) < s & r \<le> cmod (f xa - L))
152 ==> \<exists>X. \<forall>(n::nat). X n \<noteq> x &
153 cmod(X n - x) < inverse(real(Suc n)) & r \<le> cmod(f (X n) - L)"
154 apply (drule lemma_CLIM)
155 apply (drule choice, blast)
159 "\<forall>n. X n \<noteq> x &
160 cmod (X n - x) < inverse (real(Suc n)) &
161 r \<le> cmod (f (X n) - L) ==>
162 \<forall>n. cmod (X n - x) < inverse (real(Suc n))"
166 "f -- x --NSC> L ==> f -- x --C> L"
167 apply (simp add: CLIM_def NSCLIM_def)
169 apply (auto simp add: eq_Abs_hcomplex_ALL starfunC
170 CInfinitesimal_capprox_minus [symmetric] hcomplex_diff
171 CInfinitesimal_hcmod_iff hcomplex_of_complex_def
172 Infinitesimal_FreeUltrafilterNat_iff hcmod)
173 apply (simp add: linorder_not_less)
174 apply (drule lemma_skolemize_CLIM2, safe)
175 apply (drule_tac x = X in spec, auto)
176 apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
177 apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def
178 Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod, blast)
179 apply (drule_tac x = r in spec, clarify)
180 apply (drule FreeUltrafilterNat_all, ultra, arith)
184 text{*First key result*}
185 theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)"
186 by (blast intro: CLIM_NSCLIM NSCLIM_CLIM)
189 subsection{*Limit of Complex to Real Function*}
191 lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
192 apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto)
193 apply (rule_tac z = xa in eq_Abs_hcomplex)
194 apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
195 CInfinitesimal_hcmod_iff hcmod hypreal_diff
196 Infinitesimal_FreeUltrafilterNat_iff
197 Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
198 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
199 apply (drule_tac x = u in spec, auto)
200 apply (drule_tac x = s in spec, auto, ultra)
201 apply (drule sym, auto)
205 "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
206 cmod (xa - x) < s & r \<le> abs (f xa - L))
207 ==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x &
208 cmod(xa - x) < inverse(real(Suc n)) & r \<le> abs (f xa - L)"
210 apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
213 lemma lemma_skolemize_CRLIM2:
214 "\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x &
215 cmod (xa - x) < s & r \<le> abs (f xa - L))
216 ==> \<exists>X. \<forall>(n::nat). X n \<noteq> x &
217 cmod(X n - x) < inverse(real(Suc n)) & r \<le> abs (f (X n) - L)"
218 apply (drule lemma_CRLIM)
219 apply (drule choice, blast)
223 "\<forall>n. X n \<noteq> x &
224 cmod (X n - x) < inverse (real(Suc n)) &
225 r \<le> abs (f (X n) - L) ==>
226 \<forall>n. cmod (X n - x) < inverse (real(Suc n))"
229 lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
230 apply (simp add: CRLIM_def NSCRLIM_def capprox_def)
232 apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff
233 hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff
234 hcmod Infinitesimal_approx_minus [symmetric]
235 Infinitesimal_FreeUltrafilterNat_iff)
236 apply (simp add: linorder_not_less)
237 apply (drule lemma_skolemize_CRLIM2, safe)
238 apply (drule_tac x = X in spec, auto)
239 apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
240 apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def
241 Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod)
242 apply (auto simp add: hypreal_of_real_def hypreal_diff)
243 apply (drule_tac x = r in spec, clarify)
244 apply (drule FreeUltrafilterNat_all, ultra)
247 text{*Second key result*}
248 theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)"
249 by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM)
251 (** get this result easily now **)
252 lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"
253 by (auto dest: NSCLIM_NSCRLIM_Re simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
255 lemma CLIM_CRLIM_Im: "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)"
256 by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
258 lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"
259 by (simp add: CLIM_def complex_cnj_diff [symmetric])
261 lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"
262 by (simp add: CLIM_def complex_cnj_diff [symmetric])
264 (*** NSLIM_add hence CLIM_add *)
267 "[| f -- x --NSC> l; g -- x --NSC> m |]
268 ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"
269 by (auto simp: NSCLIM_def intro!: capprox_add)
272 "[| f -- x --C> l; g -- x --C> m |]
273 ==> (%x. f(x) + g(x)) -- x --C> (l + m)"
274 by (simp add: CLIM_NSCLIM_iff NSCLIM_add)
276 (*** NSLIM_mult hence CLIM_mult *)
279 "[| f -- x --NSC> l; g -- x --NSC> m |]
280 ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"
281 by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite)
284 "[| f -- x --C> l; g -- x --C> m |]
285 ==> (%x. f(x) * g(x)) -- x --C> (l * m)"
286 by (simp add: CLIM_NSCLIM_iff NSCLIM_mult)
288 (*** NSCLIM_const and CLIM_const ***)
290 lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k"
291 by (simp add: NSCLIM_def)
293 lemma CLIM_const [simp]: "(%x. k) -- x --C> k"
294 by (simp add: CLIM_def)
296 (*** NSCLIM_minus and CLIM_minus ***)
298 lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"
299 by (simp add: NSCLIM_def)
301 lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"
302 by (simp add: CLIM_NSCLIM_iff NSCLIM_minus)
304 (*** NSCLIM_diff hence CLIM_diff ***)
307 "[| f -- x --NSC> l; g -- x --NSC> m |]
308 ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"
309 by (simp add: diff_minus NSCLIM_add NSCLIM_minus)
312 "[| f -- x --C> l; g -- x --C> m |]
313 ==> (%x. f(x) - g(x)) -- x --C> (l - m)"
314 by (simp add: CLIM_NSCLIM_iff NSCLIM_diff)
316 (*** NSCLIM_inverse and hence CLIM_inverse *)
318 lemma NSCLIM_inverse:
319 "[| f -- a --NSC> L; L \<noteq> 0 |]
320 ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
321 apply (simp add: NSCLIM_def, clarify)
323 apply (force simp add: hcomplex_of_complex_capprox_inverse)
327 "[| f -- a --C> L; L \<noteq> 0 |]
328 ==> (%x. inverse(f(x))) -- a --C> (inverse L)"
329 by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse)
331 (*** NSCLIM_zero, CLIM_zero, etc. ***)
333 lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"
334 apply (simp add: diff_minus)
335 apply (rule_tac a1 = l in right_minus [THEN subst])
336 apply (rule NSCLIM_add, auto)
339 lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"
340 by (simp add: CLIM_NSCLIM_iff NSCLIM_zero)
342 lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"
343 by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto)
345 lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"
346 by (drule_tac g = "%x. l" and m = l in CLIM_add, auto)
348 (*** NSCLIM_not zero and hence CLIM_not_zero ***)
350 lemma NSCLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NSC> 0)"
351 apply (auto simp del: hcomplex_of_complex_zero simp add: NSCLIM_def)
352 apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI)
353 apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym]
354 simp del: hcomplex_of_complex_zero)
357 (* [| k \<noteq> 0; (%x. k) -- x --NSC> 0 |] ==> R *)
358 lemmas NSCLIM_not_zeroE = NSCLIM_not_zero [THEN notE, standard]
360 lemma CLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --C> 0)"
361 by (simp add: CLIM_NSCLIM_iff NSCLIM_not_zero)
363 (*** NSCLIM_const hence CLIM_const ***)
365 lemma NSCLIM_const_eq: "(%x. k) -- x --NSC> L ==> k = L"
367 apply (drule NSCLIM_zero)
368 apply (rule NSCLIM_not_zeroE [of "k-L"], auto)
371 lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L"
372 by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq)
374 (*** NSCLIM and hence CLIM are unique ***)
376 lemma NSCLIM_unique: "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M"
377 apply (drule NSCLIM_minus)
378 apply (drule NSCLIM_add, assumption)
379 apply (auto dest!: NSCLIM_const_eq [symmetric])
382 lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M"
383 by (simp add: CLIM_NSCLIM_iff NSCLIM_unique)
385 (*** NSCLIM_mult_zero and CLIM_mult_zero ***)
387 lemma NSCLIM_mult_zero:
388 "[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0"
389 by (drule NSCLIM_mult, auto)
391 lemma CLIM_mult_zero:
392 "[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0"
393 by (drule CLIM_mult, auto)
395 (*** NSCLIM_self hence CLIM_self ***)
397 lemma NSCLIM_self: "(%x. x) -- a --NSC> a"
398 by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox)
400 lemma CLIM_self: "(%x. x) -- a --C> a"
401 by (simp add: CLIM_NSCLIM_iff NSCLIM_self)
403 (** another equivalence result **)
404 lemma NSCLIM_NSCRLIM_iff:
405 "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
406 apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff)
407 apply (auto dest!: spec)
408 apply (rule_tac [!] z = xa in eq_Abs_hcomplex)
409 apply (auto simp add: hcomplex_diff starfunC starfunCR hcomplex_of_complex_def hcmod mem_infmal_iff)
412 (** much, much easier standard proof **)
413 lemma CLIM_CRLIM_iff: "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)"
414 by (simp add: CLIM_def CRLIM_def)
416 (* so this is nicer nonstandard proof *)
417 lemma NSCLIM_NSCRLIM_iff2:
418 "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
419 by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
421 lemma NSCLIM_NSCRLIM_Re_Im_iff:
422 "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) &
423 (%x. Im(f x)) -- a --NSCR> Im(L))"
424 apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im)
425 apply (auto simp add: NSCLIM_def NSCRLIM_def)
426 apply (auto dest!: spec)
427 apply (rule_tac z = x in eq_Abs_hcomplex)
428 apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
431 lemma CLIM_CRLIM_Re_Im_iff:
432 "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) &
433 (%x. Im(f x)) -- a --CR> Im(L))"
434 by (simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff NSCLIM_NSCRLIM_Re_Im_iff)
437 subsection{*Continuity*}
440 "[| isNSContc f a; y @c= hcomplex_of_complex a |]
441 ==> ( *fc* f) y @c= hcomplex_of_complex (f a)"
442 by (simp add: isNSContc_def)
444 lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) "
445 by (simp add: isNSContc_def NSCLIM_def)
447 lemma NSCLIM_isNSContc:
448 "f -- a --NSC> (f a) ==> isNSContc f a"
449 apply (simp add: isNSContc_def NSCLIM_def, auto)
450 apply (case_tac "y = hcomplex_of_complex a", auto)
453 text{*Nonstandard continuity can be defined using NS Limit in
454 similar fashion to standard definition of continuity*}
456 lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))"
457 by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc)
459 lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))"
460 by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff)
462 (*** key result for continuity ***)
463 lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)"
464 by (simp add: isContc_def isNSContc_CLIM_iff)
466 lemma isContc_isNSContc: "isContc f a ==> isNSContc f a"
467 by (erule isNSContc_isContc_iff [THEN iffD2])
469 lemma isNSContc_isContc: "isNSContc f a ==> isContc f a"
470 by (erule isNSContc_isContc_iff [THEN iffD1])
473 text{*Alternative definition of continuity*}
474 lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"
475 apply (simp add: NSCLIM_def, auto)
476 apply (drule_tac x = "hcomplex_of_complex a + x" in spec)
477 apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp)
478 apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]])
479 apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1])
480 prefer 3 apply (simp add: compare_rls hcomplex_add_commute)
481 apply (rule_tac [2] z = x in eq_Abs_hcomplex)
482 apply (rule_tac [4] z = x in eq_Abs_hcomplex)
483 apply (auto simp add: starfunC hcomplex_of_complex_def hcomplex_minus hcomplex_add)
486 lemma NSCLIM_isContc_iff:
487 "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"
488 by (rule NSCLIM_h_iff)
490 lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"
491 by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff)
493 lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"
494 by (simp add: isContc_def CLIM_isContc_iff)
497 "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"
498 by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
501 "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"
502 by (auto intro!: starfunC_mult_CFinite_capprox
503 simp del: starfunC_mult [symmetric]
504 simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
507 lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
508 by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
511 "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
512 by (auto dest: isContc_o simp add: o_def)
514 lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a"
515 by (simp add: isNSContc_def)
517 lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a"
518 by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus)
520 lemma isContc_inverse:
521 "[| isContc f x; f x \<noteq> 0 |] ==> isContc (%x. inverse (f x)) x"
522 by (simp add: isContc_def CLIM_inverse)
524 lemma isNSContc_inverse:
525 "[| isNSContc f x; f x \<noteq> 0 |] ==> isNSContc (%x. inverse (f x)) x"
526 by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff)
529 "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
530 apply (simp add: diff_minus)
531 apply (auto intro: isContc_add isContc_minus)
534 lemma isContc_const [simp]: "isContc (%x. k) a"
535 by (simp add: isContc_def)
537 lemma isNSContc_const [simp]: "isNSContc (%x. k) a"
538 by (simp add: isNSContc_def)
541 subsection{*Functions from Complex to Reals*}
544 "[| isNSContCR f a; y @c= hcomplex_of_complex a |]
545 ==> ( *fcR* f) y @= hypreal_of_real (f a)"
546 by (simp add: isNSContCR_def)
548 lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) "
549 by (simp add: isNSContCR_def NSCRLIM_def)
551 lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a"
552 apply (auto simp add: isNSContCR_def NSCRLIM_def)
553 apply (case_tac "y = hcomplex_of_complex a", auto)
556 lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))"
557 by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR)
559 lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))"
560 by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff)
562 (*** another key result for continuity ***)
563 lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)"
564 by (simp add: isContCR_def isNSContCR_CRLIM_iff)
566 lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a"
567 by (erule isNSContCR_isContCR_iff [THEN iffD2])
569 lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a"
570 by (erule isNSContCR_isContCR_iff [THEN iffD1])
572 lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)"
573 by (auto intro: capprox_hcmod_approx
574 simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric]
577 lemma isContCR_cmod [simp]: "isContCR cmod (a)"
578 by (simp add: isNSContCR_isContCR_iff [symmetric])
580 lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a"
581 by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re)
583 lemma isContc_isContCR_Im: "isContc f a ==> isContCR (%x. Im (f x)) a"
584 by (simp add: isContc_def isContCR_def CLIM_CRLIM_Im)
587 subsection{*Derivatives*}
589 lemma CDERIV_iff: "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
590 by (simp add: cderiv_def)
592 lemma CDERIV_NSC_iff:
593 "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
594 by (simp add: cderiv_def CLIM_NSCLIM_iff)
596 lemma CDERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D"
597 by (simp add: cderiv_def)
599 lemma NSC_DERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D"
600 by (simp add: cderiv_def CLIM_NSCLIM_iff)
603 lemma CDERIV_unique: "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E"
604 by (simp add: cderiv_def CLIM_unique)
606 (*** uniqueness: a nonstandard proof ***)
607 lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E"
608 apply (simp add: nscderiv_def)
609 apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"]
610 intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3)
614 subsection{* Differentiability*}
616 lemma CDERIV_CLIM_iff:
617 "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) =
618 ((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)"
619 apply (simp add: CLIM_def)
620 apply (rule_tac f=All in arg_cong)
622 apply (rule imp_cong)
624 apply (rule_tac f=Ex in arg_cong)
626 apply (rule conj_cong)
629 apply (rule all_shift [where a=a], simp)
633 "(CDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)"
634 by (simp add: cderiv_def CDERIV_CLIM_iff)
637 subsection{* Equivalence of NS and Standard Differentiation*}
639 (*** first equivalence ***)
640 lemma NSCDERIV_NSCLIM_iff:
641 "(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
642 apply (simp add: nscderiv_def NSCLIM_def, auto)
643 apply (drule_tac x = xa in bspec)
644 apply (rule_tac [3] ccontr)
645 apply (drule_tac [3] x = h in spec)
646 apply (auto simp add: mem_cinfmal_iff starfunC_lambda_cancel)
649 (*** 2nd equivalence ***)
650 lemma NSCDERIV_NSCLIM_iff2:
651 "(NSCDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)"
652 by (simp add: NSCDERIV_NSCLIM_iff CDERIV_CLIM_iff CLIM_NSCLIM_iff [symmetric])
655 "(NSCDERIV f x :> D) =
656 (\<forall>xa. xa \<noteq> hcomplex_of_complex x & xa @c= hcomplex_of_complex x -->
657 ( *fc* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"
658 by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
660 lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)"
661 by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff)
663 lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x"
664 apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus)
665 apply (drule capprox_minus_iff [THEN iffD1])
666 apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0")
667 prefer 2 apply (simp add: compare_rls)
668 apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
669 prefer 2 apply (simp add: hcomplex_add_assoc [symmetric])
670 apply (auto simp add: mem_cinfmal_iff [symmetric] hcomplex_add_commute)
671 apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
672 apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
673 simp add: mult_assoc)
674 apply (drule_tac x3 = D in
675 CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult,
676 THEN mem_cinfmal_iff [THEN iffD1]])
677 apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2])
680 lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x"
681 by (simp add: NSCDERIV_CDERIV_iff [symmetric] isNSContc_isContc_iff [symmetric] NSCDERIV_isNSContc)
683 text{* Differentiation rules for combinations of functions follow by clear,
684 straightforard algebraic manipulations*}
686 (* use simple constant nslimit theorem *)
687 lemma NSCDERIV_const [simp]: "(NSCDERIV (%x. k) x :> 0)"
688 by (simp add: NSCDERIV_NSCLIM_iff)
690 lemma CDERIV_const [simp]: "(CDERIV (%x. k) x :> 0)"
691 by (simp add: NSCDERIV_CDERIV_iff [symmetric])
694 "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
695 ==> NSCDERIV (%x. f x + g x) x :> Da + Db"
696 apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify)
697 apply (auto dest!: spec simp add: add_divide_distrib diff_minus)
698 apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add)
699 apply (auto simp add: add_ac)
703 "[| CDERIV f x :> Da; CDERIV g x :> Db |]
704 ==> CDERIV (%x. f x + g x) x :> Da + Db"
705 by (simp add: NSCDERIV_add NSCDERIV_CDERIV_iff [symmetric])
708 subsection{*Lemmas for Multiplication*}
710 lemma lemma_nscderiv1: "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
711 by (simp add: right_diff_distrib)
713 lemma lemma_nscderiv2:
714 "[| (x + y) / z = hcomplex_of_complex D + yb; z \<noteq> 0;
715 z : CInfinitesimal; yb : CInfinitesimal |]
717 apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption)
718 apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl)
719 apply (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add
720 simp add: mem_cinfmal_iff [symmetric])
721 apply (erule CInfinitesimal_subset_CFinite [THEN subsetD])
725 "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
726 ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
727 apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify)
728 apply (auto dest!: spec
729 simp add: starfunC_lambda_cancel lemma_nscderiv1)
730 apply (simp (no_asm) add: add_divide_distrib)
731 apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+
732 apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
733 apply (simp add: diff_minus)
734 apply (drule_tac D = Db in lemma_nscderiv2)
736 capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]])
737 apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc)
738 apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst])
739 apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym]
740 CInfinitesimal_add CInfinitesimal_mult
741 CInfinitesimal_hcomplex_of_complex_mult
742 CInfinitesimal_hcomplex_of_complex_mult2
743 simp add: hcomplex_add_assoc [symmetric])
747 "[| CDERIV f x :> Da; CDERIV g x :> Db |]
748 ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
749 by (simp add: NSCDERIV_mult NSCDERIV_CDERIV_iff [symmetric])
751 lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"
752 apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff
753 minus_mult_right right_distrib [symmetric] diff_minus
754 del: times_divide_eq_right minus_mult_right [symmetric])
755 apply (erule NSCLIM_const [THEN NSCLIM_mult])
758 lemma CDERIV_cmult: "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"
759 by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric])
761 lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"
762 apply (simp add: NSCDERIV_NSCLIM_iff diff_minus)
763 apply (rule_tac t = "f x" in minus_minus [THEN subst])
764 apply (simp (no_asm_simp) add: minus_add_distrib [symmetric]
765 del: minus_add_distrib minus_minus)
766 apply (erule NSCLIM_minus)
769 lemma CDERIV_minus: "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D"
770 by (simp add: NSCDERIV_minus NSCDERIV_CDERIV_iff [symmetric])
772 lemma NSCDERIV_add_minus:
773 "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
774 ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db"
775 by (blast dest: NSCDERIV_add NSCDERIV_minus)
777 lemma CDERIV_add_minus:
778 "[| CDERIV f x :> Da; CDERIV g x :> Db |]
779 ==> CDERIV (%x. f x + -g x) x :> Da + -Db"
780 by (blast dest: CDERIV_add CDERIV_minus)
783 "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
784 ==> NSCDERIV (%x. f x - g x) x :> Da - Db"
785 by (simp add: diff_minus NSCDERIV_add_minus)
788 "[| CDERIV f x :> Da; CDERIV g x :> Db |]
789 ==> CDERIV (%x. f x - g x) x :> Da - Db"
790 by (simp add: diff_minus CDERIV_add_minus)
793 subsection{*Chain Rule*}
797 "[| NSCDERIV g x :> D;
798 ( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);
799 xa : CInfinitesimal; xa \<noteq> 0
801 apply (simp add: nscderiv_def)
802 apply (drule bspec, auto)
805 lemma NSCDERIV_capprox:
806 "[| NSCDERIV f x :> D; h: CInfinitesimal; h \<noteq> 0 |]
807 ==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0"
808 apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric])
809 apply (rule CInfinitesimal_ratio)
810 apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto)
814 (*--------------------------------------------------*)
815 (* from one version of differentiability *)
818 (* --------------- @= Db *)
820 (* -------------------------------------------------*)
823 "[| NSCDERIV f (g x) :> Da;
824 ( *fc* g) (hcomplex_of_complex(x) + xa) \<noteq> hcomplex_of_complex (g x);
825 ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|]
826 ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa))
827 - hcomplex_of_complex (f (g x))) /
828 (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x))
829 @c= hcomplex_of_complex (Da)"
830 by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
832 (*--------------------------------------------------*)
833 (* from other version of differentiability *)
835 (* f(x + h) - f(x) *)
836 (* ----------------- @= Db *)
838 (*--------------------------------------------------*)
841 "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |]
842 ==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa
843 @c= hcomplex_of_complex (Db)"
844 by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
846 lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
851 theorem NSCDERIV_chain:
852 "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |]
853 ==> NSCDERIV (f o g) x :> Da * Db"
854 apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric])
856 apply (frule_tac f = g in NSCDERIV_capprox)
857 apply (auto simp add: starfunC_lambda_cancel2 starfunC_o [symmetric])
858 apply (case_tac "( *fc* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ")
859 apply (drule_tac g = g in NSCDERIV_zero)
860 apply (auto simp add: hcomplex_divide_def)
861 apply (rule_tac z1 = "( *fc* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst])
862 apply (simp (no_asm_simp))
863 apply (rule capprox_mult_hcomplex_of_complex)
864 apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2]
865 simp add: diff_minus [symmetric] divide_inverse [symmetric])
866 apply (blast intro: NSCDERIVD2)
869 text{*standard version*}
871 "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
872 ==> CDERIV (f o g) x :> Da * Db"
873 by (simp add: NSCDERIV_CDERIV_iff [symmetric] NSCDERIV_chain)
876 "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
877 ==> CDERIV (%x. f (g x)) x :> Da * Db"
878 by (auto dest: CDERIV_chain simp add: o_def)
881 subsection{* Differentiation of Natural Number Powers*}
883 lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1"
884 by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def)
886 lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1"
887 by (simp add: NSCDERIV_CDERIV_iff [symmetric])
889 lemmas isContc_Id = CDERIV_Id [THEN CDERIV_isContc, standard]
891 text{*derivative of linear multiplication*}
892 lemma CDERIV_cmult_Id [simp]: "CDERIV (op * c) x :> c"
893 by (cut_tac c = c and x = x in CDERIV_Id [THEN CDERIV_cmult], simp)
895 lemma NSCDERIV_cmult_Id [simp]: "NSCDERIV (op * c) x :> c"
896 by (simp add: NSCDERIV_CDERIV_iff)
898 lemma CDERIV_pow [simp]:
899 "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
900 apply (induct_tac "n")
901 apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
902 apply (auto simp add: complex_of_real_add [symmetric] left_distrib real_of_nat_Suc)
904 apply (auto simp add: mult_ac add_commute)
907 text{*Nonstandard version*}
909 "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
910 by (simp add: NSCDERIV_CDERIV_iff)
912 lemma lemma_CDERIV_subst:
913 "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E"
916 (*used once, in NSCDERIV_inverse*)
917 lemma CInfinitesimal_add_not_zero:
918 "[| h: CInfinitesimal; x \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0"
920 apply (drule equals_zero_I, auto)
923 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
924 lemma NSCDERIV_inverse:
925 "x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
926 apply (simp add: nscderiv_def Ball_def, clarify)
927 apply (frule CInfinitesimal_add_not_zero [where x=x])
928 apply (auto simp add: starfunC_inverse_inverse diff_minus
929 simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
930 apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
931 inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
933 del: inverse_minus_eq inverse_mult_distrib minus_mult_right [symmetric] minus_mult_left [symmetric])
934 apply (simp only: mult_assoc [symmetric] right_distrib)
935 apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
936 apply (rule inverse_add_CInfinitesimal_capprox2)
937 apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal
939 simp add: inverse_minus_eq [symmetric])
940 apply (rule CInfinitesimal_CFinite_mult2, auto)
943 lemma CDERIV_inverse:
944 "x \<noteq> 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
945 by (simp add: NSCDERIV_inverse NSCDERIV_CDERIV_iff [symmetric]
949 subsection{*Derivative of Reciprocals (Function @{term inverse})*}
951 lemma CDERIV_inverse_fun:
952 "[| CDERIV f x :> d; f(x) \<noteq> 0 |]
953 ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
954 apply (rule mult_commute [THEN subst])
955 apply (simp (no_asm_simp) add: minus_mult_left power_inverse del: complexpow_Suc minus_mult_left [symmetric])
957 apply (blast intro!: CDERIV_chain CDERIV_inverse)
960 lemma NSCDERIV_inverse_fun:
961 "[| NSCDERIV f x :> d; f(x) \<noteq> 0 |]
962 ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
963 by (simp add: NSCDERIV_CDERIV_iff CDERIV_inverse_fun del: complexpow_Suc)
966 subsection{* Derivative of Quotient*}
968 lemma CDERIV_quotient:
969 "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |]
970 ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
971 apply (simp add: diff_minus)
972 apply (drule_tac f = g in CDERIV_inverse_fun)
973 apply (drule_tac [2] CDERIV_mult, assumption+)
974 apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
976 del: minus_mult_right [symmetric] minus_mult_left [symmetric]
980 lemma NSCDERIV_quotient:
981 "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) \<noteq> 0 |]
982 ==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
983 by (simp add: NSCDERIV_CDERIV_iff CDERIV_quotient del: complexpow_Suc)
986 subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
989 "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --C> l) = (g -- a --C> l)"
990 by (simp add: CLIM_def complex_add_minus_iff)
993 "[| (%x. f(x) + -g(x)) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l"
994 apply (drule CLIM_add, assumption)
995 apply (simp add: complex_add_assoc)
1000 (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isContc g x & g x = l)"
1002 apply (rule_tac x = "%z. if z=x then l else (f (z) - f (x)) / (z-x)" in exI)
1003 apply (auto simp add: mult_assoc isContc_iff CDERIV_iff)
1004 apply (rule_tac [!] CLIM_equal [THEN iffD1], auto)
1008 lemma CARAT_NSCDERIV:
1009 "NSCDERIV f x :> l ==>
1010 \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
1011 by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
1013 (* FIXME tidy! How about a NS proof? *)
1014 lemma CARAT_CDERIVD:
1015 "(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
1016 ==> NSCDERIV f x :> l"
1017 apply (simp only: NSCDERIV_iff2)
1018 apply (tactic {*(auto_tac (claset(),
1019 simpset() delsimprocs field_cancel_factor
1020 addsimps [thm"NSCDERIV_iff2"])) *})
1021 apply (simp add: isNSContc_def)
1026 val complex_add_minus_iff = thm "complex_add_minus_iff";
1027 val complex_add_eq_0_iff = thm "complex_add_eq_0_iff";
1028 val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re";
1029 val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im";
1030 val CLIM_NSCLIM = thm "CLIM_NSCLIM";
1031 val eq_Abs_hcomplex_ALL = thm "eq_Abs_hcomplex_ALL";
1032 val lemma_CLIM = thm "lemma_CLIM";
1033 val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2";
1034 val lemma_csimp = thm "lemma_csimp";
1035 val NSCLIM_CLIM = thm "NSCLIM_CLIM";
1036 val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff";
1037 val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM";
1038 val lemma_CRLIM = thm "lemma_CRLIM";
1039 val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2";
1040 val lemma_crsimp = thm "lemma_crsimp";
1041 val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM";
1042 val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff";
1043 val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re";
1044 val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im";
1045 val CLIM_cnj = thm "CLIM_cnj";
1046 val CLIM_cnj_iff = thm "CLIM_cnj_iff";
1047 val NSCLIM_add = thm "NSCLIM_add";
1048 val CLIM_add = thm "CLIM_add";
1049 val NSCLIM_mult = thm "NSCLIM_mult";
1050 val CLIM_mult = thm "CLIM_mult";
1051 val NSCLIM_const = thm "NSCLIM_const";
1052 val CLIM_const = thm "CLIM_const";
1053 val NSCLIM_minus = thm "NSCLIM_minus";
1054 val CLIM_minus = thm "CLIM_minus";
1055 val NSCLIM_diff = thm "NSCLIM_diff";
1056 val CLIM_diff = thm "CLIM_diff";
1057 val NSCLIM_inverse = thm "NSCLIM_inverse";
1058 val CLIM_inverse = thm "CLIM_inverse";
1059 val NSCLIM_zero = thm "NSCLIM_zero";
1060 val CLIM_zero = thm "CLIM_zero";
1061 val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel";
1062 val CLIM_zero_cancel = thm "CLIM_zero_cancel";
1063 val NSCLIM_not_zero = thm "NSCLIM_not_zero";
1064 val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE";
1065 val CLIM_not_zero = thm "CLIM_not_zero";
1066 val NSCLIM_const_eq = thm "NSCLIM_const_eq";
1067 val CLIM_const_eq = thm "CLIM_const_eq";
1068 val NSCLIM_unique = thm "NSCLIM_unique";
1069 val CLIM_unique = thm "CLIM_unique";
1070 val NSCLIM_mult_zero = thm "NSCLIM_mult_zero";
1071 val CLIM_mult_zero = thm "CLIM_mult_zero";
1072 val NSCLIM_self = thm "NSCLIM_self";
1073 val CLIM_self = thm "CLIM_self";
1074 val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff";
1075 val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff";
1076 val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2";
1077 val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff";
1078 val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff";
1079 val isNSContcD = thm "isNSContcD";
1080 val isNSContc_NSCLIM = thm "isNSContc_NSCLIM";
1081 val NSCLIM_isNSContc = thm "NSCLIM_isNSContc";
1082 val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff";
1083 val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff";
1084 val isNSContc_isContc_iff = thm "isNSContc_isContc_iff";
1085 val isContc_isNSContc = thm "isContc_isNSContc";
1086 val isNSContc_isContc = thm "isNSContc_isContc";
1087 val NSCLIM_h_iff = thm "NSCLIM_h_iff";
1088 val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff";
1089 val CLIM_isContc_iff = thm "CLIM_isContc_iff";
1090 val isContc_iff = thm "isContc_iff";
1091 val isContc_add = thm "isContc_add";
1092 val isContc_mult = thm "isContc_mult";
1093 val isContc_o = thm "isContc_o";
1094 val isContc_o2 = thm "isContc_o2";
1095 val isNSContc_minus = thm "isNSContc_minus";
1096 val isContc_minus = thm "isContc_minus";
1097 val isContc_inverse = thm "isContc_inverse";
1098 val isNSContc_inverse = thm "isNSContc_inverse";
1099 val isContc_diff = thm "isContc_diff";
1100 val isContc_const = thm "isContc_const";
1101 val isNSContc_const = thm "isNSContc_const";
1102 val isNSContCRD = thm "isNSContCRD";
1103 val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM";
1104 val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR";
1105 val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff";
1106 val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff";
1107 val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff";
1108 val isContCR_isNSContCR = thm "isContCR_isNSContCR";
1109 val isNSContCR_isContCR = thm "isNSContCR_isContCR";
1110 val isNSContCR_cmod = thm "isNSContCR_cmod";
1111 val isContCR_cmod = thm "isContCR_cmod";
1112 val isContc_isContCR_Re = thm "isContc_isContCR_Re";
1113 val isContc_isContCR_Im = thm "isContc_isContCR_Im";
1114 val CDERIV_iff = thm "CDERIV_iff";
1115 val CDERIV_NSC_iff = thm "CDERIV_NSC_iff";
1116 val CDERIVD = thm "CDERIVD";
1117 val NSC_DERIVD = thm "NSC_DERIVD";
1118 val CDERIV_unique = thm "CDERIV_unique";
1119 val NSCDeriv_unique = thm "NSCDeriv_unique";
1120 val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff";
1121 val CDERIV_iff2 = thm "CDERIV_iff2";
1122 val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff";
1123 val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2";
1124 val NSCDERIV_iff2 = thm "NSCDERIV_iff2";
1125 val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff";
1126 val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc";
1127 val CDERIV_isContc = thm "CDERIV_isContc";
1128 val NSCDERIV_const = thm "NSCDERIV_const";
1129 val CDERIV_const = thm "CDERIV_const";
1130 val NSCDERIV_add = thm "NSCDERIV_add";
1131 val CDERIV_add = thm "CDERIV_add";
1132 val lemma_nscderiv1 = thm "lemma_nscderiv1";
1133 val lemma_nscderiv2 = thm "lemma_nscderiv2";
1134 val NSCDERIV_mult = thm "NSCDERIV_mult";
1135 val CDERIV_mult = thm "CDERIV_mult";
1136 val NSCDERIV_cmult = thm "NSCDERIV_cmult";
1137 val CDERIV_cmult = thm "CDERIV_cmult";
1138 val NSCDERIV_minus = thm "NSCDERIV_minus";
1139 val CDERIV_minus = thm "CDERIV_minus";
1140 val NSCDERIV_add_minus = thm "NSCDERIV_add_minus";
1141 val CDERIV_add_minus = thm "CDERIV_add_minus";
1142 val NSCDERIV_diff = thm "NSCDERIV_diff";
1143 val CDERIV_diff = thm "CDERIV_diff";
1144 val NSCDERIV_zero = thm "NSCDERIV_zero";
1145 val NSCDERIV_capprox = thm "NSCDERIV_capprox";
1146 val NSCDERIVD1 = thm "NSCDERIVD1";
1147 val NSCDERIVD2 = thm "NSCDERIVD2";
1148 val lemma_complex_chain = thm "lemma_complex_chain";
1149 val NSCDERIV_chain = thm "NSCDERIV_chain";
1150 val CDERIV_chain = thm "CDERIV_chain";
1151 val CDERIV_chain2 = thm "CDERIV_chain2";
1152 val NSCDERIV_Id = thm "NSCDERIV_Id";
1153 val CDERIV_Id = thm "CDERIV_Id";
1154 val isContc_Id = thms "isContc_Id";
1155 val CDERIV_cmult_Id = thm "CDERIV_cmult_Id";
1156 val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id";
1157 val CDERIV_pow = thm "CDERIV_pow";
1158 val NSCDERIV_pow = thm "NSCDERIV_pow";
1159 val lemma_CDERIV_subst = thm "lemma_CDERIV_subst";
1160 val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero";
1161 val NSCDERIV_inverse = thm "NSCDERIV_inverse";
1162 val CDERIV_inverse = thm "CDERIV_inverse";
1163 val CDERIV_inverse_fun = thm "CDERIV_inverse_fun";
1164 val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun";
1165 val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared";
1166 val CDERIV_quotient = thm "CDERIV_quotient";
1167 val NSCDERIV_quotient = thm "NSCDERIV_quotient";
1168 val CLIM_equal = thm "CLIM_equal";
1169 val CLIM_trans = thm "CLIM_trans";
1170 val CARAT_CDERIV = thm "CARAT_CDERIV";
1171 val CARAT_NSCDERIV = thm "CARAT_NSCDERIV";
1172 val CARAT_CDERIVD = thm "CARAT_CDERIVD";