src/HOL/Complex/NSCA.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       : NSCA.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2001,2002 University of Edinburgh
     4     Description : Infinite, infinitesimal complex number etc! 
     5 *)
     6 
     7 (*--------------------------------------------------------------------------------------*)
     8 (* Closure laws for members of (embedded) set standard complex SComplex                 *)
     9 (* -------------------------------------------------------------------------------------*)
    10 
    11 Goalw [SComplex_def] "[| (x::hcomplex): SComplex; y: SComplex |] ==> x + y: SComplex";
    12 by (Step_tac 1);
    13 by (res_inst_tac [("x","r + ra")] exI 1);
    14 by (Simp_tac 1);
    15 qed "SComplex_add";
    16 
    17 Goalw [SComplex_def] "[| (x::hcomplex): SComplex; y: SComplex |] ==> x * y: SComplex";
    18 by (Step_tac 1);
    19 by (res_inst_tac [("x","r * ra")] exI 1);
    20 by (Simp_tac 1);
    21 qed "SComplex_mult";
    22 
    23 Goalw [SComplex_def] "x: SComplex ==> inverse x : SComplex";
    24 by (blast_tac (claset() addIs [hcomplex_of_complex_inverse RS sym]) 1); 
    25 qed "SComplex_inverse";
    26 
    27 Goal "[| x: SComplex;  y: SComplex |] ==> x/y: SComplex";
    28 by (asm_simp_tac (simpset() addsimps [SComplex_mult,SComplex_inverse,
    29                                       hcomplex_divide_def]) 1); 
    30 qed "SComplex_divide";
    31 
    32 Goalw [SComplex_def] "x: SComplex ==> -x : SComplex";
    33 by (blast_tac (claset() addIs [hcomplex_of_complex_minus RS sym]) 1); 
    34 qed "SComplex_minus";
    35 
    36 Goal "(-x : SComplex) = (x: SComplex)";
    37 by Auto_tac;  
    38 by (etac SComplex_minus 2); 
    39 by (dtac SComplex_minus 1); 
    40 by Auto_tac;  
    41 qed "SComplex_minus_iff";
    42 Addsimps [SComplex_minus_iff]; 
    43 
    44 Goal "[| x + y : SComplex; y: SComplex |] ==> x: SComplex";
    45 by (dres_inst_tac [("x","y")] SComplex_minus 1);
    46 by (dtac SComplex_add 1);
    47 by (assume_tac 1); 
    48 by Auto_tac;  
    49 qed "SComplex_add_cancel";
    50 
    51 Goalw [hcomplex_of_complex_def]
    52      "hcmod (hcomplex_of_complex r) : Reals";
    53 by (simp_tac (simpset() addsimps [hcmod,SReal_def,
    54     hypreal_of_real_def]) 1);
    55 qed "SReal_hcmod_hcomplex_of_complex";
    56 Addsimps [SReal_hcmod_hcomplex_of_complex];
    57 
    58 Goalw [hcomplex_number_of_def]
    59     "hcmod (number_of w ::hcomplex) : Reals";
    60 by (rtac SReal_hcmod_hcomplex_of_complex 1);
    61 qed "SReal_hcmod_number_of";
    62 Addsimps [SReal_hcmod_number_of];
    63 
    64 Goalw [SComplex_def] "x: SComplex ==> hcmod x : Reals";
    65 by Auto_tac;
    66 qed "SReal_hcmod_SComplex";
    67 
    68 Goalw [SComplex_def] "hcomplex_of_complex x: SComplex";
    69 by (Blast_tac 1);
    70 qed "SComplex_hcomplex_of_complex";
    71 Addsimps [SComplex_hcomplex_of_complex];
    72 
    73 Goalw [hcomplex_number_of_def] "(number_of w ::hcomplex) : SComplex";
    74 by (rtac SComplex_hcomplex_of_complex 1);
    75 qed "SComplex_number_of";
    76 Addsimps [SComplex_number_of];
    77 
    78 Goalw [hcomplex_divide_def] "r : SComplex ==> r/(number_of w::hcomplex) : SComplex";
    79 by (blast_tac (claset() addSIs [SComplex_number_of, SComplex_mult, 
    80                                 SComplex_inverse]) 1);
    81 qed "SComplex_divide_number_of";
    82 
    83 Goalw [SComplex_def] "{x. hcomplex_of_complex x : SComplex} = (UNIV::complex set)";
    84 by Auto_tac;
    85 qed "SComplex_UNIV_complex";
    86 
    87 Goalw [SComplex_def] "(x: SComplex) = (EX y. x = hcomplex_of_complex y)";
    88 by Auto_tac;
    89 qed "SComplex_iff";
    90 
    91 Goalw [SComplex_def] "hcomplex_of_complex `(UNIV::complex set) = SComplex";
    92 by Auto_tac;
    93 qed "hcomplex_of_complex_image";
    94 
    95 Goalw [SComplex_def] "inv hcomplex_of_complex `SComplex = (UNIV::complex set)";
    96 by Auto_tac;
    97 by (rtac (inj_hcomplex_of_complex RS inv_f_f RS subst) 1);
    98 by (Blast_tac 1);
    99 qed "inv_hcomplex_of_complex_image";
   100 
   101 Goalw [SComplex_def] 
   102       "[| EX x. x: P; P <= SComplex |] ==> EX Q. P = hcomplex_of_complex ` Q";
   103 by (Best_tac 1); 
   104 qed "SComplex_hcomplex_of_complex_image";
   105 
   106 Goal "[| (x::hcomplex): SComplex; y: SComplex; hcmod x < hcmod y \
   107 \     |] ==> EX r: Reals. hcmod x< r & r < hcmod y";
   108 by (auto_tac (claset() addIs [SReal_dense], simpset() 
   109     addsimps [SReal_hcmod_SComplex]));
   110 qed "SComplex_SReal_dense";
   111 
   112 Goalw [SComplex_def,SReal_def] 
   113       "z : SComplex ==> hcmod z : Reals";
   114 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   115 by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
   116     hcomplex_of_complex_def,cmod_def]));
   117 by (res_inst_tac [("x","cmod r")] exI 1);
   118 by (ultra_tac (claset(),simpset() addsimps [cmod_def]) 1);
   119 qed "SComplex_hcmod_SReal";
   120 
   121 Goal "0 : SComplex";
   122 by (auto_tac (claset(),simpset() addsimps [SComplex_def]));
   123 qed "SComplex_zero";
   124 Addsimps [SComplex_zero];
   125 
   126 Goal "1 : SComplex";
   127 by (auto_tac (claset(),simpset() addsimps [SComplex_def,hcomplex_of_complex_def,
   128     hcomplex_one_def]));
   129 qed "SComplex_one";
   130 Addsimps [SComplex_one];
   131 
   132 (*
   133 Goalw [SComplex_def,SReal_def] "hcmod z : Reals ==> z : SComplex";
   134 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   135 by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
   136     hcomplex_of_complex_def,cmod_def]));
   137 *)
   138 
   139 (*--------------------------------------------------------------------------------------------*)
   140 (*        Set of finite elements is a subring of the extended complex numbers                 *)
   141 (* -------------------------------------------------------------------------------------------*)
   142 
   143 Goalw [CFinite_def] "[|x : CFinite; y : CFinite|] ==> (x+y) : CFinite";
   144 by (blast_tac (claset() addSIs [SReal_add,hcmod_add_less]) 1);
   145 qed "CFinite_add";
   146 
   147 Goalw [CFinite_def] "[|x : CFinite; y : CFinite|] ==> x*y : CFinite";
   148 by (blast_tac (claset() addSIs [SReal_mult,hcmod_mult_less]) 1);
   149 qed "CFinite_mult";
   150 
   151 Goalw [CFinite_def] "(-x : CFinite) = (x : CFinite)";
   152 by (Simp_tac 1);
   153 qed "CFinite_minus_iff";
   154 Addsimps [CFinite_minus_iff];
   155 
   156 Goalw [SComplex_def,CFinite_def] "SComplex <= CFinite";
   157 by Auto_tac;
   158 by (res_inst_tac [("x","1 + hcmod(hcomplex_of_complex r)")] bexI 1);
   159 by (auto_tac (claset() addIs [SReal_add],simpset()));
   160 qed "SComplex_subset_CFinite";
   161 Addsimps [ SComplex_subset_CFinite];
   162 
   163 Goal "hcmod (hcomplex_of_complex r) : HFinite";
   164 by (auto_tac (claset() addSIs [ SReal_subset_HFinite RS subsetD],simpset()));
   165 qed "HFinite_hcmod_hcomplex_of_complex";
   166 Addsimps [HFinite_hcmod_hcomplex_of_complex];
   167 
   168 Goal "hcomplex_of_complex x: CFinite";
   169 by (auto_tac (claset() addSIs [ SComplex_subset_CFinite RS subsetD],simpset()));
   170 qed "CFinite_hcomplex_of_complex";
   171 Addsimps [CFinite_hcomplex_of_complex];
   172 
   173 Goalw [CFinite_def] "x : CFinite ==> EX t: Reals. hcmod x < t";
   174 by Auto_tac;
   175 qed "CFiniteD";
   176 
   177 Goalw [CFinite_def] "(x : CFinite) = (hcmod x : HFinite)";
   178 by (auto_tac (claset(), simpset() addsimps [HFinite_def]));
   179 qed "CFinite_hcmod_iff";
   180 
   181 Goal "number_of w : CFinite";
   182 by (rtac (SComplex_number_of RS (SComplex_subset_CFinite RS subsetD)) 1);
   183 qed "CFinite_number_of";
   184 Addsimps [CFinite_number_of];
   185 
   186 Goal "[|x : CFinite; y <= hcmod x; 0 <= y |] ==> y: HFinite";
   187 by (auto_tac (claset() addIs [HFinite_bounded],simpset() addsimps 
   188     [CFinite_hcmod_iff]));
   189 qed "CFinite_bounded";
   190 
   191 (*--------------------------------------------------------------------------------------*)
   192 (* Set of complex infinitesimals is a subring of the nonstandard complex numbers        *) 
   193 (*--------------------------------------------------------------------------------------*)
   194 	 
   195 Goalw [CInfinitesimal_def]
   196       "x : CInfinitesimal ==> ALL r: Reals. 0 < r --> hcmod x < r";
   197 by Auto_tac;
   198 qed "CInfinitesimalD";
   199 
   200 Goalw [CInfinitesimal_def] "0 : CInfinitesimal";
   201 by Auto_tac;
   202 qed "CInfinitesimal_zero";
   203 AddIffs [CInfinitesimal_zero];
   204 
   205 Goal "x/(2::hcomplex) + x/(2::hcomplex) = x";
   206 by Auto_tac;  
   207 qed "hcomplex_sum_of_halves";
   208 
   209 Goalw [CInfinitesimal_def,Infinitesimal_def] 
   210    "(z : CInfinitesimal) = (hcmod z : Infinitesimal)";
   211 by Auto_tac;
   212 qed "CInfinitesimal_hcmod_iff";
   213 
   214 Goal "1 ~: CInfinitesimal";
   215 by (simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff]) 1);
   216 qed "one_not_CInfinitesimal";
   217 Addsimps [one_not_CInfinitesimal];
   218 
   219 Goal "[| x : CInfinitesimal; y : CInfinitesimal |] ==> (x+y) : CInfinitesimal";
   220 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
   221 by (rtac hrabs_le_Infinitesimal 1);
   222 by (res_inst_tac [("y","hcmod y")] Infinitesimal_add 1);
   223 by Auto_tac;
   224 qed "CInfinitesimal_add";
   225 
   226 Goalw [CInfinitesimal_def] "(-x:CInfinitesimal) = (x:CInfinitesimal)";
   227 by (Full_simp_tac 1);
   228 qed "CInfinitesimal_minus_iff";
   229 Addsimps [CInfinitesimal_minus_iff];
   230 
   231 Goal "[| x : CInfinitesimal;  y : CInfinitesimal |] ==> x-y : CInfinitesimal";
   232 by (asm_simp_tac
   233     (simpset() addsimps [hcomplex_diff_def, CInfinitesimal_add]) 1);
   234 qed "CInfinitesimal_diff";
   235 
   236 Goal "[| x : CInfinitesimal; y : CInfinitesimal |] ==> (x * y) : CInfinitesimal";
   237 by (auto_tac (claset() addIs [Infinitesimal_mult],simpset() addsimps 
   238     [CInfinitesimal_hcmod_iff,hcmod_mult]));
   239 qed "CInfinitesimal_mult";
   240 
   241 Goal "[| x : CInfinitesimal; y : CFinite |] ==> (x * y) : CInfinitesimal";
   242 by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult],simpset() 
   243     addsimps [CInfinitesimal_hcmod_iff,CFinite_hcmod_iff,hcmod_mult]));
   244 qed "CInfinitesimal_CFinite_mult";
   245 
   246 Goal "[| x : CInfinitesimal; y : CFinite |] ==> (y * x) : CInfinitesimal";
   247 by (auto_tac (claset() addDs [CInfinitesimal_CFinite_mult],
   248               simpset() addsimps [hcomplex_mult_commute]));
   249 qed "CInfinitesimal_CFinite_mult2";
   250 
   251 Goalw [CInfinite_def,HInfinite_def] 
   252    "(z : CInfinite) = (hcmod z : HInfinite)";
   253 by Auto_tac;
   254 qed "CInfinite_hcmod_iff";
   255 
   256 Goal "x: CInfinite ==> inverse x: CInfinitesimal";
   257 by (auto_tac (claset() addIs [HInfinite_inverse_Infinitesimal],
   258     simpset() addsimps [CInfinitesimal_hcmod_iff,
   259     CInfinite_hcmod_iff,hcmod_hcomplex_inverse]));
   260 qed "CInfinite_inverse_CInfinitesimal";
   261 
   262 Goal "[|x: CInfinite; y: CInfinite|] ==> (x*y): CInfinite";
   263 by (auto_tac (claset() addIs [HInfinite_mult],simpset() addsimps 
   264     [CInfinite_hcmod_iff,hcmod_mult]));
   265 qed "CInfinite_mult";
   266 
   267 Goalw [CInfinite_def] "(-x : CInfinite) = (x : CInfinite)";
   268 by (Simp_tac 1);
   269 qed "CInfinite_minus_iff";
   270 Addsimps [CInfinite_minus_iff];
   271 
   272 Goal "[|a: CFinite; b: CFinite; c: CFinite|] \ 
   273 \     ==> a*a + b*b + c*c : CFinite";
   274 by (auto_tac (claset() addIs [CFinite_mult,CFinite_add], simpset()));
   275 qed "CFinite_sum_squares";
   276 
   277 Goal "x ~: CInfinitesimal ==> x ~= 0";
   278 by Auto_tac;
   279 qed "not_CInfinitesimal_not_zero";
   280 
   281 Goal "x: CFinite - CInfinitesimal ==> x ~= 0";
   282 by Auto_tac;
   283 qed "not_CInfinitesimal_not_zero2";
   284 
   285 Goal "x : CFinite - CInfinitesimal ==> hcmod x : HFinite - Infinitesimal";
   286 by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,CInfinitesimal_hcmod_iff]));
   287 qed "CFinite_diff_CInfinitesimal_hcmod";
   288 
   289 Goal "[| e : CInfinitesimal; hcmod x < hcmod e |] ==> x : CInfinitesimal";
   290 by (auto_tac (claset() addIs [hrabs_less_Infinitesimal],simpset() 
   291     addsimps [CInfinitesimal_hcmod_iff]));
   292 qed "hcmod_less_CInfinitesimal";
   293 
   294 Goal "[| e : CInfinitesimal; hcmod x <= hcmod e |] ==> x : CInfinitesimal";
   295 by (auto_tac (claset() addIs [hrabs_le_Infinitesimal],simpset() 
   296     addsimps [CInfinitesimal_hcmod_iff]));
   297 qed "hcmod_le_CInfinitesimal";
   298 
   299 Goal  "[| e : CInfinitesimal; \
   300 \         e' : CInfinitesimal; \
   301 \         hcmod e' < hcmod x ; hcmod x < hcmod e \
   302 \      |] ==> x : CInfinitesimal";
   303 by (auto_tac (claset() addIs [Infinitesimal_interval],simpset() 
   304     addsimps [CInfinitesimal_hcmod_iff]));
   305 qed "CInfinitesimal_interval";
   306 
   307 Goal "[| e : CInfinitesimal; \
   308 \        e' : CInfinitesimal; \
   309 \        hcmod e' <= hcmod x ; hcmod x <= hcmod e \
   310 \     |] ==> x : CInfinitesimal";
   311 by (auto_tac (claset() addIs [Infinitesimal_interval2],simpset() 
   312     addsimps [CInfinitesimal_hcmod_iff]));
   313 qed "CInfinitesimal_interval2";
   314 
   315 Goal "[| x ~: CInfinitesimal;  y ~: CInfinitesimal|] ==> (x*y) ~: CInfinitesimal";
   316 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
   317 by (dtac not_Infinitesimal_mult 1);
   318 by Auto_tac;
   319 qed "not_CInfinitesimal_mult";
   320 
   321 Goal "x*y : CInfinitesimal ==> x : CInfinitesimal | y : CInfinitesimal";
   322 by (auto_tac (claset() addDs [Infinitesimal_mult_disj],simpset() addsimps 
   323     [CInfinitesimal_hcmod_iff,hcmod_mult]));
   324 qed "CInfinitesimal_mult_disj";
   325 
   326 Goal "[| x : CFinite - CInfinitesimal; \
   327 \                  y : CFinite - CInfinitesimal \
   328 \               |] ==> (x*y) : CFinite - CInfinitesimal";
   329 by (Clarify_tac 1);
   330 by (blast_tac (claset() addDs [CFinite_mult,not_CInfinitesimal_mult]) 1);
   331 qed "CFinite_CInfinitesimal_diff_mult";
   332 
   333 Goal "CInfinitesimal <= CFinite";
   334 by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
   335     simpset() addsimps [CInfinitesimal_hcmod_iff,CFinite_hcmod_iff]));
   336 qed "CInfinitesimal_subset_CFinite";
   337 
   338 Goal "x: CInfinitesimal ==> x * hcomplex_of_complex r : CInfinitesimal";
   339 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult],
   340     simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
   341 qed "CInfinitesimal_hcomplex_of_complex_mult";
   342 
   343 Goal "x: CInfinitesimal ==> hcomplex_of_complex r * x: CInfinitesimal";
   344 by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
   345     simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
   346 qed "CInfinitesimal_hcomplex_of_complex_mult2";
   347 
   348 
   349 (*--------------------------------------------------------------------------------------*)
   350 (* Infinitely close relation @c=                                                        *)
   351 (* -------------------------------------------------------------------------------------*)
   352 
   353 (*
   354 Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)";
   355 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
   356 *)
   357 
   358 Goal "x:CInfinitesimal = (x @c= 0)";
   359 by (simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff,
   360     capprox_def]) 1);
   361 qed "mem_cinfmal_iff";
   362 
   363 Goalw [capprox_def,hcomplex_diff_def]
   364       " (x @c= y) = (x + -y @c= 0)";
   365 by (Simp_tac 1);
   366 qed "capprox_minus_iff";
   367 
   368 Goalw [capprox_def,hcomplex_diff_def]
   369       " (x @c= y) = (-y + x @c= 0)";
   370 by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
   371 qed "capprox_minus_iff2";
   372 
   373 Goalw [capprox_def] "x @c= x";
   374 by (Simp_tac 1);
   375 qed "capprox_refl";
   376 Addsimps [capprox_refl];
   377 
   378 Goalw [capprox_def,CInfinitesimal_def]  
   379      "x @c= y ==> y @c= x";
   380 by (auto_tac (claset() addSDs [bspec],simpset() addsimps 
   381     [hcmod_diff_commute]));
   382 qed "capprox_sym";
   383 
   384 Goalw [capprox_def]  "[| x @c= y; y @c= z |] ==> x @c= z";
   385 by (dtac CInfinitesimal_add 1); 
   386 by (assume_tac 1); 
   387 by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]));
   388 qed "capprox_trans";
   389 
   390 Goal "[| r @c= x; s @c= x |] ==> r @c= s";
   391 by (blast_tac (claset() addIs [capprox_sym, capprox_trans]) 1); 
   392 qed "capprox_trans2";
   393 
   394 Goal "[| x @c= r; x @c= s|] ==> r @c= s";
   395 by (blast_tac (claset() addIs [capprox_sym, capprox_trans]) 1); 
   396 qed "capprox_trans3";
   397 
   398 Goal "(number_of w @c= x) = (x @c= number_of w)";
   399 by (blast_tac (claset() addIs [capprox_sym]) 1); 
   400 qed "number_of_capprox_reorient";
   401 Addsimps [number_of_capprox_reorient];
   402 
   403 Goal "(x-y : CInfinitesimal) = (x @c= y)";
   404 by (auto_tac (claset(),
   405               simpset() addsimps [hcomplex_diff_def, capprox_minus_iff RS sym,
   406                                   mem_cinfmal_iff]));
   407 qed "CInfinitesimal_capprox_minus";
   408 
   409 Goalw [cmonad_def] "(x @c= y) = (cmonad(x)=cmonad(y))";
   410 by (auto_tac (claset() addDs [capprox_sym] 
   411                        addSEs [capprox_trans,equalityCE],
   412               simpset()));
   413 qed "capprox_monad_iff";
   414 
   415 Goal "[| x: CInfinitesimal; y: CInfinitesimal |] ==> x @c= y";
   416 by (asm_full_simp_tac (simpset() addsimps [mem_cinfmal_iff]) 1);
   417 by (blast_tac (claset() addIs [capprox_trans, capprox_sym]) 1); 
   418 qed "Infinitesimal_capprox";
   419 
   420 val prem1::prem2::rest = 
   421 goalw thy [capprox_def,hcomplex_diff_def] 
   422      "[| a @c= b; c @c= d |] ==> a+c @c= b+d";
   423 by (rtac (hcomplex_minus_add_distrib RS ssubst) 1);
   424 by (rtac (hcomplex_add_assoc RS ssubst) 1);
   425 by (res_inst_tac [("y1","c")] (hcomplex_add_left_commute RS subst) 1);
   426 by (rtac (hcomplex_add_assoc RS subst) 1);
   427 by (rtac ([prem1,prem2] MRS CInfinitesimal_add) 1);
   428 qed "capprox_add";
   429 
   430 Goal "a @c= b ==> -a @c= -b";
   431 by (rtac ((capprox_minus_iff RS iffD2) RS capprox_sym) 1);
   432 by (dtac (capprox_minus_iff RS iffD1) 1);
   433 by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
   434 qed "capprox_minus";
   435 
   436 Goal "-a @c= -b ==> a @c= b";
   437 by (auto_tac (claset() addDs [capprox_minus], simpset()));
   438 qed "capprox_minus2";
   439 
   440 Goal "(-a @c= -b) = (a @c= b)";
   441 by (blast_tac (claset() addIs [capprox_minus,capprox_minus2]) 1);
   442 qed "capprox_minus_cancel";
   443 Addsimps [capprox_minus_cancel];
   444 
   445 Goal "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d";
   446 by (blast_tac (claset() addSIs [capprox_add,capprox_minus]) 1);
   447 qed "capprox_add_minus";
   448 
   449 Goalw [capprox_def,hcomplex_diff_def] 
   450       "[| a @c= b; c: CFinite|] ==> a*c @c= b*c"; 
   451 by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_CFinite_mult,
   452     hcomplex_minus_mult_eq1,hcomplex_add_mult_distrib RS sym] 
   453     delsimps [hcomplex_minus_mult_eq1 RS sym]) 1);
   454 qed "capprox_mult1";
   455 
   456 Goal "[|a @c= b; c: CFinite|] ==> c*a @c= c*b"; 
   457 by (asm_simp_tac (simpset() addsimps [capprox_mult1,hcomplex_mult_commute]) 1);
   458 qed "capprox_mult2";
   459 
   460 Goal "[|u @c= v*x; x @c= y; v: CFinite|] ==> u @c= v*y";
   461 by (fast_tac (claset() addIs [capprox_mult2,capprox_trans]) 1);
   462 qed "capprox_mult_subst";
   463 
   464 Goal "[| u @c= x*v; x @c= y; v: CFinite |] ==> u @c= y*v";
   465 by (fast_tac (claset() addIs [capprox_mult1,capprox_trans]) 1);
   466 qed "capprox_mult_subst2";
   467 
   468 Goal "[| u @c= x*hcomplex_of_complex v; x @c= y |] ==> u @c= y*hcomplex_of_complex v";
   469 by (auto_tac (claset() addIs [capprox_mult_subst2], simpset()));
   470 qed "capprox_mult_subst_SComplex";
   471 
   472 Goalw [capprox_def]  "a = b ==> a @c= b";
   473 by (Asm_simp_tac 1);
   474 qed "capprox_eq_imp";
   475 
   476 Goal "x: CInfinitesimal ==> -x @c= x"; 
   477 by (fast_tac (HOL_cs addIs [CInfinitesimal_minus_iff RS iffD2,
   478     mem_cinfmal_iff RS iffD1,capprox_trans2]) 1);
   479 qed "CInfinitesimal_minus_capprox";
   480 
   481 Goalw [capprox_def]  
   482      "(EX y: CInfinitesimal. x - z = y) = (x @c= z)";
   483 by (Blast_tac 1);
   484 qed "bex_CInfinitesimal_iff";
   485 
   486 Goal "(EX y: CInfinitesimal. x = z + y) = (x @c= z)";
   487 by (asm_full_simp_tac (simpset() addsimps [bex_CInfinitesimal_iff RS sym]) 1);
   488 by (Force_tac 1);
   489 qed "bex_CInfinitesimal_iff2";
   490 
   491 Goal "[| y: CInfinitesimal; x + y = z |] ==> x @c= z";
   492 by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
   493 by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
   494 by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
   495 qed "CInfinitesimal_add_capprox";
   496 
   497 Goal "y: CInfinitesimal ==> x @c= x + y";
   498 by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
   499 by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
   500 by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
   501 qed "CInfinitesimal_add_capprox_self";
   502 
   503 Goal "y: CInfinitesimal ==> x @c= y + x";
   504 by (auto_tac (claset() addDs [CInfinitesimal_add_capprox_self],
   505     simpset() addsimps [hcomplex_add_commute]));
   506 qed "CInfinitesimal_add_capprox_self2";
   507 
   508 Goal "y: CInfinitesimal ==> x @c= x + -y";
   509 by (blast_tac (claset() addSIs [CInfinitesimal_add_capprox_self,
   510                                 CInfinitesimal_minus_iff RS iffD2]) 1);
   511 qed "CInfinitesimal_add_minus_capprox_self";
   512 
   513 Goal "[| y: CInfinitesimal; x+y @c= z|] ==> x @c= z";
   514 by (dres_inst_tac [("x","x")] (CInfinitesimal_add_capprox_self RS capprox_sym) 1);
   515 by (etac (capprox_trans3 RS capprox_sym) 1);
   516 by (assume_tac 1);
   517 qed "CInfinitesimal_add_cancel";
   518 
   519 Goal "[| y: CInfinitesimal; x @c= z + y|] ==> x @c= z";
   520 by (dres_inst_tac [("x","z")] (CInfinitesimal_add_capprox_self2  RS capprox_sym) 1);
   521 by (etac (capprox_trans3 RS capprox_sym) 1);
   522 by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
   523 by (etac capprox_sym 1);
   524 qed "CInfinitesimal_add_right_cancel";
   525 
   526 Goal "d + b  @c= d + c ==> b @c= c";
   527 by (dtac (capprox_minus_iff RS iffD1) 1);
   528 by (asm_full_simp_tac (simpset() addsimps 
   529     [hcomplex_minus_add_distrib,capprox_minus_iff RS sym] 
   530     @ hcomplex_add_ac) 1);
   531 qed "capprox_add_left_cancel";
   532 
   533 Goal "b + d @c= c + d ==> b @c= c";
   534 by (rtac capprox_add_left_cancel 1);
   535 by (asm_full_simp_tac (simpset() addsimps 
   536     [hcomplex_add_commute]) 1);
   537 qed "capprox_add_right_cancel";
   538 
   539 Goal "b @c= c ==> d + b @c= d + c";
   540 by (rtac (capprox_minus_iff RS iffD2) 1);
   541 by (asm_full_simp_tac (simpset() addsimps 
   542     [capprox_minus_iff RS sym] @ hcomplex_add_ac) 1);
   543 qed "capprox_add_mono1";
   544 
   545 Goal "b @c= c ==> b + a @c= c + a";
   546 by (asm_simp_tac (simpset() addsimps 
   547     [hcomplex_add_commute,capprox_add_mono1]) 1);
   548 qed "capprox_add_mono2";
   549 
   550 Goal "(a + b @c= a + c) = (b @c= c)";
   551 by (fast_tac (claset() addEs [capprox_add_left_cancel,
   552     capprox_add_mono1]) 1);
   553 qed "capprox_add_left_iff";
   554 
   555 AddIffs [capprox_add_left_iff];
   556 
   557 
   558 Goal "(b + a @c= c + a) = (b @c= c)";
   559 by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
   560 qed "capprox_add_right_iff";
   561 
   562 AddIffs [capprox_add_right_iff];
   563 
   564 Goal "[| x: CFinite; x @c= y |] ==> y: CFinite";
   565 by (dtac (bex_CInfinitesimal_iff2 RS iffD2) 1);
   566 by (Step_tac 1);
   567 by (dtac (CInfinitesimal_subset_CFinite RS subsetD 
   568           RS (CFinite_minus_iff RS iffD2)) 1);
   569 by (dtac CFinite_add 1);
   570 by (assume_tac 1 THEN Auto_tac);
   571 qed "capprox_CFinite";
   572 
   573 Goal "x @c= hcomplex_of_complex D ==> x: CFinite";
   574 by (rtac (capprox_sym RSN (2,capprox_CFinite)) 1);
   575 by Auto_tac;
   576 qed "capprox_hcomplex_of_complex_CFinite";
   577 
   578 Goal "[|a @c= b; c @c= d; b: CFinite; d: CFinite|] ==> a*c @c= b*d";
   579 by (rtac capprox_trans 1); 
   580 by (rtac capprox_mult2 2); 
   581 by (rtac capprox_mult1 1);
   582 by (blast_tac (claset() addIs [capprox_CFinite, capprox_sym]) 2);  
   583 by Auto_tac;  
   584 qed "capprox_mult_CFinite";
   585 
   586 Goal "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |] \
   587 \     ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d";
   588 by (blast_tac (claset() addSIs [capprox_mult_CFinite,
   589             capprox_hcomplex_of_complex_CFinite,CFinite_hcomplex_of_complex]) 1);
   590 qed "capprox_mult_hcomplex_of_complex";
   591 
   592 Goal "[| a: SComplex; a ~= 0; a*x @c= 0 |] ==> x @c= 0";
   593 by (dtac (SComplex_inverse RS (SComplex_subset_CFinite RS subsetD)) 1);
   594 by (auto_tac (claset() addDs [capprox_mult2],
   595     simpset() addsimps [hcomplex_mult_assoc RS sym]));
   596 qed "capprox_SComplex_mult_cancel_zero";
   597 
   598 Goal "[| a: SComplex; x @c= 0 |] ==> x*a @c= 0";
   599 by (auto_tac (claset() addDs [(SComplex_subset_CFinite RS subsetD),
   600               capprox_mult1], simpset()));
   601 qed "capprox_mult_SComplex1";
   602 
   603 Goal "[| a: SComplex; x @c= 0 |] ==> a*x @c= 0";
   604 by (auto_tac (claset() addDs [(SComplex_subset_CFinite RS subsetD),
   605               capprox_mult2], simpset()));
   606 qed "capprox_mult_SComplex2";
   607 
   608 Goal "[|a : SComplex; a ~= 0 |] ==> (a*x @c= 0) = (x @c= 0)";
   609 by (blast_tac (claset() addIs [capprox_SComplex_mult_cancel_zero,
   610     capprox_mult_SComplex2]) 1);
   611 qed "capprox_mult_SComplex_zero_cancel_iff";
   612 Addsimps [capprox_mult_SComplex_zero_cancel_iff];
   613 
   614 Goal "[| a: SComplex; a ~= 0; a* w @c= a*z |] ==> w @c= z";
   615 by (dtac (SComplex_inverse RS (SComplex_subset_CFinite RS subsetD)) 1);
   616 by (auto_tac (claset() addDs [capprox_mult2],
   617     simpset() addsimps [hcomplex_mult_assoc RS sym]));
   618 qed "capprox_SComplex_mult_cancel";
   619 
   620 Goal "[| a: SComplex; a ~= 0|] ==> (a* w @c= a*z) = (w @c= z)";
   621 by (auto_tac (claset() addSIs [capprox_mult2,SComplex_subset_CFinite RS subsetD] 
   622     addIs [capprox_SComplex_mult_cancel], simpset()));
   623 qed "capprox_SComplex_mult_cancel_iff1";
   624 Addsimps [capprox_SComplex_mult_cancel_iff1];
   625 
   626 Goal "(x @c= y) = (hcmod (y - x) @= 0)";
   627 by (rtac (capprox_minus_iff RS ssubst) 1);
   628 by (auto_tac (claset(),simpset() addsimps [capprox_def,
   629     CInfinitesimal_hcmod_iff,mem_infmal_iff,symmetric hcomplex_diff_def,
   630     hcmod_diff_commute]));
   631 qed "capprox_hcmod_approx_zero";
   632 
   633 Goal "(x @c= 0) = (hcmod x @= 0)";
   634 by (auto_tac (claset(),simpset() addsimps 
   635     [capprox_hcmod_approx_zero]));
   636 qed "capprox_approx_zero_iff";
   637 
   638 Goal "(-x @c= 0) = (x @c= 0)";
   639 by (auto_tac (claset(),simpset() addsimps 
   640     [capprox_hcmod_approx_zero]));
   641 qed "capprox_minus_zero_cancel_iff";
   642 Addsimps [capprox_minus_zero_cancel_iff];
   643 
   644 Goal "u @c= 0 ==> hcmod(x + u) - hcmod x : Infinitesimal";
   645 by (res_inst_tac [("e","hcmod u"),("e'","- hcmod u")] Infinitesimal_interval2 1);
   646 by (auto_tac (claset() addDs [capprox_approx_zero_iff RS iffD1], 
   647     simpset() addsimps [mem_infmal_iff RS sym,hypreal_diff_def]));
   648 by (res_inst_tac [("C","hcmod x")] hypreal_le_add_left_cancel 1);
   649 by (auto_tac (claset(),simpset() addsimps [symmetric hypreal_diff_def]));
   650 qed "Infinitesimal_hcmod_add_diff";
   651 
   652 Goal "u @c= 0 ==> hcmod(x + u) @= hcmod x";
   653 by (rtac (approx_minus_iff RS iffD2) 1);
   654 by (auto_tac (claset() addIs [Infinitesimal_hcmod_add_diff],
   655     simpset() addsimps [mem_infmal_iff RS sym,symmetric hypreal_diff_def]));
   656 qed "approx_hcmod_add_hcmod";
   657 
   658 Goal "x @c= y ==> hcmod x @= hcmod y";
   659 by (auto_tac (claset() addIs [approx_hcmod_add_hcmod] 
   660     addSDs [bex_CInfinitesimal_iff2 RS iffD2],simpset() addsimps [mem_cinfmal_iff]));
   661 qed "capprox_hcmod_approx";
   662 
   663 (*--------------------------------------------------------------------------------------*)
   664 (* zero is the only complex number that is also infinitesimal                           *)
   665 (*--------------------------------------------------------------------------------------*)
   666 
   667 Goal "[| x: SComplex; y: CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x";
   668 by (auto_tac (claset() addSIs [Infinitesimal_less_SReal,SComplex_hcmod_SReal],
   669     simpset() addsimps [CInfinitesimal_hcmod_iff]));
   670 qed "CInfinitesimal_less_SComplex";
   671 
   672 Goal "y: CInfinitesimal ==> ALL r: SComplex. 0 < hcmod r --> hcmod y < hcmod r";
   673 by (blast_tac (claset() addIs [CInfinitesimal_less_SComplex]) 1);
   674 qed "CInfinitesimal_less_SComplex2";
   675 
   676 Goal "SComplex Int CInfinitesimal = {0}";
   677 by (auto_tac (claset(),simpset() addsimps [SComplex_def,CInfinitesimal_hcmod_iff]));
   678 by (cut_inst_tac [("r","r")] SReal_hcmod_hcomplex_of_complex 1);
   679 by (dres_inst_tac [("A","Reals")] IntI 1 THEN assume_tac 1);
   680 by (subgoal_tac "hcmod (hcomplex_of_complex r) = 0" 1);
   681 by (Asm_full_simp_tac 1);
   682 by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
   683 by (rotate_tac 2 1);
   684 by (Asm_full_simp_tac 1);
   685 qed "SComplex_Int_CInfinitesimal_zero";
   686 
   687 Goal "[| x: SComplex; x: CInfinitesimal|] ==> x = 0";
   688 by (cut_facts_tac [SComplex_Int_CInfinitesimal_zero] 1);
   689 by (Blast_tac 1);
   690 qed "SComplex_CInfinitesimal_zero";
   691 
   692 Goal "[| x : SComplex; x ~= 0 |] ==> x : CFinite - CInfinitesimal";
   693 by (auto_tac (claset() addDs [SComplex_CInfinitesimal_zero,
   694                               SComplex_subset_CFinite RS subsetD], 
   695               simpset()));
   696 qed "SComplex_CFinite_diff_CInfinitesimal";
   697 
   698 Goal "hcomplex_of_complex x ~= 0 ==> hcomplex_of_complex x : CFinite - CInfinitesimal";
   699 by (rtac SComplex_CFinite_diff_CInfinitesimal 1);
   700 by Auto_tac;
   701 qed "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
   702 
   703 Goal "(hcomplex_of_complex x : CInfinitesimal) = (x=0)";
   704 by (auto_tac (claset(), simpset() addsimps [hcomplex_of_complex_zero]));  
   705 by (rtac ccontr 1); 
   706 by (rtac (hcomplex_of_complex_CFinite_diff_CInfinitesimal RS DiffD2) 1); 
   707 by Auto_tac;  
   708 qed "hcomplex_of_complex_CInfinitesimal_iff_0";
   709 AddIffs [hcomplex_of_complex_CInfinitesimal_iff_0];
   710 
   711 Goal "number_of w ~= (0::hcomplex) ==> number_of w ~: CInfinitesimal";
   712 by (fast_tac (claset() addDs [SComplex_number_of RS SComplex_CInfinitesimal_zero]) 1);
   713 qed "number_of_not_CInfinitesimal";
   714 Addsimps [number_of_not_CInfinitesimal];
   715 
   716 Goal "[| y: SComplex; x @c= y; y~= 0 |] ==> x ~= 0";
   717 by (auto_tac (claset() addDs [SComplex_CInfinitesimal_zero,
   718     capprox_sym RS (mem_cinfmal_iff RS iffD2)],simpset()));
   719 qed "capprox_SComplex_not_zero";
   720 
   721 Goal "[| x @c= y; y : CFinite - CInfinitesimal |] \
   722 \     ==> x : CFinite - CInfinitesimal";
   723 by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)],
   724               simpset() addsimps [mem_cinfmal_iff]));
   725 by (dtac capprox_trans3 1 THEN assume_tac 1);
   726 by (blast_tac (claset() addDs [capprox_sym]) 1);
   727 qed "CFinite_diff_CInfinitesimal_capprox";
   728 
   729 Goal "[| y ~= 0;  y: CInfinitesimal;  x/y : CFinite |] ==> x : CInfinitesimal";
   730 by (dtac CInfinitesimal_CFinite_mult2 1);
   731 by (assume_tac 1);
   732 by (asm_full_simp_tac 
   733     (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 1);
   734 qed "CInfinitesimal_ratio";
   735 
   736 Goal "[|x: SComplex; y: SComplex|] ==> (x @c= y) = (x = y)"; 
   737 by Auto_tac;
   738 by (rewrite_goals_tac [capprox_def]);
   739 by (dres_inst_tac [("x","y")] SComplex_minus 1);
   740 by (dtac SComplex_add 1 THEN assume_tac 1);
   741 by (rtac (CLAIM "x - y = 0 ==> x = (y::hcomplex)") 1);
   742 by (rtac SComplex_CInfinitesimal_zero 1);
   743 by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]));
   744 qed "SComplex_capprox_iff";
   745 
   746 Goal "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))";
   747 by (rtac SComplex_capprox_iff 1); 
   748 by Auto_tac;  
   749 qed "number_of_capprox_iff";
   750 Addsimps [number_of_capprox_iff];
   751 
   752 Goal "(number_of w : CInfinitesimal) = (number_of w = (0::hcomplex))";
   753 by (rtac iffI 1);
   754 by (fast_tac (claset() addDs [SComplex_number_of RS SComplex_CInfinitesimal_zero]) 1);
   755 by (Asm_simp_tac 1);
   756 qed "number_of_CInfinitesimal_iff";
   757 Addsimps [number_of_CInfinitesimal_iff];
   758 
   759 Goal "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)";
   760 by Auto_tac;  
   761 by (rtac (inj_hcomplex_of_complex RS injD) 1); 
   762 by (rtac (SComplex_capprox_iff RS iffD1) 1); 
   763 by Auto_tac;  
   764 qed "hcomplex_of_complex_approx_iff";
   765 Addsimps [hcomplex_of_complex_approx_iff];
   766 
   767 Goal "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)";
   768 by (stac (hcomplex_of_complex_approx_iff RS sym) 1); 
   769 by Auto_tac;  
   770 qed "hcomplex_of_complex_capprox_number_of_iff";
   771 Addsimps [hcomplex_of_complex_capprox_number_of_iff];
   772 
   773 Goal "[| r: SComplex; s: SComplex; r @c= x; s @c= x|] ==> r = s";
   774 by (blast_tac (claset() addIs [(SComplex_capprox_iff RS iffD1),
   775                capprox_trans2]) 1);
   776 qed "capprox_unique_complex";
   777 
   778 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) \
   779 \     ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @= \
   780 \         Abs_hypreal(hyprel `` {%n. Re(Y n)})";
   781 by (auto_tac (claset(),simpset() addsimps [approx_FreeUltrafilterNat_iff]));
   782 by (dtac (capprox_minus_iff RS iffD1) 1);
   783 by (auto_tac (claset(),simpset() addsimps [hcomplex_minus,hcomplex_add,
   784     mem_cinfmal_iff RS sym,CInfinitesimal_hcmod_iff,hcmod,
   785     Infinitesimal_FreeUltrafilterNat_iff2]));
   786 by (dres_inst_tac [("x","m")] spec 1);
   787 by (Ultra_tac 1);
   788 by (rename_tac "Z x" 1);
   789 by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
   790 by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
   791 by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
   792     complex_mod] delsimps [realpow_Suc]));
   793 by (rtac order_le_less_trans 1 THEN assume_tac 2);
   794 by (dres_inst_tac [("t","Z x")] sym 1);
   795 by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
   796 qed "hcomplex_capproxD1";
   797 
   798 (* same proof *)
   799 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) \
   800 \     ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @= \
   801 \         Abs_hypreal(hyprel `` {%n. Im(Y n)})";
   802 by (auto_tac (claset(),simpset() addsimps [approx_FreeUltrafilterNat_iff]));
   803 by (dtac (capprox_minus_iff RS iffD1) 1);
   804 by (auto_tac (claset(),simpset() addsimps [hcomplex_minus,hcomplex_add,
   805     mem_cinfmal_iff RS sym,CInfinitesimal_hcmod_iff,hcmod,
   806     Infinitesimal_FreeUltrafilterNat_iff2]));
   807 by (dres_inst_tac [("x","m")] spec 1);
   808 by (Ultra_tac 1);
   809 by (rename_tac "Z x" 1);
   810 by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
   811 by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
   812 by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
   813     complex_mod] delsimps [realpow_Suc]));
   814 by (rtac order_le_less_trans 1 THEN assume_tac 2);
   815 by (dres_inst_tac [("t","Z x")] sym 1);
   816 by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
   817 qed "hcomplex_capproxD2";
   818 
   819 Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @= \
   820 \        Abs_hypreal(hyprel `` {%n. Re(Y n)}); \
   821 \        Abs_hypreal(hyprel `` {%n. Im(X n)}) @= \
   822 \        Abs_hypreal(hyprel `` {%n. Im(Y n)}) \
   823 \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})";
   824 by (dtac (approx_minus_iff RS iffD1) 1);
   825 by (dtac (approx_minus_iff RS iffD1) 1);
   826 by (rtac (capprox_minus_iff RS iffD2) 1);
   827 by (auto_tac (claset(),simpset() addsimps [mem_cinfmal_iff RS sym,
   828     mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
   829     hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_FreeUltrafilterNat_iff]));
   830 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   831 by Auto_tac;
   832 by (dres_inst_tac [("x","u/2")] spec 1);
   833 by (dres_inst_tac [("x","u/2")] spec 1);
   834 by (Step_tac 1);
   835 by (TRYALL(Force_tac));
   836 by (ultra_tac (claset(),HOL_ss) 1);
   837 by (dtac sym 1 THEN dtac sym 1);
   838 by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
   839 by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
   840 by (auto_tac (claset(),HOL_ss addsimps [complex_minus,complex_add,
   841     complex_mod,pair_mem_complex RS Abs_complex_inverse,snd_conv,
   842     fst_conv,two_eq_Suc_Suc]));
   843 by (rtac (realpow_two_abs RS subst) 1);
   844 by (res_inst_tac [("x1","xa + - xb")] (realpow_two_abs RS subst) 1);
   845 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1);
   846 by (rtac lemma_sqrt_hcomplex_capprox 1);
   847 by Auto_tac;
   848 qed "hcomplex_capproxI";
   849 
   850 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) =\
   851 \      (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) & \
   852 \       Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))";
   853 by (blast_tac (claset() addIs [hcomplex_capproxI,hcomplex_capproxD1,hcomplex_capproxD2]) 1);
   854 qed "capprox_approx_iff";
   855 
   856 Goal "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)";
   857 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   858 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   859 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
   860     capprox_approx_iff]));
   861 qed "hcomplex_of_hypreal_capprox_iff";
   862 Addsimps [hcomplex_of_hypreal_capprox_iff];
   863 
   864 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite \
   865 \     ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite";
   866 by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
   867     hcmod,HFinite_FreeUltrafilterNat_iff]));
   868 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   869 by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
   870 by (Ultra_tac 1);
   871 by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
   872 by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc]));
   873 by (rtac ccontr 1 THEN dtac real_leI 1);
   874 by (dtac order_less_le_trans 1 THEN assume_tac 1);
   875 by (dtac (real_sqrt_ge_abs1 RSN (2,order_less_le_trans)) 1);
   876 by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc RS sym]));
   877 qed "CFinite_HFinite_Re";
   878 
   879 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite \
   880 \     ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite";
   881 by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
   882     hcmod,HFinite_FreeUltrafilterNat_iff]));
   883 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   884 by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
   885 by (Ultra_tac 1);
   886 by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
   887 by (auto_tac (claset(),simpset() addsimps [complex_mod] delsimps [realpow_Suc]));
   888 by (rtac ccontr 1 THEN dtac real_leI 1);
   889 by (dtac order_less_le_trans 1 THEN assume_tac 1);
   890 by (dtac (real_sqrt_ge_abs2 RSN (2,order_less_le_trans)) 1);
   891 by Auto_tac;
   892 qed "CFinite_HFinite_Im";
   893 
   894 Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite; \
   895 \        Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite \
   896 \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite";
   897 by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
   898     hcmod,HFinite_FreeUltrafilterNat_iff]));
   899 by (rename_tac "Y Z u v" 1);
   900 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
   901 by (res_inst_tac [("x","2*(u + v)")] exI 1);
   902 by (Ultra_tac 1);
   903 by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
   904 by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc]));
   905 by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
   906 by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
   907 by (rtac (realpow_two_abs RS subst) 1);
   908 by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1);
   909 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1);
   910 by (rtac lemma_sqrt_hcomplex_capprox 1);
   911 by Auto_tac;
   912 qed "HFinite_Re_Im_CFinite";
   913 
   914 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite) = \
   915 \     (Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite & \
   916 \      Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite)";
   917 by (blast_tac (claset() addIs [HFinite_Re_Im_CFinite,CFinite_HFinite_Im,
   918     CFinite_HFinite_Re]) 1);
   919 qed "CFinite_HFinite_iff";
   920 
   921 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex \
   922 \     ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals";
   923 by (auto_tac (claset(),simpset() addsimps [SComplex_def,
   924     hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
   925 by (res_inst_tac [("x","Re r")] exI 1);
   926 by (Ultra_tac 1);
   927 qed "SComplex_Re_SReal";
   928 
   929 Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex \
   930 \     ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals";
   931 by (auto_tac (claset(),simpset() addsimps [SComplex_def,
   932     hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
   933 by (res_inst_tac [("x","Im r")] exI 1);
   934 by (Ultra_tac 1);
   935 qed "SComplex_Im_SReal";
   936 
   937 Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals; \
   938 \        Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals \
   939 \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex";
   940 by (auto_tac (claset(),simpset() addsimps [SComplex_def,
   941     hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
   942 by (res_inst_tac [("x","complex_of_real r + ii  * complex_of_real ra")] exI 1);
   943 by (Ultra_tac 1);
   944 by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
   945 by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
   946     complex_add,complex_mult]));
   947 qed "Reals_Re_Im_SComplex";
   948 
   949 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \
   950 \     (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals & \
   951 \      Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals)";
   952 by (blast_tac (claset() addIs [SComplex_Re_SReal,SComplex_Im_SReal,
   953     Reals_Re_Im_SComplex]) 1);
   954 qed "SComplex_SReal_iff";
   955 
   956 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CInfinitesimal) = \
   957 \     (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Infinitesimal & \
   958 \      Abs_hypreal(hyprel `` {%n. Im(X n)}) : Infinitesimal)";
   959 by (auto_tac (claset(),simpset() addsimps [mem_cinfmal_iff,
   960     mem_infmal_iff,hcomplex_zero_num,hypreal_zero_num,capprox_approx_iff]));
   961 qed "CInfinitesimal_Infinitesimal_iff";
   962 
   963 (*** more lemmas ****)
   964 Goal "(EX t. P t) = (EX X. P (Abs_hcomplex(hcomplexrel `` {X})))";
   965 by Auto_tac;
   966 by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1);
   967 by Auto_tac;
   968 qed "eq_Abs_hcomplex_EX";
   969 
   970 Goal "(EX t : A. P t) = (EX X. (Abs_hcomplex(hcomplexrel `` {X})) : A & \
   971 \                        P (Abs_hcomplex(hcomplexrel `` {X})))";
   972 by Auto_tac;
   973 by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1);
   974 by Auto_tac;
   975 qed "eq_Abs_hcomplex_Bex";
   976 
   977 (* Here we go - easy proof now!! *)
   978 Goal "x:CFinite ==> EX t: SComplex. x @c= t";
   979 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
   980 by (auto_tac (claset(),simpset() addsimps [CFinite_HFinite_iff,
   981     eq_Abs_hcomplex_Bex,SComplex_SReal_iff,capprox_approx_iff]));
   982 by (REPEAT(dtac st_part_Ex 1 THEN Step_tac 1));
   983 by (res_inst_tac [("z","t")] eq_Abs_hypreal 1);
   984 by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1);
   985 by Auto_tac;
   986 by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")]
   987     exI 1);
   988 by Auto_tac;
   989 qed "stc_part_Ex";
   990 
   991 Goal "x:CFinite ==> EX! t. t : SComplex &  x @c= t";
   992 by (dtac stc_part_Ex 1 THEN Step_tac 1);
   993 by (dtac capprox_sym 2 THEN dtac capprox_sym 2 
   994     THEN dtac capprox_sym 2);
   995 by (auto_tac (claset() addSIs [capprox_unique_complex], simpset()));
   996 qed "stc_part_Ex1";
   997 
   998 Goalw [CFinite_def,CInfinite_def] "CFinite Int CInfinite = {}";
   999 by Auto_tac;
  1000 qed "CFinite_Int_CInfinite_empty";
  1001 Addsimps [CFinite_Int_CInfinite_empty];
  1002 
  1003 Goal "x: CFinite ==> x ~: CInfinite";
  1004 by (EVERY1[Step_tac, dtac IntI, assume_tac]);
  1005 by Auto_tac;
  1006 qed "CFinite_not_CInfinite";
  1007 
  1008 Goal "x~: CFinite ==> x: CInfinite";
  1009 by (auto_tac (claset() addIs [not_HFinite_HInfinite],
  1010     simpset() addsimps [CFinite_hcmod_iff,CInfinite_hcmod_iff]));
  1011 qed "not_CFinite_CInfinite";
  1012 
  1013 Goal "x : CInfinite | x : CFinite";
  1014 by (blast_tac (claset() addIs [not_CFinite_CInfinite]) 1);
  1015 qed "CInfinite_CFinite_disj";
  1016 
  1017 Goal "(x : CInfinite) = (x ~: CFinite)";
  1018 by (blast_tac (claset() addDs [CFinite_not_CInfinite,
  1019                not_CFinite_CInfinite]) 1);
  1020 qed "CInfinite_CFinite_iff";
  1021 
  1022 Goal "(x : CFinite) = (x ~: CInfinite)";
  1023 by (simp_tac (simpset() addsimps [CInfinite_CFinite_iff]) 1);
  1024 qed "CFinite_CInfinite_iff";
  1025 
  1026 Goal "x ~: CInfinitesimal ==> x : CInfinite | x : CFinite - CInfinitesimal";
  1027 by (fast_tac (claset() addIs [not_CFinite_CInfinite]) 1);
  1028 qed "CInfinite_diff_CFinite_CInfinitesimal_disj";
  1029 
  1030 Goal "[| x : CFinite; x ~: CInfinitesimal |] ==> inverse x : CFinite";
  1031 by (cut_inst_tac [("x","inverse x")] CInfinite_CFinite_disj 1);
  1032 by (auto_tac (claset() addSDs [CInfinite_inverse_CInfinitesimal], simpset()));
  1033 qed "CFinite_inverse";
  1034 
  1035 Goal "x : CFinite - CInfinitesimal ==> inverse x : CFinite";
  1036 by (blast_tac (claset() addIs [CFinite_inverse]) 1);
  1037 qed "CFinite_inverse2";
  1038 
  1039 Goal "x ~: CInfinitesimal ==> inverse(x) : CFinite";
  1040 by (dtac CInfinite_diff_CFinite_CInfinitesimal_disj 1);
  1041 by (blast_tac (claset() addIs [CFinite_inverse,
  1042                  CInfinite_inverse_CInfinitesimal,
  1043                  CInfinitesimal_subset_CFinite RS subsetD]) 1);
  1044 qed "CInfinitesimal_inverse_CFinite";
  1045 
  1046 
  1047 Goal "x : CFinite - CInfinitesimal ==> inverse x : CFinite - CInfinitesimal";
  1048 by (auto_tac (claset() addIs [CInfinitesimal_inverse_CFinite], simpset()));
  1049 by (dtac CInfinitesimal_CFinite_mult2 1);
  1050 by (assume_tac 1);
  1051 by (asm_full_simp_tac (simpset() addsimps [not_CInfinitesimal_not_zero]) 1); 
  1052 qed "CFinite_not_CInfinitesimal_inverse";
  1053 
  1054 Goal "[| x @c= y; y :  CFinite - CInfinitesimal |] \
  1055 \     ==> inverse x @c= inverse y";
  1056 by (forward_tac [CFinite_diff_CInfinitesimal_capprox] 1);
  1057 by (assume_tac 1);
  1058 by (forward_tac [not_CInfinitesimal_not_zero2] 1);
  1059 by (forw_inst_tac [("x","x")] not_CInfinitesimal_not_zero2 1);
  1060 by (REPEAT(dtac CFinite_inverse2 1));
  1061 by (dtac capprox_mult2 1 THEN assume_tac 1);
  1062 by Auto_tac;
  1063 by (dres_inst_tac [("c","inverse x")] capprox_mult1 1 
  1064     THEN assume_tac 1);
  1065 by (auto_tac (claset() addIs [capprox_sym],
  1066     simpset() addsimps [hcomplex_mult_assoc]));
  1067 qed "capprox_inverse";
  1068 
  1069 bind_thm ("hcomplex_of_complex_capprox_inverse",
  1070        hcomplex_of_complex_CFinite_diff_CInfinitesimal RSN (2, capprox_inverse));
  1071 
  1072 Goal "[| x: CFinite - CInfinitesimal; \
  1073 \        h : CInfinitesimal |] ==> inverse(x + h) @c= inverse x";
  1074 by (auto_tac (claset() addIs [capprox_inverse, capprox_sym, 
  1075                               CInfinitesimal_add_capprox_self], 
  1076               simpset()));
  1077 qed "inverse_add_CInfinitesimal_capprox";
  1078 
  1079 Goal "[| x: CFinite - CInfinitesimal; \
  1080 \        h : CInfinitesimal |] ==> inverse(h + x) @c= inverse x";
  1081 by (rtac (hcomplex_add_commute RS subst) 1);
  1082 by (blast_tac (claset() addIs [inverse_add_CInfinitesimal_capprox]) 1);
  1083 qed "inverse_add_CInfinitesimal_capprox2";
  1084 
  1085 Goal "[| x : CFinite - CInfinitesimal; \
  1086 \        h : CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h"; 
  1087 by (rtac capprox_trans2 1);
  1088 by (auto_tac (claset() addIs [inverse_add_CInfinitesimal_capprox],
  1089               simpset() addsimps [mem_cinfmal_iff,hcomplex_diff_def,
  1090                                   capprox_minus_iff RS sym]));
  1091 qed "inverse_add_CInfinitesimal_approx_CInfinitesimal";
  1092 
  1093 Goal "(x*x : CInfinitesimal) = (x : CInfinitesimal)";
  1094 by (auto_tac (claset(), simpset() addsimps [CInfinitesimal_hcmod_iff,
  1095     hcmod_mult]));
  1096 qed "CInfinitesimal_square_iff";
  1097 AddIffs [CInfinitesimal_square_iff];
  1098 
  1099 Goal "[| a: CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z";
  1100 by (Step_tac 1);
  1101 by (ftac CFinite_inverse 1 THEN assume_tac 1);
  1102 by (dtac not_CInfinitesimal_not_zero 1);
  1103 by (auto_tac (claset() addDs [capprox_mult2],
  1104     simpset() addsimps [hcomplex_mult_assoc RS sym]));
  1105 qed "capprox_CFinite_mult_cancel";
  1106 
  1107 Goal "a: CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)";
  1108 by (auto_tac (claset() addIs [capprox_mult2,
  1109     capprox_CFinite_mult_cancel], simpset()));
  1110 qed "capprox_CFinite_mult_cancel_iff1";
  1111 
  1112 
  1113 (*---------------------------------------------------------------------------*)
  1114 (* Theorems about monads                                                     *)
  1115 (*---------------------------------------------------------------------------*)
  1116 
  1117 Goalw [cmonad_def] "(x @c= y) = (cmonad(x)=cmonad(y))";
  1118 by (auto_tac (claset() addDs [capprox_sym] 
  1119                        addSEs [capprox_trans,equalityCE],
  1120               simpset()));
  1121 qed "capprox_cmonad_iff";
  1122 
  1123 Goal "e : CInfinitesimal ==> cmonad (x+e) = cmonad x";
  1124 by (fast_tac (claset() addSIs [CInfinitesimal_add_capprox_self RS capprox_sym,
  1125     capprox_cmonad_iff RS iffD1]) 1);
  1126 qed "CInfinitesimal_cmonad_eq";
  1127 
  1128 Goalw [cmonad_def] "(u:cmonad x) = (-u:cmonad (-x))";
  1129 by Auto_tac;
  1130 qed "mem_cmonad_iff";
  1131 
  1132 Goalw [cmonad_def] "(x:CInfinitesimal) = (x:cmonad 0)";
  1133 by (auto_tac (claset() addIs [capprox_sym],
  1134     simpset() addsimps [mem_cinfmal_iff]));
  1135 qed "CInfinitesimal_cmonad_zero_iff";
  1136 
  1137 Goal "(x:cmonad 0) = (-x:cmonad 0)";
  1138 by (simp_tac (simpset() addsimps [CInfinitesimal_cmonad_zero_iff RS sym]) 1);
  1139 qed "cmonad_zero_minus_iff";
  1140 
  1141 Goal "(x:cmonad 0) = (hcmod x:monad 0)";
  1142 by (auto_tac (claset(), simpset() addsimps 
  1143     [CInfinitesimal_cmonad_zero_iff RS sym,
  1144      CInfinitesimal_hcmod_iff,Infinitesimal_monad_zero_iff RS sym]));
  1145 qed "cmonad_zero_hcmod_iff";
  1146 
  1147 Goalw [cmonad_def] "x:cmonad x";
  1148 by (Simp_tac 1);
  1149 qed "mem_cmonad_self";
  1150 Addsimps [mem_cmonad_self];
  1151 
  1152 (*---------------------------------------------------------------------------*)
  1153 (* Theorems about standard part                                              *)
  1154 (*---------------------------------------------------------------------------*)
  1155 Goalw [stc_def] "x: CFinite ==> stc x @c= x";
  1156 by (forward_tac [stc_part_Ex] 1 THEN Step_tac 1);
  1157 by (rtac someI2 1);
  1158 by (auto_tac (claset() addIs [capprox_sym], simpset()));
  1159 qed "stc_capprox_self";
  1160 
  1161 Goalw [stc_def] "x: CFinite ==> stc x: SComplex";
  1162 by (forward_tac [stc_part_Ex] 1 THEN Step_tac 1);
  1163 by (rtac someI2 1);
  1164 by (auto_tac (claset() addIs [capprox_sym], simpset()));
  1165 qed "stc_SComplex";
  1166 
  1167 Goal "x: CFinite ==> stc x: CFinite";
  1168 by (etac (stc_SComplex RS (SComplex_subset_CFinite RS subsetD)) 1);
  1169 qed "stc_CFinite";
  1170 
  1171 Goalw [stc_def] "x: SComplex ==> stc x = x";
  1172 by (rtac some_equality 1);
  1173 by (auto_tac (claset() addIs [(SComplex_subset_CFinite RS subsetD)],simpset()));
  1174 by (blast_tac (claset() addDs [SComplex_capprox_iff RS iffD1]) 1);
  1175 qed "stc_SComplex_eq";
  1176 Addsimps [stc_SComplex_eq];
  1177 
  1178 Goal "stc (hcomplex_of_complex x) = hcomplex_of_complex x";
  1179 by Auto_tac;
  1180 qed "stc_hcomplex_of_complex";
  1181 
  1182 Goal "[| x: CFinite; y: CFinite; stc x = stc y |] ==> x @c= y";
  1183 by (auto_tac (claset() addSDs [stc_capprox_self] 
  1184               addSEs [capprox_trans3], simpset()));
  1185 qed "stc_eq_capprox";
  1186 
  1187 Goal "[| x: CFinite; y: CFinite; x @c= y |] ==> stc x = stc y";
  1188 by (EVERY1 [forward_tac [stc_capprox_self],
  1189     forw_inst_tac [("x","y")] stc_capprox_self,
  1190     dtac stc_SComplex,dtac stc_SComplex]);
  1191 by (fast_tac (claset() addEs [capprox_trans,
  1192     capprox_trans2,SComplex_capprox_iff RS iffD1]) 1);
  1193 qed "capprox_stc_eq";
  1194 
  1195 Goal "[| x: CFinite; y: CFinite|] ==> (x @c= y) = (stc x = stc y)";
  1196 by (blast_tac (claset() addIs [capprox_stc_eq,stc_eq_capprox]) 1);
  1197 qed "stc_eq_capprox_iff";
  1198 
  1199 Goal "[| x: SComplex; e: CInfinitesimal |] ==> stc(x + e) = x";
  1200 by (forward_tac [stc_SComplex_eq RS subst] 1);
  1201 by (assume_tac 2);
  1202 by (forward_tac [SComplex_subset_CFinite RS subsetD] 1);
  1203 by (forward_tac [CInfinitesimal_subset_CFinite RS subsetD] 1);
  1204 by (dtac stc_SComplex_eq 1);
  1205 by (rtac capprox_stc_eq 1);
  1206 by (auto_tac (claset() addIs  [CFinite_add],
  1207     simpset() addsimps [CInfinitesimal_add_capprox_self 
  1208     RS capprox_sym]));
  1209 qed "stc_CInfinitesimal_add_SComplex";
  1210 
  1211 Goal "[| x: SComplex; e: CInfinitesimal |] ==> stc(e + x) = x";
  1212 by (rtac (hcomplex_add_commute RS subst) 1);
  1213 by (blast_tac (claset() addSIs [stc_CInfinitesimal_add_SComplex]) 1);
  1214 qed "stc_CInfinitesimal_add_SComplex2";
  1215 
  1216 Goal "x: CFinite ==> EX e: CInfinitesimal. x = stc(x) + e";
  1217 by (blast_tac (claset() addSDs [(stc_capprox_self RS 
  1218     capprox_sym),bex_CInfinitesimal_iff2 RS iffD2]) 1);
  1219 qed "CFinite_stc_CInfinitesimal_add";
  1220 
  1221 Goal "[| x: CFinite; y: CFinite |] ==> stc (x + y) = stc(x) + stc(y)";
  1222 by (forward_tac [CFinite_stc_CInfinitesimal_add] 1);
  1223 by (forw_inst_tac [("x","y")] CFinite_stc_CInfinitesimal_add 1);
  1224 by (Step_tac 1);
  1225 by (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))" 1);
  1226 by (dtac sym 2 THEN dtac sym 2);
  1227 by (Asm_full_simp_tac 2);
  1228 by (asm_simp_tac (simpset() addsimps hcomplex_add_ac) 1);
  1229 by (REPEAT(dtac stc_SComplex 1));
  1230 by (dtac SComplex_add 1 THEN assume_tac 1);
  1231 by (dtac CInfinitesimal_add 1 THEN assume_tac 1);
  1232 by (rtac (hcomplex_add_assoc RS subst) 1);
  1233 by (blast_tac (claset() addSIs [stc_CInfinitesimal_add_SComplex2]) 1);
  1234 qed "stc_add";
  1235 
  1236 Goal "stc (number_of w) = number_of w";
  1237 by (rtac (SComplex_number_of RS stc_SComplex_eq) 1);
  1238 qed "stc_number_of";
  1239 Addsimps [stc_number_of];
  1240 
  1241 Goal "stc 0 = 0";
  1242 by (Simp_tac 1);
  1243 qed "stc_zero";
  1244 Addsimps [stc_zero];
  1245 
  1246 Goal "stc 1 = 1";
  1247 by (Simp_tac 1);
  1248 qed "stc_one";
  1249 Addsimps [stc_one];
  1250 
  1251 Goal "y: CFinite ==> stc(-y) = -stc(y)";
  1252 by (forward_tac [CFinite_minus_iff RS iffD2] 1);
  1253 by (rtac hcomplex_add_minus_eq_minus 1);
  1254 by (dtac (stc_add RS sym) 1 THEN assume_tac 1);
  1255 by (asm_simp_tac (simpset() addsimps [add_commute]) 1); 
  1256 qed "stc_minus";
  1257 
  1258 Goalw [hcomplex_diff_def]
  1259      "[| x: CFinite; y: CFinite |] ==> stc (x-y) = stc(x) - stc(y)";
  1260 by (forw_inst_tac [("y1","y")] (stc_minus RS sym) 1);
  1261 by (dres_inst_tac [("x1","y")] (CFinite_minus_iff RS iffD2) 1);
  1262 by (auto_tac (claset() addIs [stc_add],simpset()));
  1263 qed "stc_diff";
  1264 
  1265 Goal "[| x: CFinite; y: CFinite; \
  1266 \        e: CInfinitesimal;       \
  1267 \        ea: CInfinitesimal |]   \
  1268 \      ==> e*y + x*ea + e*ea: CInfinitesimal";
  1269 by (forw_inst_tac [("x","e"),("y","y")] CInfinitesimal_CFinite_mult 1);
  1270 by (forw_inst_tac [("x","ea"),("y","x")] CInfinitesimal_CFinite_mult 2);
  1271 by (dtac CInfinitesimal_mult 3);
  1272 by (auto_tac (claset() addIs [CInfinitesimal_add],
  1273               simpset() addsimps hcomplex_add_ac @ hcomplex_mult_ac));
  1274 qed "lemma_stc_mult";
  1275 
  1276 Goal "[| x: CFinite; y: CFinite |] \
  1277 \              ==> stc (x * y) = stc(x) * stc(y)";
  1278 by (forward_tac [CFinite_stc_CInfinitesimal_add] 1);
  1279 by (forw_inst_tac [("x","y")] CFinite_stc_CInfinitesimal_add 1);
  1280 by (Step_tac 1);
  1281 by (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))" 1);
  1282 by (dtac sym 2 THEN dtac sym 2);
  1283 by (Asm_full_simp_tac 2);
  1284 by (thin_tac "x = stc x + e" 1);
  1285 by (thin_tac "y = stc y + ea" 1);
  1286 by (asm_full_simp_tac (simpset() addsimps 
  1287     [hcomplex_add_mult_distrib,hcomplex_add_mult_distrib2]) 1);
  1288 by (REPEAT(dtac stc_SComplex 1));
  1289 by (full_simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
  1290 by (rtac stc_CInfinitesimal_add_SComplex 1);
  1291 by (blast_tac (claset() addSIs [SComplex_mult]) 1);
  1292 by (REPEAT(dtac (SComplex_subset_CFinite RS subsetD) 1));
  1293 by (rtac (hcomplex_add_assoc RS subst) 1);
  1294 by (blast_tac (claset() addSIs [lemma_stc_mult]) 1);
  1295 qed "stc_mult";
  1296 
  1297 Goal "x: CInfinitesimal ==> stc x = 0";
  1298 by (rtac (stc_zero RS subst) 1);
  1299 by (rtac capprox_stc_eq 1);
  1300 by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite RS subsetD],
  1301               simpset() addsimps [mem_cinfmal_iff RS sym]));
  1302 qed "stc_CInfinitesimal";
  1303 
  1304 Goal "stc(x) ~= 0 ==> x ~: CInfinitesimal";
  1305 by (fast_tac (claset() addIs [stc_CInfinitesimal]) 1);
  1306 qed "stc_not_CInfinitesimal";
  1307 
  1308 Goal "[| x: CFinite; stc x ~= 0 |] \
  1309 \     ==> stc(inverse x) = inverse (stc x)";
  1310 by (res_inst_tac [("c1","stc x")] (hcomplex_mult_left_cancel RS iffD1) 1);
  1311 by (auto_tac (claset(),
  1312        simpset() addsimps [stc_mult RS sym, stc_not_CInfinitesimal,
  1313                            CFinite_inverse]));
  1314 by (stac right_inverse 1); 
  1315 by Auto_tac;  
  1316 qed "stc_inverse";
  1317 
  1318 Goal "[| x: CFinite; y: CFinite; stc y ~= 0 |] \
  1319 \     ==> stc(x/y) = (stc x) / (stc y)";
  1320 by (auto_tac (claset(),
  1321       simpset() addsimps [hcomplex_divide_def, stc_mult, stc_not_CInfinitesimal, 
  1322                           CFinite_inverse, stc_inverse]));
  1323 qed "stc_divide";
  1324 Addsimps [stc_divide];
  1325 
  1326 Goal "x: CFinite ==> stc(stc(x)) = stc(x)";
  1327 by (blast_tac (claset() addIs [stc_CFinite, stc_capprox_self,
  1328                                capprox_stc_eq]) 1);
  1329 qed "stc_idempotent";
  1330 Addsimps [stc_idempotent];
  1331 
  1332 Goal "z : HFinite ==> hcomplex_of_hypreal z : CFinite";
  1333 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
  1334 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
  1335     CFinite_HFinite_iff,symmetric hypreal_zero_def]));
  1336 qed "CFinite_HFinite_hcomplex_of_hypreal";
  1337 
  1338 Goal "x : Reals ==>  hcomplex_of_hypreal x : SComplex";
  1339 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1340 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
  1341     SComplex_SReal_iff,symmetric hypreal_zero_def]));
  1342 qed "SComplex_SReal_hcomplex_of_hypreal";
  1343 
  1344 Goalw [st_def,stc_def] 
  1345  "z : HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)";
  1346 by (ftac st_part_Ex 1 THEN Step_tac 1);
  1347 by (rtac someI2 1);
  1348 by (auto_tac (claset() addIs [approx_sym],simpset()));
  1349 by (dtac CFinite_HFinite_hcomplex_of_hypreal 1);
  1350 by (ftac stc_part_Ex 1 THEN Step_tac 1);
  1351 by (rtac someI2 1);
  1352 by (auto_tac (claset() addIs [capprox_sym] addSIs [capprox_unique_complex] 
  1353     addDs [SComplex_SReal_hcomplex_of_hypreal],simpset()));
  1354 qed "stc_hcomplex_of_hypreal";
  1355 
  1356 (*
  1357 Goal "x: CFinite ==> hcmod(stc x) = st(hcmod x)";
  1358 by (dtac stc_capprox_self 1);
  1359 by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym]));
  1360 
  1361 
  1362 approx_hcmod_add_hcmod
  1363 *)
  1364 
  1365 (*---------------------------------------------------------------------------*)
  1366 (* More nonstandard complex specific theorems                                *)        
  1367 (*---------------------------------------------------------------------------*)
  1368 Goal "(hcnj z : CInfinitesimal) = (z : CInfinitesimal)";
  1369 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
  1370 qed "CInfinitesimal_hcnj_iff";
  1371 Addsimps [CInfinitesimal_hcnj_iff];
  1372 
  1373 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CInfinite) = \
  1374 \     (Abs_hypreal(hyprel `` {%n. Re(X n)}) : HInfinite | \
  1375 \      Abs_hypreal(hyprel `` {%n. Im(X n)}) : HInfinite)";
  1376 by (auto_tac (claset(),simpset() addsimps [CInfinite_CFinite_iff,
  1377     HInfinite_HFinite_iff,CFinite_HFinite_iff]));
  1378 qed "CInfinite_HInfinite_iff";
  1379 
  1380 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CInfinitesimal) = \
  1381 \     (x : Infinitesimal & y : Infinitesimal)";
  1382 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1383 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1384 by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
  1385     hcomplex_of_hypreal,CInfinitesimal_Infinitesimal_iff]));
  1386 qed "hcomplex_split_CInfinitesimal_iff";
  1387 
  1388 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CFinite) = \
  1389 \     (x : HFinite & y : HFinite)";
  1390 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1391 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1392 by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
  1393     hcomplex_of_hypreal,CFinite_HFinite_iff]));
  1394 qed "hcomplex_split_CFinite_iff";
  1395 
  1396 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : SComplex) = \
  1397 \     (x : Reals & y : Reals)";
  1398 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1399 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1400 by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
  1401     hcomplex_of_hypreal,SComplex_SReal_iff]));
  1402 qed "hcomplex_split_SComplex_iff";
  1403 
  1404 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CInfinite) = \
  1405 \     (x : HInfinite | y : HInfinite)";
  1406 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1407 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1408 by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
  1409     hcomplex_of_hypreal,CInfinite_HInfinite_iff]));
  1410 qed "hcomplex_split_CInfinite_iff";
  1411 
  1412 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c= \
  1413 \      hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = \
  1414 \     (x @= x' & y @= y')";
  1415 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1416 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1417 by (res_inst_tac [("z","x'")] eq_Abs_hypreal 1);
  1418 by (res_inst_tac [("z","y'")] eq_Abs_hypreal 1);
  1419 by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
  1420     hcomplex_of_hypreal,capprox_approx_iff]));
  1421 qed "hcomplex_split_capprox_iff";
  1422 
  1423 (*** More theorems ***)
  1424 
  1425 Goal "ALL n. cmod (X n - x) < inverse (real (Suc n)) ==> \
  1426 \     Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x : CInfinitesimal";
  1427 by (auto_tac (claset(),simpset() addsimps [hcomplex_diff,
  1428     CInfinitesimal_hcmod_iff,hcomplex_of_complex_def,
  1429     Infinitesimal_FreeUltrafilterNat_iff,hcmod]));
  1430 by (rtac bexI 1 THEN Auto_tac);
  1431 by (auto_tac (claset() addDs [FreeUltrafilterNat_inverse_real_of_posnat,
  1432                   FreeUltrafilterNat_all,FreeUltrafilterNat_Int] 
  1433            addIs [order_less_trans, FreeUltrafilterNat_subset],
  1434       simpset()));
  1435 qed "complex_seq_to_hcomplex_CInfinitesimal";
  1436 
  1437 Goal "hcomplex_of_hypreal epsilon : CInfinitesimal";
  1438 by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
  1439 qed "CInfinitesimal_hcomplex_of_hypreal_epsilon";
  1440 Addsimps [CInfinitesimal_hcomplex_of_hypreal_epsilon];
  1441 
  1442 Goal "(hcomplex_of_complex z @c= 0) = (z = 0)";
  1443 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_zero RS sym]
  1444     delsimps [hcomplex_of_complex_zero]));
  1445 qed "hcomplex_of_complex_approx_zero_iff";
  1446 
  1447 Goal "(0 @c= hcomplex_of_complex z) = (z = 0)";
  1448 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_zero RS sym]
  1449     delsimps [hcomplex_of_complex_zero]));
  1450 qed "hcomplex_of_complex_approx_zero_iff2";
  1451 
  1452 Addsimps [hcomplex_of_complex_approx_zero_iff,hcomplex_of_complex_approx_zero_iff2];
  1453 
  1454