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