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