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--
```     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
```