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