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