author | wenzelm |
Fri, 02 Jun 2006 23:22:29 +0200 | |
changeset 19765 | dfe940911617 |
parent 19233 | 77ca20b0ed77 |
child 20217 | 25b068a99d2b |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : CLim.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2001 University of Edinburgh |
|
14469 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13957 | 5 |
*) |
6 |
||
14469 | 7 |
header{*Limits, Continuity and Differentiation for Complex Functions*} |
8 |
||
15131 | 9 |
theory CLim |
15140 | 10 |
imports CSeries |
15131 | 11 |
begin |
14405 | 12 |
|
13 |
(*not in simpset?*) |
|
14 |
declare hypreal_epsilon_not_zero [simp] |
|
15 |
||
16 |
(*??generalize*) |
|
17 |
lemma lemma_complex_mult_inverse_squared [simp]: |
|
18 |
"x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x" |
|
14469 | 19 |
by (simp add: numeral_2_eq_2) |
14405 | 20 |
|
21 |
text{*Changing the quantified variable. Install earlier?*} |
|
14738 | 22 |
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"; |
14405 | 23 |
apply auto |
24 |
apply (drule_tac x="x+a" in spec) |
|
25 |
apply (simp add: diff_minus add_assoc) |
|
26 |
done |
|
27 |
||
28 |
lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)" |
|
29 |
by (simp add: diff_eq_eq diff_minus [symmetric]) |
|
30 |
||
31 |
lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)" |
|
32 |
apply auto |
|
33 |
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto) |
|
34 |
done |
|
13957 | 35 |
|
19765 | 36 |
definition |
13957 | 37 |
|
14405 | 38 |
CLIM :: "[complex=>complex,complex,complex] => bool" |
13957 | 39 |
("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60) |
19765 | 40 |
"f -- a --C> L = |
41 |
(\<forall>r. 0 < r --> |
|
14405 | 42 |
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s) |
19765 | 43 |
--> cmod(f x - L) < r))))" |
13957 | 44 |
|
14405 | 45 |
NSCLIM :: "[complex=>complex,complex,complex] => bool" |
13957 | 46 |
("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60) |
19765 | 47 |
"f -- a --NSC> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a & |
14405 | 48 |
x @c= hcomplex_of_complex a |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
49 |
--> ( *f* f) x @c= hcomplex_of_complex L))" |
13957 | 50 |
|
51 |
(* f: C --> R *) |
|
14405 | 52 |
CRLIM :: "[complex=>real,complex,real] => bool" |
13957 | 53 |
("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60) |
19765 | 54 |
"f -- a --CR> L = |
55 |
(\<forall>r. 0 < r --> |
|
14405 | 56 |
(\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s) |
19765 | 57 |
--> abs(f x - L) < r))))" |
13957 | 58 |
|
14405 | 59 |
NSCRLIM :: "[complex=>real,complex,real] => bool" |
13957 | 60 |
("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60) |
19765 | 61 |
"f -- a --NSCR> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a & |
14405 | 62 |
x @c= hcomplex_of_complex a |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
63 |
--> ( *f* f) x @= hypreal_of_real L))" |
13957 | 64 |
|
65 |
||
14405 | 66 |
isContc :: "[complex=>complex,complex] => bool" |
19765 | 67 |
"isContc f a = (f -- a --C> (f a))" |
13957 | 68 |
|
69 |
(* NS definition dispenses with limit notions *) |
|
14405 | 70 |
isNSContc :: "[complex=>complex,complex] => bool" |
19765 | 71 |
"isNSContc f a = (\<forall>y. y @c= hcomplex_of_complex a --> |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
72 |
( *f* f) y @c= hcomplex_of_complex (f a))" |
13957 | 73 |
|
14405 | 74 |
isContCR :: "[complex=>real,complex] => bool" |
19765 | 75 |
"isContCR f a = (f -- a --CR> (f a))" |
13957 | 76 |
|
77 |
(* NS definition dispenses with limit notions *) |
|
14405 | 78 |
isNSContCR :: "[complex=>real,complex] => bool" |
19765 | 79 |
"isNSContCR f a = (\<forall>y. y @c= hcomplex_of_complex a --> |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
80 |
( *f* f) y @= hypreal_of_real (f a))" |
13957 | 81 |
|
82 |
(* differentiation: D is derivative of function f at x *) |
|
14405 | 83 |
cderiv:: "[complex=>complex,complex,complex] => bool" |
13957 | 84 |
("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
19765 | 85 |
"CDERIV f x :> D = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)" |
13957 | 86 |
|
14405 | 87 |
nscderiv :: "[complex=>complex,complex,complex] => bool" |
13957 | 88 |
("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) |
19765 | 89 |
"NSCDERIV f x :> D = (\<forall>h \<in> CInfinitesimal - {0}. |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
90 |
(( *f* f)(hcomplex_of_complex x + h) |
13957 | 91 |
- hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)" |
92 |
||
14405 | 93 |
cdifferentiable :: "[complex=>complex,complex] => bool" |
94 |
(infixl "cdifferentiable" 60) |
|
19765 | 95 |
"f cdifferentiable x = (\<exists>D. CDERIV f x :> D)" |
14405 | 96 |
|
97 |
NSCdifferentiable :: "[complex=>complex,complex] => bool" |
|
98 |
(infixl "NSCdifferentiable" 60) |
|
19765 | 99 |
"f NSCdifferentiable x = (\<exists>D. NSCDERIV f x :> D)" |
14405 | 100 |
|
101 |
||
102 |
isUContc :: "(complex=>complex) => bool" |
|
19765 | 103 |
"isUContc f = (\<forall>r. 0 < r --> |
14405 | 104 |
(\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s |
105 |
--> cmod(f x - f y) < r)))" |
|
106 |
||
107 |
isNSUContc :: "(complex=>complex) => bool" |
|
19765 | 108 |
"isNSUContc f = (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)" |
14405 | 109 |
|
110 |
||
111 |
||
112 |
subsection{*Limit of Complex to Complex Function*} |
|
113 |
||
114 |
lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)" |
|
14469 | 115 |
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff |
116 |
hRe_hcomplex_of_complex) |
|
117 |
||
14405 | 118 |
|
14469 | 119 |
lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)" |
120 |
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff |
|
121 |
hIm_hcomplex_of_complex) |
|
14405 | 122 |
|
123 |
lemma CLIM_NSCLIM: |
|
124 |
"f -- x --C> L ==> f -- x --NSC> L" |
|
14469 | 125 |
apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
126 |
apply (rule_tac x = xa in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
127 |
apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff |
14405 | 128 |
CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
129 |
apply (rule bexI [OF _ Rep_star_star_n], safe) |
14405 | 130 |
apply (drule_tac x = u in spec, auto) |
131 |
apply (drule_tac x = s in spec, auto, ultra) |
|
132 |
apply (drule sym, auto) |
|
133 |
done |
|
134 |
||
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
135 |
lemma eq_Abs_star_ALL: "(\<forall>t. P t) = (\<forall>X. P (star_n X))" |
14405 | 136 |
apply auto |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
137 |
apply (rule_tac x = t in star_cases, auto) |
14405 | 138 |
done |
139 |
||
140 |
lemma lemma_CLIM: |
|
141 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
142 |
cmod (xa - x) < s & r \<le> cmod (f xa - L)) |
|
143 |
==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x & |
|
144 |
cmod(xa - x) < inverse(real(Suc n)) & r \<le> cmod(f xa - L)" |
|
145 |
apply clarify |
|
146 |
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
|
147 |
done |
|
148 |
||
149 |
||
150 |
lemma lemma_skolemize_CLIM2: |
|
151 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
152 |
cmod (xa - x) < s & r \<le> cmod (f xa - L)) |
|
153 |
==> \<exists>X. \<forall>(n::nat). X n \<noteq> x & |
|
154 |
cmod(X n - x) < inverse(real(Suc n)) & r \<le> cmod(f (X n) - L)" |
|
155 |
apply (drule lemma_CLIM) |
|
156 |
apply (drule choice, blast) |
|
157 |
done |
|
158 |
||
159 |
lemma lemma_csimp: |
|
160 |
"\<forall>n. X n \<noteq> x & |
|
161 |
cmod (X n - x) < inverse (real(Suc n)) & |
|
162 |
r \<le> cmod (f (X n) - L) ==> |
|
163 |
\<forall>n. cmod (X n - x) < inverse (real(Suc n))" |
|
164 |
by auto |
|
165 |
||
166 |
lemma NSCLIM_CLIM: |
|
167 |
"f -- x --NSC> L ==> f -- x --C> L" |
|
14469 | 168 |
apply (simp add: CLIM_def NSCLIM_def) |
14405 | 169 |
apply (rule ccontr) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
170 |
apply (auto simp add: eq_Abs_star_ALL starfun |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
171 |
CInfinitesimal_capprox_minus [symmetric] star_n_diff |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
172 |
CInfinitesimal_hcmod_iff star_of_def star_n_eq_iff |
14469 | 173 |
Infinitesimal_FreeUltrafilterNat_iff hcmod) |
14405 | 174 |
apply (simp add: linorder_not_less) |
175 |
apply (drule lemma_skolemize_CLIM2, safe) |
|
176 |
apply (drule_tac x = X in spec, auto) |
|
177 |
apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
178 |
apply (simp add: CInfinitesimal_hcmod_iff star_of_def |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
179 |
Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod, blast) |
14405 | 180 |
apply (drule_tac x = r in spec, clarify) |
181 |
apply (drule FreeUltrafilterNat_all, ultra, arith) |
|
182 |
done |
|
183 |
||
184 |
||
185 |
text{*First key result*} |
|
186 |
theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)" |
|
187 |
by (blast intro: CLIM_NSCLIM NSCLIM_CLIM) |
|
188 |
||
189 |
||
190 |
subsection{*Limit of Complex to Real Function*} |
|
191 |
||
192 |
lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L" |
|
14469 | 193 |
apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
194 |
apply (rule_tac x = xa in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
195 |
apply (auto simp add: starfun star_n_diff |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
196 |
CInfinitesimal_hcmod_iff hcmod |
14469 | 197 |
Infinitesimal_FreeUltrafilterNat_iff |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
198 |
star_of_def star_n_eq_iff |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
199 |
Infinitesimal_approx_minus [symmetric]) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
200 |
apply (rule bexI [OF _ Rep_star_star_n], safe) |
14405 | 201 |
apply (drule_tac x = u in spec, auto) |
202 |
apply (drule_tac x = s in spec, auto, ultra) |
|
203 |
apply (drule sym, auto) |
|
204 |
done |
|
205 |
||
206 |
lemma lemma_CRLIM: |
|
207 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
208 |
cmod (xa - x) < s & r \<le> abs (f xa - L)) |
|
209 |
==> \<forall>(n::nat). \<exists>xa. xa \<noteq> x & |
|
210 |
cmod(xa - x) < inverse(real(Suc n)) & r \<le> abs (f xa - L)" |
|
211 |
apply clarify |
|
212 |
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) |
|
213 |
done |
|
214 |
||
215 |
lemma lemma_skolemize_CRLIM2: |
|
216 |
"\<forall>s. 0 < s --> (\<exists>xa. xa \<noteq> x & |
|
217 |
cmod (xa - x) < s & r \<le> abs (f xa - L)) |
|
218 |
==> \<exists>X. \<forall>(n::nat). X n \<noteq> x & |
|
219 |
cmod(X n - x) < inverse(real(Suc n)) & r \<le> abs (f (X n) - L)" |
|
220 |
apply (drule lemma_CRLIM) |
|
221 |
apply (drule choice, blast) |
|
222 |
done |
|
223 |
||
224 |
lemma lemma_crsimp: |
|
225 |
"\<forall>n. X n \<noteq> x & |
|
226 |
cmod (X n - x) < inverse (real(Suc n)) & |
|
227 |
r \<le> abs (f (X n) - L) ==> |
|
228 |
\<forall>n. cmod (X n - x) < inverse (real(Suc n))" |
|
229 |
by auto |
|
230 |
||
231 |
lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L" |
|
14469 | 232 |
apply (simp add: CRLIM_def NSCRLIM_def capprox_def) |
14405 | 233 |
apply (rule ccontr) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
234 |
apply (auto simp add: eq_Abs_star_ALL starfun star_n_diff |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
235 |
CInfinitesimal_hcmod_iff |
17300 | 236 |
hcmod Infinitesimal_approx_minus [symmetric] |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
237 |
star_of_def star_n_eq_iff |
14405 | 238 |
Infinitesimal_FreeUltrafilterNat_iff) |
239 |
apply (simp add: linorder_not_less) |
|
240 |
apply (drule lemma_skolemize_CRLIM2, safe) |
|
241 |
apply (drule_tac x = X in spec, auto) |
|
242 |
apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
243 |
apply (simp add: CInfinitesimal_hcmod_iff star_of_def |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
244 |
Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
245 |
apply (auto simp add: star_of_def star_n_diff) |
14405 | 246 |
apply (drule_tac x = r in spec, clarify) |
247 |
apply (drule FreeUltrafilterNat_all, ultra) |
|
248 |
done |
|
249 |
||
250 |
text{*Second key result*} |
|
251 |
theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)" |
|
252 |
by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM) |
|
253 |
||
254 |
(** get this result easily now **) |
|
255 |
lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)" |
|
256 |
by (auto dest: NSCLIM_NSCRLIM_Re simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric]) |
|
257 |
||
258 |
lemma CLIM_CRLIM_Im: "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)" |
|
259 |
by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric]) |
|
260 |
||
261 |
lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L" |
|
14469 | 262 |
by (simp add: CLIM_def complex_cnj_diff [symmetric]) |
14405 | 263 |
|
264 |
lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)" |
|
14469 | 265 |
by (simp add: CLIM_def complex_cnj_diff [symmetric]) |
14405 | 266 |
|
267 |
(*** NSLIM_add hence CLIM_add *) |
|
268 |
||
269 |
lemma NSCLIM_add: |
|
270 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
271 |
==> (%x. f(x) + g(x)) -- x --NSC> (l + m)" |
|
272 |
by (auto simp: NSCLIM_def intro!: capprox_add) |
|
273 |
||
274 |
lemma CLIM_add: |
|
275 |
"[| f -- x --C> l; g -- x --C> m |] |
|
276 |
==> (%x. f(x) + g(x)) -- x --C> (l + m)" |
|
277 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_add) |
|
278 |
||
279 |
(*** NSLIM_mult hence CLIM_mult *) |
|
280 |
||
281 |
lemma NSCLIM_mult: |
|
282 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
283 |
==> (%x. f(x) * g(x)) -- x --NSC> (l * m)" |
|
284 |
by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite) |
|
285 |
||
286 |
lemma CLIM_mult: |
|
287 |
"[| f -- x --C> l; g -- x --C> m |] |
|
288 |
==> (%x. f(x) * g(x)) -- x --C> (l * m)" |
|
289 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_mult) |
|
290 |
||
291 |
(*** NSCLIM_const and CLIM_const ***) |
|
292 |
||
293 |
lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k" |
|
294 |
by (simp add: NSCLIM_def) |
|
295 |
||
296 |
lemma CLIM_const [simp]: "(%x. k) -- x --C> k" |
|
297 |
by (simp add: CLIM_def) |
|
298 |
||
299 |
(*** NSCLIM_minus and CLIM_minus ***) |
|
300 |
||
301 |
lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L" |
|
302 |
by (simp add: NSCLIM_def) |
|
303 |
||
304 |
lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L" |
|
305 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_minus) |
|
306 |
||
307 |
(*** NSCLIM_diff hence CLIM_diff ***) |
|
308 |
||
309 |
lemma NSCLIM_diff: |
|
310 |
"[| f -- x --NSC> l; g -- x --NSC> m |] |
|
311 |
==> (%x. f(x) - g(x)) -- x --NSC> (l - m)" |
|
14469 | 312 |
by (simp add: diff_minus NSCLIM_add NSCLIM_minus) |
14405 | 313 |
|
314 |
lemma CLIM_diff: |
|
315 |
"[| f -- x --C> l; g -- x --C> m |] |
|
316 |
==> (%x. f(x) - g(x)) -- x --C> (l - m)" |
|
317 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_diff) |
|
318 |
||
319 |
(*** NSCLIM_inverse and hence CLIM_inverse *) |
|
320 |
||
321 |
lemma NSCLIM_inverse: |
|
322 |
"[| f -- a --NSC> L; L \<noteq> 0 |] |
|
323 |
==> (%x. inverse(f(x))) -- a --NSC> (inverse L)" |
|
14469 | 324 |
apply (simp add: NSCLIM_def, clarify) |
14405 | 325 |
apply (drule spec) |
14469 | 326 |
apply (force simp add: hcomplex_of_complex_capprox_inverse) |
14405 | 327 |
done |
328 |
||
329 |
lemma CLIM_inverse: |
|
330 |
"[| f -- a --C> L; L \<noteq> 0 |] |
|
331 |
==> (%x. inverse(f(x))) -- a --C> (inverse L)" |
|
332 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse) |
|
333 |
||
334 |
(*** NSCLIM_zero, CLIM_zero, etc. ***) |
|
335 |
||
336 |
lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0" |
|
14469 | 337 |
apply (simp add: diff_minus) |
14405 | 338 |
apply (rule_tac a1 = l in right_minus [THEN subst]) |
14469 | 339 |
apply (rule NSCLIM_add, auto) |
14405 | 340 |
done |
341 |
||
342 |
lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0" |
|
343 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_zero) |
|
344 |
||
345 |
lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l" |
|
346 |
by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto) |
|
347 |
||
348 |
lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l" |
|
349 |
by (drule_tac g = "%x. l" and m = l in CLIM_add, auto) |
|
350 |
||
351 |
(*** NSCLIM_not zero and hence CLIM_not_zero ***) |
|
13957 | 352 |
|
14405 | 353 |
lemma NSCLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NSC> 0)" |
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
354 |
apply (auto simp del: star_of_zero simp add: NSCLIM_def) |
14405 | 355 |
apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI) |
356 |
apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym] |
|
17373
27509e72f29e
removed duplicated lemmas; convert more proofs to transfer principle
huffman
parents:
17318
diff
changeset
|
357 |
simp del: star_of_zero) |
14405 | 358 |
done |
359 |
||
360 |
(* [| k \<noteq> 0; (%x. k) -- x --NSC> 0 |] ==> R *) |
|
361 |
lemmas NSCLIM_not_zeroE = NSCLIM_not_zero [THEN notE, standard] |
|
362 |
||
363 |
lemma CLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --C> 0)" |
|
364 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_not_zero) |
|
365 |
||
366 |
(*** NSCLIM_const hence CLIM_const ***) |
|
367 |
||
368 |
lemma NSCLIM_const_eq: "(%x. k) -- x --NSC> L ==> k = L" |
|
369 |
apply (rule ccontr) |
|
370 |
apply (drule NSCLIM_zero) |
|
371 |
apply (rule NSCLIM_not_zeroE [of "k-L"], auto) |
|
372 |
done |
|
373 |
||
374 |
lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L" |
|
375 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq) |
|
376 |
||
377 |
(*** NSCLIM and hence CLIM are unique ***) |
|
378 |
||
379 |
lemma NSCLIM_unique: "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M" |
|
380 |
apply (drule NSCLIM_minus) |
|
381 |
apply (drule NSCLIM_add, assumption) |
|
382 |
apply (auto dest!: NSCLIM_const_eq [symmetric]) |
|
383 |
done |
|
384 |
||
385 |
lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M" |
|
386 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_unique) |
|
387 |
||
388 |
(*** NSCLIM_mult_zero and CLIM_mult_zero ***) |
|
389 |
||
390 |
lemma NSCLIM_mult_zero: |
|
391 |
"[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0" |
|
392 |
by (drule NSCLIM_mult, auto) |
|
393 |
||
394 |
lemma CLIM_mult_zero: |
|
395 |
"[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0" |
|
396 |
by (drule CLIM_mult, auto) |
|
397 |
||
398 |
(*** NSCLIM_self hence CLIM_self ***) |
|
399 |
||
400 |
lemma NSCLIM_self: "(%x. x) -- a --NSC> a" |
|
401 |
by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox) |
|
402 |
||
403 |
lemma CLIM_self: "(%x. x) -- a --C> a" |
|
404 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_self) |
|
405 |
||
406 |
(** another equivalence result **) |
|
407 |
lemma NSCLIM_NSCRLIM_iff: |
|
408 |
"(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)" |
|
409 |
apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff) |
|
410 |
apply (auto dest!: spec) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
411 |
apply (rule_tac [!] x = xa in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
412 |
apply (auto simp add: star_n_diff starfun hcmod mem_infmal_iff star_of_def) |
14405 | 413 |
done |
414 |
||
415 |
(** much, much easier standard proof **) |
|
416 |
lemma CLIM_CRLIM_iff: "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)" |
|
417 |
by (simp add: CLIM_def CRLIM_def) |
|
418 |
||
419 |
(* so this is nicer nonstandard proof *) |
|
420 |
lemma NSCLIM_NSCRLIM_iff2: |
|
421 |
"(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)" |
|
14469 | 422 |
by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric]) |
14405 | 423 |
|
424 |
lemma NSCLIM_NSCRLIM_Re_Im_iff: |
|
425 |
"(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) & |
|
426 |
(%x. Im(f x)) -- a --NSCR> Im(L))" |
|
427 |
apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im) |
|
428 |
apply (auto simp add: NSCLIM_def NSCRLIM_def) |
|
429 |
apply (auto dest!: spec) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
430 |
apply (rule_tac x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
431 |
apply (simp add: capprox_approx_iff starfun star_of_def) |
14405 | 432 |
done |
433 |
||
434 |
lemma CLIM_CRLIM_Re_Im_iff: |
|
435 |
"(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & |
|
436 |
(%x. Im(f x)) -- a --CR> Im(L))" |
|
437 |
by (simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff NSCLIM_NSCRLIM_Re_Im_iff) |
|
438 |
||
439 |
||
440 |
subsection{*Continuity*} |
|
441 |
||
442 |
lemma isNSContcD: |
|
443 |
"[| isNSContc f a; y @c= hcomplex_of_complex a |] |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
444 |
==> ( *f* f) y @c= hcomplex_of_complex (f a)" |
14405 | 445 |
by (simp add: isNSContc_def) |
446 |
||
447 |
lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) " |
|
448 |
by (simp add: isNSContc_def NSCLIM_def) |
|
449 |
||
450 |
lemma NSCLIM_isNSContc: |
|
451 |
"f -- a --NSC> (f a) ==> isNSContc f a" |
|
452 |
apply (simp add: isNSContc_def NSCLIM_def, auto) |
|
453 |
apply (case_tac "y = hcomplex_of_complex a", auto) |
|
454 |
done |
|
455 |
||
456 |
text{*Nonstandard continuity can be defined using NS Limit in |
|
457 |
similar fashion to standard definition of continuity*} |
|
458 |
||
459 |
lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))" |
|
460 |
by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc) |
|
461 |
||
462 |
lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))" |
|
463 |
by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff) |
|
464 |
||
465 |
(*** key result for continuity ***) |
|
466 |
lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)" |
|
467 |
by (simp add: isContc_def isNSContc_CLIM_iff) |
|
468 |
||
469 |
lemma isContc_isNSContc: "isContc f a ==> isNSContc f a" |
|
470 |
by (erule isNSContc_isContc_iff [THEN iffD2]) |
|
471 |
||
472 |
lemma isNSContc_isContc: "isNSContc f a ==> isContc f a" |
|
473 |
by (erule isNSContc_isContc_iff [THEN iffD1]) |
|
474 |
||
475 |
||
476 |
text{*Alternative definition of continuity*} |
|
477 |
lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)" |
|
478 |
apply (simp add: NSCLIM_def, auto) |
|
479 |
apply (drule_tac x = "hcomplex_of_complex a + x" in spec) |
|
480 |
apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp) |
|
481 |
apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]]) |
|
482 |
apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
483 |
prefer 3 apply (simp add: compare_rls add_commute) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
484 |
apply (rule_tac [2] x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
485 |
apply (rule_tac [4] x = x in star_cases) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
486 |
apply (auto simp add: starfun star_n_minus star_n_add star_of_def) |
14405 | 487 |
done |
488 |
||
489 |
lemma NSCLIM_isContc_iff: |
|
490 |
"(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)" |
|
491 |
by (rule NSCLIM_h_iff) |
|
492 |
||
493 |
lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))" |
|
494 |
by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff) |
|
495 |
||
496 |
lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))" |
|
497 |
by (simp add: isContc_def CLIM_isContc_iff) |
|
498 |
||
499 |
lemma isContc_add: |
|
500 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a" |
|
501 |
by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) |
|
502 |
||
503 |
lemma isContc_mult: |
|
504 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
505 |
by (auto intro!: starfun_mult_CFinite_capprox |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
506 |
[simplified starfun_mult [symmetric]] |
14405 | 507 |
simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) |
508 |
||
509 |
||
510 |
lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a" |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
511 |
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfun_o [symmetric]) |
14405 | 512 |
|
513 |
lemma isContc_o2: |
|
514 |
"[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a" |
|
515 |
by (auto dest: isContc_o simp add: o_def) |
|
516 |
||
517 |
lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a" |
|
518 |
by (simp add: isNSContc_def) |
|
519 |
||
520 |
lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a" |
|
521 |
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus) |
|
522 |
||
523 |
lemma isContc_inverse: |
|
524 |
"[| isContc f x; f x \<noteq> 0 |] ==> isContc (%x. inverse (f x)) x" |
|
525 |
by (simp add: isContc_def CLIM_inverse) |
|
526 |
||
527 |
lemma isNSContc_inverse: |
|
528 |
"[| isNSContc f x; f x \<noteq> 0 |] ==> isNSContc (%x. inverse (f x)) x" |
|
529 |
by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff) |
|
530 |
||
531 |
lemma isContc_diff: |
|
532 |
"[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a" |
|
14469 | 533 |
apply (simp add: diff_minus) |
14405 | 534 |
apply (auto intro: isContc_add isContc_minus) |
535 |
done |
|
536 |
||
537 |
lemma isContc_const [simp]: "isContc (%x. k) a" |
|
538 |
by (simp add: isContc_def) |
|
539 |
||
540 |
lemma isNSContc_const [simp]: "isNSContc (%x. k) a" |
|
541 |
by (simp add: isNSContc_def) |
|
542 |
||
543 |
||
544 |
subsection{*Functions from Complex to Reals*} |
|
545 |
||
546 |
lemma isNSContCRD: |
|
547 |
"[| isNSContCR f a; y @c= hcomplex_of_complex a |] |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
548 |
==> ( *f* f) y @= hypreal_of_real (f a)" |
14405 | 549 |
by (simp add: isNSContCR_def) |
550 |
||
551 |
lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) " |
|
552 |
by (simp add: isNSContCR_def NSCRLIM_def) |
|
553 |
||
554 |
lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a" |
|
555 |
apply (auto simp add: isNSContCR_def NSCRLIM_def) |
|
556 |
apply (case_tac "y = hcomplex_of_complex a", auto) |
|
557 |
done |
|
558 |
||
559 |
lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))" |
|
560 |
by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR) |
|
561 |
||
562 |
lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))" |
|
563 |
by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff) |
|
564 |
||
565 |
(*** another key result for continuity ***) |
|
566 |
lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)" |
|
567 |
by (simp add: isContCR_def isNSContCR_CRLIM_iff) |
|
568 |
||
569 |
lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a" |
|
570 |
by (erule isNSContCR_isContCR_iff [THEN iffD2]) |
|
571 |
||
572 |
lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a" |
|
573 |
by (erule isNSContCR_isContCR_iff [THEN iffD1]) |
|
574 |
||
575 |
lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)" |
|
576 |
by (auto intro: capprox_hcmod_approx |
|
577 |
simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] |
|
578 |
isNSContCR_def) |
|
579 |
||
580 |
lemma isContCR_cmod [simp]: "isContCR cmod (a)" |
|
14469 | 581 |
by (simp add: isNSContCR_isContCR_iff [symmetric]) |
14405 | 582 |
|
583 |
lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a" |
|
584 |
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re) |
|
585 |
||
586 |
lemma isContc_isContCR_Im: "isContc f a ==> isContCR (%x. Im (f x)) a" |
|
587 |
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Im) |
|
588 |
||
589 |
||
590 |
subsection{*Derivatives*} |
|
591 |
||
592 |
lemma CDERIV_iff: "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)" |
|
593 |
by (simp add: cderiv_def) |
|
594 |
||
595 |
lemma CDERIV_NSC_iff: |
|
596 |
"(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)" |
|
597 |
by (simp add: cderiv_def CLIM_NSCLIM_iff) |
|
598 |
||
599 |
lemma CDERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D" |
|
600 |
by (simp add: cderiv_def) |
|
601 |
||
602 |
lemma NSC_DERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D" |
|
603 |
by (simp add: cderiv_def CLIM_NSCLIM_iff) |
|
604 |
||
605 |
text{*Uniqueness*} |
|
606 |
lemma CDERIV_unique: "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E" |
|
607 |
by (simp add: cderiv_def CLIM_unique) |
|
608 |
||
609 |
(*** uniqueness: a nonstandard proof ***) |
|
610 |
lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E" |
|
611 |
apply (simp add: nscderiv_def) |
|
612 |
apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"] |
|
613 |
intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3) |
|
614 |
done |
|
13957 | 615 |
|
616 |
||
14405 | 617 |
subsection{* Differentiability*} |
618 |
||
619 |
lemma CDERIV_CLIM_iff: |
|
620 |
"((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = |
|
621 |
((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)" |
|
622 |
apply (simp add: CLIM_def) |
|
623 |
apply (rule_tac f=All in arg_cong) |
|
624 |
apply (rule ext) |
|
625 |
apply (rule imp_cong) |
|
626 |
apply (rule refl) |
|
627 |
apply (rule_tac f=Ex in arg_cong) |
|
628 |
apply (rule ext) |
|
629 |
apply (rule conj_cong) |
|
630 |
apply (rule refl) |
|
631 |
apply (rule trans) |
|
632 |
apply (rule all_shift [where a=a], simp) |
|
633 |
done |
|
634 |
||
635 |
lemma CDERIV_iff2: |
|
636 |
"(CDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)" |
|
637 |
by (simp add: cderiv_def CDERIV_CLIM_iff) |
|
638 |
||
639 |
||
640 |
subsection{* Equivalence of NS and Standard Differentiation*} |
|
641 |
||
642 |
(*** first equivalence ***) |
|
643 |
lemma NSCDERIV_NSCLIM_iff: |
|
644 |
"(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)" |
|
645 |
apply (simp add: nscderiv_def NSCLIM_def, auto) |
|
646 |
apply (drule_tac x = xa in bspec) |
|
647 |
apply (rule_tac [3] ccontr) |
|
648 |
apply (drule_tac [3] x = h in spec) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
649 |
apply (auto simp add: mem_cinfmal_iff starfun_lambda_cancel) |
14405 | 650 |
done |
651 |
||
652 |
(*** 2nd equivalence ***) |
|
653 |
lemma NSCDERIV_NSCLIM_iff2: |
|
654 |
"(NSCDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)" |
|
655 |
by (simp add: NSCDERIV_NSCLIM_iff CDERIV_CLIM_iff CLIM_NSCLIM_iff [symmetric]) |
|
656 |
||
657 |
lemma NSCDERIV_iff2: |
|
658 |
"(NSCDERIV f x :> D) = |
|
659 |
(\<forall>xa. xa \<noteq> hcomplex_of_complex x & xa @c= hcomplex_of_complex x --> |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
660 |
( *f* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)" |
14405 | 661 |
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) |
662 |
||
663 |
lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)" |
|
664 |
by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff) |
|
665 |
||
666 |
lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x" |
|
667 |
apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus) |
|
668 |
apply (drule capprox_minus_iff [THEN iffD1]) |
|
669 |
apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0") |
|
670 |
prefer 2 apply (simp add: compare_rls) |
|
671 |
apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec) |
|
15013 | 672 |
prefer 2 apply (simp add: add_assoc [symmetric]) |
673 |
apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute) |
|
14405 | 674 |
apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1) |
675 |
apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD] |
|
676 |
simp add: mult_assoc) |
|
677 |
apply (drule_tac x3 = D in |
|
678 |
CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult, |
|
679 |
THEN mem_cinfmal_iff [THEN iffD1]]) |
|
680 |
apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2]) |
|
681 |
done |
|
682 |
||
683 |
lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x" |
|
684 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric] isNSContc_isContc_iff [symmetric] NSCDERIV_isNSContc) |
|
685 |
||
686 |
text{* Differentiation rules for combinations of functions follow by clear, |
|
687 |
straightforard algebraic manipulations*} |
|
688 |
||
689 |
(* use simple constant nslimit theorem *) |
|
690 |
lemma NSCDERIV_const [simp]: "(NSCDERIV (%x. k) x :> 0)" |
|
691 |
by (simp add: NSCDERIV_NSCLIM_iff) |
|
692 |
||
693 |
lemma CDERIV_const [simp]: "(CDERIV (%x. k) x :> 0)" |
|
694 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric]) |
|
695 |
||
696 |
lemma NSCDERIV_add: |
|
697 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
698 |
==> NSCDERIV (%x. f x + g x) x :> Da + Db" |
|
699 |
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) |
|
700 |
apply (auto dest!: spec simp add: add_divide_distrib diff_minus) |
|
701 |
apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add) |
|
702 |
apply (auto simp add: add_ac) |
|
703 |
done |
|
704 |
||
705 |
lemma CDERIV_add: |
|
706 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
707 |
==> CDERIV (%x. f x + g x) x :> Da + Db" |
|
708 |
by (simp add: NSCDERIV_add NSCDERIV_CDERIV_iff [symmetric]) |
|
709 |
||
710 |
||
711 |
subsection{*Lemmas for Multiplication*} |
|
712 |
||
713 |
lemma lemma_nscderiv1: "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))" |
|
714 |
by (simp add: right_diff_distrib) |
|
715 |
||
716 |
lemma lemma_nscderiv2: |
|
717 |
"[| (x + y) / z = hcomplex_of_complex D + yb; z \<noteq> 0; |
|
718 |
z : CInfinitesimal; yb : CInfinitesimal |] |
|
719 |
==> x + y @c= 0" |
|
720 |
apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption) |
|
721 |
apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl) |
|
722 |
apply (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add |
|
723 |
simp add: mem_cinfmal_iff [symmetric]) |
|
724 |
apply (erule CInfinitesimal_subset_CFinite [THEN subsetD]) |
|
725 |
done |
|
726 |
||
727 |
lemma NSCDERIV_mult: |
|
728 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
729 |
==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" |
|
730 |
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) |
|
731 |
apply (auto dest!: spec |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
732 |
simp add: starfun_lambda_cancel lemma_nscderiv1) |
14405 | 733 |
apply (simp (no_asm) add: add_divide_distrib) |
734 |
apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+ |
|
735 |
apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric]) |
|
736 |
apply (simp add: diff_minus) |
|
737 |
apply (drule_tac D = Db in lemma_nscderiv2) |
|
738 |
apply (drule_tac [4] |
|
739 |
capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]]) |
|
740 |
apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc) |
|
741 |
apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst]) |
|
742 |
apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym] |
|
743 |
CInfinitesimal_add CInfinitesimal_mult |
|
744 |
CInfinitesimal_hcomplex_of_complex_mult |
|
745 |
CInfinitesimal_hcomplex_of_complex_mult2 |
|
15013 | 746 |
simp add: add_assoc [symmetric]) |
14405 | 747 |
done |
748 |
||
749 |
lemma CDERIV_mult: |
|
750 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
751 |
==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" |
|
752 |
by (simp add: NSCDERIV_mult NSCDERIV_CDERIV_iff [symmetric]) |
|
753 |
||
754 |
lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D" |
|
755 |
apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff |
|
14469 | 756 |
minus_mult_right right_distrib [symmetric] diff_minus |
14405 | 757 |
del: times_divide_eq_right minus_mult_right [symmetric]) |
758 |
apply (erule NSCLIM_const [THEN NSCLIM_mult]) |
|
759 |
done |
|
760 |
||
761 |
lemma CDERIV_cmult: "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D" |
|
762 |
by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric]) |
|
763 |
||
764 |
lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D" |
|
14469 | 765 |
apply (simp add: NSCDERIV_NSCLIM_iff diff_minus) |
14405 | 766 |
apply (rule_tac t = "f x" in minus_minus [THEN subst]) |
767 |
apply (simp (no_asm_simp) add: minus_add_distrib [symmetric] |
|
768 |
del: minus_add_distrib minus_minus) |
|
769 |
apply (erule NSCLIM_minus) |
|
770 |
done |
|
771 |
||
772 |
lemma CDERIV_minus: "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D" |
|
773 |
by (simp add: NSCDERIV_minus NSCDERIV_CDERIV_iff [symmetric]) |
|
774 |
||
775 |
lemma NSCDERIV_add_minus: |
|
776 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
777 |
==> NSCDERIV (%x. f x + -g x) x :> Da + -Db" |
|
778 |
by (blast dest: NSCDERIV_add NSCDERIV_minus) |
|
779 |
||
780 |
lemma CDERIV_add_minus: |
|
781 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
782 |
==> CDERIV (%x. f x + -g x) x :> Da + -Db" |
|
783 |
by (blast dest: CDERIV_add CDERIV_minus) |
|
784 |
||
785 |
lemma NSCDERIV_diff: |
|
786 |
"[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] |
|
787 |
==> NSCDERIV (%x. f x - g x) x :> Da - Db" |
|
14469 | 788 |
by (simp add: diff_minus NSCDERIV_add_minus) |
14405 | 789 |
|
790 |
lemma CDERIV_diff: |
|
791 |
"[| CDERIV f x :> Da; CDERIV g x :> Db |] |
|
792 |
==> CDERIV (%x. f x - g x) x :> Da - Db" |
|
14469 | 793 |
by (simp add: diff_minus CDERIV_add_minus) |
14405 | 794 |
|
795 |
||
796 |
subsection{*Chain Rule*} |
|
797 |
||
798 |
(* lemmas *) |
|
799 |
lemma NSCDERIV_zero: |
|
800 |
"[| NSCDERIV g x :> D; |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
801 |
( *f* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x); |
14405 | 802 |
xa : CInfinitesimal; xa \<noteq> 0 |
803 |
|] ==> D = 0" |
|
804 |
apply (simp add: nscderiv_def) |
|
805 |
apply (drule bspec, auto) |
|
806 |
done |
|
807 |
||
808 |
lemma NSCDERIV_capprox: |
|
809 |
"[| NSCDERIV f x :> D; h: CInfinitesimal; h \<noteq> 0 |] |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
810 |
==> ( *f* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0" |
14405 | 811 |
apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric]) |
812 |
apply (rule CInfinitesimal_ratio) |
|
813 |
apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto) |
|
814 |
done |
|
815 |
||
816 |
||
817 |
(*--------------------------------------------------*) |
|
818 |
(* from one version of differentiability *) |
|
819 |
(* *) |
|
820 |
(* f(x) - f(a) *) |
|
821 |
(* --------------- @= Db *) |
|
822 |
(* x - a *) |
|
823 |
(* -------------------------------------------------*) |
|
824 |
||
825 |
lemma NSCDERIVD1: |
|
826 |
"[| NSCDERIV f (g x) :> Da; |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
827 |
( *f* g) (hcomplex_of_complex(x) + xa) \<noteq> hcomplex_of_complex (g x); |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
828 |
( *f* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|] |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
829 |
==> (( *f* f) (( *f* g) (hcomplex_of_complex(x) + xa)) |
14405 | 830 |
- hcomplex_of_complex (f (g x))) / |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
831 |
(( *f* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) |
14405 | 832 |
@c= hcomplex_of_complex (Da)" |
14469 | 833 |
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) |
14405 | 834 |
|
835 |
(*--------------------------------------------------*) |
|
836 |
(* from other version of differentiability *) |
|
837 |
(* *) |
|
838 |
(* f(x + h) - f(x) *) |
|
839 |
(* ----------------- @= Db *) |
|
840 |
(* h *) |
|
841 |
(*--------------------------------------------------*) |
|
842 |
||
843 |
lemma NSCDERIVD2: |
|
844 |
"[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |] |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
845 |
==> (( *f* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa |
14405 | 846 |
@c= hcomplex_of_complex (Db)" |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
847 |
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfun_lambda_cancel) |
14405 | 848 |
|
849 |
lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)" |
|
850 |
by auto |
|
851 |
||
852 |
||
853 |
text{*Chain rule*} |
|
854 |
theorem NSCDERIV_chain: |
|
855 |
"[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] |
|
856 |
==> NSCDERIV (f o g) x :> Da * Db" |
|
857 |
apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric]) |
|
858 |
apply safe |
|
859 |
apply (frule_tac f = g in NSCDERIV_capprox) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
860 |
apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric]) |
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
861 |
apply (case_tac "( *f* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ") |
14405 | 862 |
apply (drule_tac g = g in NSCDERIV_zero) |
17300 | 863 |
apply (auto simp add: divide_inverse) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
864 |
apply (rule_tac z1 = "( *f* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst]) |
14405 | 865 |
apply (simp (no_asm_simp)) |
866 |
apply (rule capprox_mult_hcomplex_of_complex) |
|
867 |
apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] |
|
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
868 |
simp add: diff_minus [symmetric] divide_inverse [symmetric]) |
14405 | 869 |
apply (blast intro: NSCDERIVD2) |
870 |
done |
|
871 |
||
872 |
text{*standard version*} |
|
873 |
lemma CDERIV_chain: |
|
874 |
"[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] |
|
875 |
==> CDERIV (f o g) x :> Da * Db" |
|
876 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric] NSCDERIV_chain) |
|
877 |
||
878 |
lemma CDERIV_chain2: |
|
879 |
"[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] |
|
880 |
==> CDERIV (%x. f (g x)) x :> Da * Db" |
|
881 |
by (auto dest: CDERIV_chain simp add: o_def) |
|
882 |
||
883 |
||
884 |
subsection{* Differentiation of Natural Number Powers*} |
|
885 |
||
886 |
lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1" |
|
15228 | 887 |
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def divide_self del: divide_self_if) |
14405 | 888 |
|
889 |
lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1" |
|
890 |
by (simp add: NSCDERIV_CDERIV_iff [symmetric]) |
|
891 |
||
892 |
lemmas isContc_Id = CDERIV_Id [THEN CDERIV_isContc, standard] |
|
13957 | 893 |
|
14405 | 894 |
text{*derivative of linear multiplication*} |
895 |
lemma CDERIV_cmult_Id [simp]: "CDERIV (op * c) x :> c" |
|
896 |
by (cut_tac c = c and x = x in CDERIV_Id [THEN CDERIV_cmult], simp) |
|
897 |
||
898 |
lemma NSCDERIV_cmult_Id [simp]: "NSCDERIV (op * c) x :> c" |
|
899 |
by (simp add: NSCDERIV_CDERIV_iff) |
|
900 |
||
901 |
lemma CDERIV_pow [simp]: |
|
902 |
"CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
|
903 |
apply (induct_tac "n") |
|
904 |
apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult]) |
|
15013 | 905 |
apply (auto simp add: left_distrib real_of_nat_Suc) |
14405 | 906 |
apply (case_tac "n") |
907 |
apply (auto simp add: mult_ac add_commute) |
|
908 |
done |
|
909 |
||
910 |
text{*Nonstandard version*} |
|
911 |
lemma NSCDERIV_pow: |
|
912 |
"NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" |
|
913 |
by (simp add: NSCDERIV_CDERIV_iff) |
|
914 |
||
915 |
lemma lemma_CDERIV_subst: |
|
916 |
"[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E" |
|
917 |
by auto |
|
918 |
||
919 |
(*used once, in NSCDERIV_inverse*) |
|
920 |
lemma CInfinitesimal_add_not_zero: |
|
921 |
"[| h: CInfinitesimal; x \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0" |
|
922 |
apply clarify |
|
923 |
apply (drule equals_zero_I, auto) |
|
924 |
done |
|
925 |
||
926 |
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*} |
|
927 |
lemma NSCDERIV_inverse: |
|
928 |
"x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))" |
|
929 |
apply (simp add: nscderiv_def Ball_def, clarify) |
|
930 |
apply (frule CInfinitesimal_add_not_zero [where x=x]) |
|
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
931 |
apply (auto simp add: starfun_inverse_inverse diff_minus |
14405 | 932 |
simp del: minus_mult_left [symmetric] minus_mult_right [symmetric]) |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17300
diff
changeset
|
933 |
apply (simp add: add_commute numeral_2_eq_2 inverse_add |
14405 | 934 |
inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric] |
935 |
add_ac mult_ac |
|
15013 | 936 |
del: inverse_minus_eq inverse_mult_distrib |
937 |
minus_mult_right [symmetric] minus_mult_left [symmetric]) |
|
14405 | 938 |
apply (simp only: mult_assoc [symmetric] right_distrib) |
939 |
apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans) |
|
940 |
apply (rule inverse_add_CInfinitesimal_capprox2) |
|
941 |
apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal |
|
942 |
intro: CFinite_mult |
|
943 |
simp add: inverse_minus_eq [symmetric]) |
|
944 |
apply (rule CInfinitesimal_CFinite_mult2, auto) |
|
945 |
done |
|
946 |
||
947 |
lemma CDERIV_inverse: |
|
948 |
"x \<noteq> 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))" |
|
949 |
by (simp add: NSCDERIV_inverse NSCDERIV_CDERIV_iff [symmetric] |
|
950 |
del: complexpow_Suc) |
|
951 |
||
952 |
||
953 |
subsection{*Derivative of Reciprocals (Function @{term inverse})*} |
|
954 |
||
955 |
lemma CDERIV_inverse_fun: |
|
956 |
"[| CDERIV f x :> d; f(x) \<noteq> 0 |] |
|
957 |
==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
958 |
apply (rule mult_commute [THEN subst]) |
|
15013 | 959 |
apply (simp add: minus_mult_left power_inverse |
960 |
del: complexpow_Suc minus_mult_left [symmetric]) |
|
14405 | 961 |
apply (fold o_def) |
962 |
apply (blast intro!: CDERIV_chain CDERIV_inverse) |
|
963 |
done |
|
964 |
||
965 |
lemma NSCDERIV_inverse_fun: |
|
966 |
"[| NSCDERIV f x :> d; f(x) \<noteq> 0 |] |
|
967 |
==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))" |
|
968 |
by (simp add: NSCDERIV_CDERIV_iff CDERIV_inverse_fun del: complexpow_Suc) |
|
969 |
||
970 |
||
971 |
subsection{* Derivative of Quotient*} |
|
972 |
||
973 |
lemma CDERIV_quotient: |
|
974 |
"[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |] |
|
975 |
==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
14469 | 976 |
apply (simp add: diff_minus) |
14405 | 977 |
apply (drule_tac f = g in CDERIV_inverse_fun) |
978 |
apply (drule_tac [2] CDERIV_mult, assumption+) |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17373
diff
changeset
|
979 |
apply (simp add: divide_inverse left_distrib power_inverse minus_mult_left |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
980 |
mult_ac |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
981 |
del: minus_mult_right [symmetric] minus_mult_left [symmetric] |
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14405
diff
changeset
|
982 |
complexpow_Suc) |
14405 | 983 |
done |
984 |
||
985 |
lemma NSCDERIV_quotient: |
|
986 |
"[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) \<noteq> 0 |] |
|
987 |
==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
|
988 |
by (simp add: NSCDERIV_CDERIV_iff CDERIV_quotient del: complexpow_Suc) |
|
989 |
||
990 |
||
991 |
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*} |
|
992 |
||
993 |
lemma CLIM_equal: |
|
994 |
"[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --C> l) = (g -- a --C> l)" |
|
995 |
by (simp add: CLIM_def complex_add_minus_iff) |
|
996 |
||
997 |
lemma CLIM_trans: |
|
998 |
"[| (%x. f(x) + -g(x)) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l" |
|
999 |
apply (drule CLIM_add, assumption) |
|
1000 |
apply (simp add: complex_add_assoc) |
|
1001 |
done |
|
1002 |
||
1003 |
lemma CARAT_CDERIV: |
|
1004 |
"(CDERIV f x :> l) = |
|
1005 |
(\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isContc g x & g x = l)" |
|
1006 |
apply safe |
|
1007 |
apply (rule_tac x = "%z. if z=x then l else (f (z) - f (x)) / (z-x)" in exI) |
|
1008 |
apply (auto simp add: mult_assoc isContc_iff CDERIV_iff) |
|
1009 |
apply (rule_tac [!] CLIM_equal [THEN iffD1], auto) |
|
1010 |
done |
|
1011 |
||
1012 |
||
1013 |
lemma CARAT_NSCDERIV: |
|
1014 |
"NSCDERIV f x :> l ==> |
|
1015 |
\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l" |
|
14469 | 1016 |
by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV) |
14405 | 1017 |
|
1018 |
lemma CARAT_CDERIVD: |
|
1019 |
"(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l |
|
1020 |
==> NSCDERIV f x :> l" |
|
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset
|
1021 |
by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq); |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset
|
1022 |
|
14405 | 1023 |
end |