124 "f -- x --C> L ==> f -- x --NSC> L" |
124 "f -- x --C> L ==> f -- x --NSC> L" |
125 apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) |
125 apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) |
126 apply (rule_tac z = xa in eq_Abs_hcomplex) |
126 apply (rule_tac z = xa in eq_Abs_hcomplex) |
127 apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff |
127 apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff |
128 CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
128 CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) |
129 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe) |
129 apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe) |
130 apply (drule_tac x = u in spec, auto) |
130 apply (drule_tac x = u in spec, auto) |
131 apply (drule_tac x = s in spec, auto, ultra) |
131 apply (drule_tac x = s in spec, auto, ultra) |
132 apply (drule sym, auto) |
132 apply (drule sym, auto) |
133 done |
133 done |
134 |
134 |
194 apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) |
194 apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) |
195 apply (rule_tac z = xa in eq_Abs_hcomplex) |
195 apply (rule_tac z = xa in eq_Abs_hcomplex) |
196 apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff |
196 apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff |
197 CInfinitesimal_hcmod_iff hcmod hypreal_diff |
197 CInfinitesimal_hcmod_iff hcmod hypreal_diff |
198 Infinitesimal_FreeUltrafilterNat_iff |
198 Infinitesimal_FreeUltrafilterNat_iff |
|
199 star_of_def star_n_def |
199 Infinitesimal_approx_minus [symmetric] hypreal_of_real_def) |
200 Infinitesimal_approx_minus [symmetric] hypreal_of_real_def) |
200 apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe) |
201 apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe) |
201 apply (drule_tac x = u in spec, auto) |
202 apply (drule_tac x = u in spec, auto) |
202 apply (drule_tac x = s in spec, auto, ultra) |
203 apply (drule_tac x = s in spec, auto, ultra) |
203 apply (drule sym, auto) |
204 apply (drule sym, auto) |
204 done |
205 done |
205 |
206 |
239 apply (drule lemma_skolemize_CRLIM2, safe) |
240 apply (drule lemma_skolemize_CRLIM2, safe) |
240 apply (drule_tac x = X in spec, auto) |
241 apply (drule_tac x = X in spec, auto) |
241 apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
242 apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) |
242 apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def |
243 apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def |
243 Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod) |
244 Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod) |
244 apply (auto simp add: hypreal_of_real_def hypreal_diff) |
245 apply (auto simp add: hypreal_of_real_def star_of_def star_n_def hypreal_diff) |
245 apply (drule_tac x = r in spec, clarify) |
246 apply (drule_tac x = r in spec, clarify) |
246 apply (drule FreeUltrafilterNat_all, ultra) |
247 apply (drule FreeUltrafilterNat_all, ultra) |
247 done |
248 done |
248 |
249 |
249 text{*Second key result*} |
250 text{*Second key result*} |
425 (%x. Im(f x)) -- a --NSCR> Im(L))" |
426 (%x. Im(f x)) -- a --NSCR> Im(L))" |
426 apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im) |
427 apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im) |
427 apply (auto simp add: NSCLIM_def NSCRLIM_def) |
428 apply (auto simp add: NSCLIM_def NSCRLIM_def) |
428 apply (auto dest!: spec) |
429 apply (auto dest!: spec) |
429 apply (rule_tac z = x in eq_Abs_hcomplex) |
430 apply (rule_tac z = x in eq_Abs_hcomplex) |
430 apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def) |
431 apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def star_of_def star_n_def) |
431 done |
432 done |
432 |
433 |
433 lemma CLIM_CRLIM_Re_Im_iff: |
434 lemma CLIM_CRLIM_Re_Im_iff: |
434 "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & |
435 "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & |
435 (%x. Im(f x)) -- a --CR> Im(L))" |
436 (%x. Im(f x)) -- a --CR> Im(L))" |