--- a/src/HOL/Complex/NSCA.ML Mon Feb 23 17:33:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1457 +0,0 @@
-(* Title : NSCA.ML
- Author : Jacques D. Fleuriot
- Copyright : 2001,2002 University of Edinburgh
- Description : Infinite, infinitesimal complex number etc!
-*)
-
-val complex_induct = thm"complex.induct";
-val hcomplex_number_of = thm"hcomplex_number_of";
-
-(*--------------------------------------------------------------------------------------*)
-(* Closure laws for members of (embedded) set standard complex SComplex *)
-(* -------------------------------------------------------------------------------------*)
-
-Goalw [SComplex_def] "[| (x::hcomplex): SComplex; y: SComplex |] ==> x + y: SComplex";
-by (Step_tac 1);
-by (res_inst_tac [("x","r + ra")] exI 1);
-by (Simp_tac 1);
-qed "SComplex_add";
-
-Goalw [SComplex_def] "[| (x::hcomplex): SComplex; y: SComplex |] ==> x * y: SComplex";
-by (Step_tac 1);
-by (res_inst_tac [("x","r * ra")] exI 1);
-by (Simp_tac 1);
-qed "SComplex_mult";
-
-Goalw [SComplex_def] "x: SComplex ==> inverse x : SComplex";
-by (blast_tac (claset() addIs [hcomplex_of_complex_inverse RS sym]) 1);
-qed "SComplex_inverse";
-
-Goal "[| x: SComplex; y: SComplex |] ==> x/y: SComplex";
-by (asm_simp_tac (simpset() addsimps [SComplex_mult,SComplex_inverse,
- hcomplex_divide_def]) 1);
-qed "SComplex_divide";
-
-Goalw [SComplex_def] "x: SComplex ==> -x : SComplex";
-by (blast_tac (claset() addIs [hcomplex_of_complex_minus RS sym]) 1);
-qed "SComplex_minus";
-
-Goal "(-x : SComplex) = (x: SComplex)";
-by Auto_tac;
-by (etac SComplex_minus 2);
-by (dtac SComplex_minus 1);
-by Auto_tac;
-qed "SComplex_minus_iff";
-Addsimps [SComplex_minus_iff];
-
-Goal "[| x + y : SComplex; y: SComplex |] ==> x: SComplex";
-by (dres_inst_tac [("x","y")] SComplex_minus 1);
-by (dtac SComplex_add 1);
-by (assume_tac 1);
-by Auto_tac;
-qed "SComplex_add_cancel";
-
-Goalw [hcomplex_of_complex_def]
- "hcmod (hcomplex_of_complex r) : Reals";
-by (simp_tac (simpset() addsimps [hcmod,SReal_def,
- hypreal_of_real_def]) 1);
-qed "SReal_hcmod_hcomplex_of_complex";
-Addsimps [SReal_hcmod_hcomplex_of_complex];
-
-Goal "hcmod (number_of w ::hcomplex) : Reals";
-by (stac (hcomplex_number_of RS sym) 1);
-by (rtac SReal_hcmod_hcomplex_of_complex 1);
-qed "SReal_hcmod_number_of";
-Addsimps [SReal_hcmod_number_of];
-
-Goalw [SComplex_def] "x: SComplex ==> hcmod x : Reals";
-by Auto_tac;
-qed "SReal_hcmod_SComplex";
-
-Goalw [SComplex_def] "hcomplex_of_complex x: SComplex";
-by (Blast_tac 1);
-qed "SComplex_hcomplex_of_complex";
-Addsimps [SComplex_hcomplex_of_complex];
-
-Goal "(number_of w ::hcomplex) : SComplex";
-by (stac (hcomplex_number_of RS sym) 1);
-by (rtac SComplex_hcomplex_of_complex 1);
-qed "SComplex_number_of";
-Addsimps [SComplex_number_of];
-
-Goalw [hcomplex_divide_def] "r : SComplex ==> r/(number_of w::hcomplex) : SComplex";
-by (blast_tac (claset() addSIs [SComplex_number_of, SComplex_mult,
- SComplex_inverse]) 1);
-qed "SComplex_divide_number_of";
-
-Goalw [SComplex_def] "{x. hcomplex_of_complex x : SComplex} = (UNIV::complex set)";
-by Auto_tac;
-qed "SComplex_UNIV_complex";
-
-Goalw [SComplex_def] "(x: SComplex) = (EX y. x = hcomplex_of_complex y)";
-by Auto_tac;
-qed "SComplex_iff";
-
-Goalw [SComplex_def] "hcomplex_of_complex `(UNIV::complex set) = SComplex";
-by Auto_tac;
-qed "hcomplex_of_complex_image";
-
-Goalw [SComplex_def] "inv hcomplex_of_complex `SComplex = (UNIV::complex set)";
-by Auto_tac;
-by (rtac (inj_hcomplex_of_complex RS inv_f_f RS subst) 1);
-by (Blast_tac 1);
-qed "inv_hcomplex_of_complex_image";
-
-Goalw [SComplex_def]
- "[| EX x. x: P; P <= SComplex |] ==> EX Q. P = hcomplex_of_complex ` Q";
-by (Best_tac 1);
-qed "SComplex_hcomplex_of_complex_image";
-
-Goal "[| (x::hcomplex): SComplex; y: SComplex; hcmod x < hcmod y \
-\ |] ==> EX r: Reals. hcmod x< r & r < hcmod y";
-by (auto_tac (claset() addIs [SReal_dense], simpset()
- addsimps [SReal_hcmod_SComplex]));
-qed "SComplex_SReal_dense";
-
-Goalw [SComplex_def,SReal_def]
- "z : SComplex ==> hcmod z : Reals";
-by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
-by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
- hcomplex_of_complex_def,cmod_def]));
-by (res_inst_tac [("x","cmod r")] exI 1);
-by (ultra_tac (claset(),simpset() addsimps [cmod_def]) 1);
-qed "SComplex_hcmod_SReal";
-
-Goal "0 : SComplex";
-by (auto_tac ((claset(),simpset() addsimps [SComplex_def]) addIffs [hcomplex_of_complex_zero_iff]));
-qed "SComplex_zero";
-Addsimps [SComplex_zero];
-
-Goal "1 : SComplex";
-by (auto_tac (claset(),simpset() addsimps [SComplex_def,hcomplex_of_complex_def,
- hcomplex_one_def]));
-qed "SComplex_one";
-Addsimps [SComplex_one];
-
-(*
-Goalw [SComplex_def,SReal_def] "hcmod z : Reals ==> z : SComplex";
-by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
-by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def,
- hcomplex_of_complex_def,cmod_def]));
-*)
-
-(*--------------------------------------------------------------------------------------------*)
-(* Set of finite elements is a subring of the extended complex numbers *)
-(* -------------------------------------------------------------------------------------------*)
-
-Goalw [CFinite_def] "[|x : CFinite; y : CFinite|] ==> (x+y) : CFinite";
-by (blast_tac (claset() addSIs [SReal_add,hcmod_add_less]) 1);
-qed "CFinite_add";
-
-Goalw [CFinite_def] "[|x : CFinite; y : CFinite|] ==> x*y : CFinite";
-by (blast_tac (claset() addSIs [SReal_mult,hcmod_mult_less]) 1);
-qed "CFinite_mult";
-
-Goalw [CFinite_def] "(-x : CFinite) = (x : CFinite)";
-by (Simp_tac 1);
-qed "CFinite_minus_iff";
-Addsimps [CFinite_minus_iff];
-
-Goalw [SComplex_def,CFinite_def] "SComplex <= CFinite";
-by Auto_tac;
-by (res_inst_tac [("x","1 + hcmod(hcomplex_of_complex r)")] bexI 1);
-by (auto_tac (claset() addIs [SReal_add],simpset()));
-qed "SComplex_subset_CFinite";
-Addsimps [ SComplex_subset_CFinite];
-
-Goal "hcmod (hcomplex_of_complex r) : HFinite";
-by (auto_tac (claset() addSIs [ SReal_subset_HFinite RS subsetD],simpset()));
-qed "HFinite_hcmod_hcomplex_of_complex";
-Addsimps [HFinite_hcmod_hcomplex_of_complex];
-
-Goal "hcomplex_of_complex x: CFinite";
-by (auto_tac (claset() addSIs [ SComplex_subset_CFinite RS subsetD],simpset()));
-qed "CFinite_hcomplex_of_complex";
-Addsimps [CFinite_hcomplex_of_complex];
-
-Goalw [CFinite_def] "x : CFinite ==> EX t: Reals. hcmod x < t";
-by Auto_tac;
-qed "CFiniteD";
-
-Goalw [CFinite_def] "(x : CFinite) = (hcmod x : HFinite)";
-by (auto_tac (claset(), simpset() addsimps [HFinite_def]));
-qed "CFinite_hcmod_iff";
-
-Goal "number_of w : CFinite";
-by (rtac (SComplex_number_of RS (SComplex_subset_CFinite RS subsetD)) 1);
-qed "CFinite_number_of";
-Addsimps [CFinite_number_of];
-
-Goal "[|x : CFinite; y <= hcmod x; 0 <= y |] ==> y: HFinite";
-by (auto_tac (claset() addIs [HFinite_bounded],simpset() addsimps
- [CFinite_hcmod_iff]));
-qed "CFinite_bounded";
-
-(*--------------------------------------------------------------------------------------*)
-(* Set of complex infinitesimals is a subring of the nonstandard complex numbers *)
-(*--------------------------------------------------------------------------------------*)
-
-Goalw [CInfinitesimal_def]
- "x : CInfinitesimal ==> ALL r: Reals. 0 < r --> hcmod x < r";
-by Auto_tac;
-qed "CInfinitesimalD";
-
-Goalw [CInfinitesimal_def] "0 : CInfinitesimal";
-by Auto_tac;
-qed "CInfinitesimal_zero";
-AddIffs [CInfinitesimal_zero];
-
-Goal "x/(2::hcomplex) + x/(2::hcomplex) = x";
-by Auto_tac;
-qed "hcomplex_sum_of_halves";
-
-Goalw [CInfinitesimal_def,Infinitesimal_def]
- "(z : CInfinitesimal) = (hcmod z : Infinitesimal)";
-by Auto_tac;
-qed "CInfinitesimal_hcmod_iff";
-
-Goal "1 ~: CInfinitesimal";
-by (simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff]) 1);
-qed "one_not_CInfinitesimal";
-Addsimps [one_not_CInfinitesimal];
-
-Goal "[| x : CInfinitesimal; y : CInfinitesimal |] ==> (x+y) : CInfinitesimal";
-by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
-by (rtac hrabs_le_Infinitesimal 1);
-by (res_inst_tac [("y","hcmod y")] Infinitesimal_add 1);
-by Auto_tac;
-qed "CInfinitesimal_add";
-
-Goalw [CInfinitesimal_def] "(-x:CInfinitesimal) = (x:CInfinitesimal)";
-by (Full_simp_tac 1);
-qed "CInfinitesimal_minus_iff";
-Addsimps [CInfinitesimal_minus_iff];
-
-Goal "[| x : CInfinitesimal; y : CInfinitesimal |] ==> x-y : CInfinitesimal";
-by (asm_simp_tac
- (simpset() addsimps [hcomplex_diff_def, CInfinitesimal_add]) 1);
-qed "CInfinitesimal_diff";
-
-Goal "[| x : CInfinitesimal; y : CInfinitesimal |] ==> (x * y) : CInfinitesimal";
-by (auto_tac (claset() addIs [Infinitesimal_mult],simpset() addsimps
- [CInfinitesimal_hcmod_iff,hcmod_mult]));
-qed "CInfinitesimal_mult";
-
-Goal "[| x : CInfinitesimal; y : CFinite |] ==> (x * y) : CInfinitesimal";
-by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult],simpset()
- addsimps [CInfinitesimal_hcmod_iff,CFinite_hcmod_iff,hcmod_mult]));
-qed "CInfinitesimal_CFinite_mult";
-
-Goal "[| x : CInfinitesimal; y : CFinite |] ==> (y * x) : CInfinitesimal";
-by (auto_tac (claset() addDs [CInfinitesimal_CFinite_mult],
- simpset() addsimps [hcomplex_mult_commute]));
-qed "CInfinitesimal_CFinite_mult2";
-
-Goalw [CInfinite_def,HInfinite_def]
- "(z : CInfinite) = (hcmod z : HInfinite)";
-by Auto_tac;
-qed "CInfinite_hcmod_iff";
-
-Goal "x: CInfinite ==> inverse x: CInfinitesimal";
-by (auto_tac (claset() addIs [HInfinite_inverse_Infinitesimal],
- simpset() addsimps [CInfinitesimal_hcmod_iff,
- CInfinite_hcmod_iff,hcmod_hcomplex_inverse]));
-qed "CInfinite_inverse_CInfinitesimal";
-
-Goal "[|x: CInfinite; y: CInfinite|] ==> (x*y): CInfinite";
-by (auto_tac (claset() addIs [HInfinite_mult],simpset() addsimps
- [CInfinite_hcmod_iff,hcmod_mult]));
-qed "CInfinite_mult";
-
-Goalw [CInfinite_def] "(-x : CInfinite) = (x : CInfinite)";
-by (Simp_tac 1);
-qed "CInfinite_minus_iff";
-Addsimps [CInfinite_minus_iff];
-
-Goal "[|a: CFinite; b: CFinite; c: CFinite|] \
-\ ==> a*a + b*b + c*c : CFinite";
-by (auto_tac (claset() addIs [CFinite_mult,CFinite_add], simpset()));
-qed "CFinite_sum_squares";
-
-Goal "x ~: CInfinitesimal ==> x ~= 0";
-by Auto_tac;
-qed "not_CInfinitesimal_not_zero";
-
-Goal "x: CFinite - CInfinitesimal ==> x ~= 0";
-by Auto_tac;
-qed "not_CInfinitesimal_not_zero2";
-
-Goal "x : CFinite - CInfinitesimal ==> hcmod x : HFinite - Infinitesimal";
-by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,CInfinitesimal_hcmod_iff]));
-qed "CFinite_diff_CInfinitesimal_hcmod";
-
-Goal "[| e : CInfinitesimal; hcmod x < hcmod e |] ==> x : CInfinitesimal";
-by (auto_tac (claset() addIs [hrabs_less_Infinitesimal],simpset()
- addsimps [CInfinitesimal_hcmod_iff]));
-qed "hcmod_less_CInfinitesimal";
-
-Goal "[| e : CInfinitesimal; hcmod x <= hcmod e |] ==> x : CInfinitesimal";
-by (auto_tac (claset() addIs [hrabs_le_Infinitesimal],simpset()
- addsimps [CInfinitesimal_hcmod_iff]));
-qed "hcmod_le_CInfinitesimal";
-
-Goal "[| e : CInfinitesimal; \
-\ e' : CInfinitesimal; \
-\ hcmod e' < hcmod x ; hcmod x < hcmod e \
-\ |] ==> x : CInfinitesimal";
-by (auto_tac (claset() addIs [Infinitesimal_interval],simpset()
- addsimps [CInfinitesimal_hcmod_iff]));
-qed "CInfinitesimal_interval";
-
-Goal "[| e : CInfinitesimal; \
-\ e' : CInfinitesimal; \
-\ hcmod e' <= hcmod x ; hcmod x <= hcmod e \
-\ |] ==> x : CInfinitesimal";
-by (auto_tac (claset() addIs [Infinitesimal_interval2],simpset()
- addsimps [CInfinitesimal_hcmod_iff]));
-qed "CInfinitesimal_interval2";
-
-Goal "[| x ~: CInfinitesimal; y ~: CInfinitesimal|] ==> (x*y) ~: CInfinitesimal";
-by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
-by (dtac not_Infinitesimal_mult 1);
-by Auto_tac;
-qed "not_CInfinitesimal_mult";
-
-Goal "x*y : CInfinitesimal ==> x : CInfinitesimal | y : CInfinitesimal";
-by (auto_tac (claset() addDs [Infinitesimal_mult_disj],simpset() addsimps
- [CInfinitesimal_hcmod_iff,hcmod_mult]));
-qed "CInfinitesimal_mult_disj";
-
-Goal "[| x : CFinite - CInfinitesimal; \
-\ y : CFinite - CInfinitesimal \
-\ |] ==> (x*y) : CFinite - CInfinitesimal";
-by (Clarify_tac 1);
-by (blast_tac (claset() addDs [CFinite_mult,not_CInfinitesimal_mult]) 1);
-qed "CFinite_CInfinitesimal_diff_mult";
-
-Goal "CInfinitesimal <= CFinite";
-by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
- simpset() addsimps [CInfinitesimal_hcmod_iff,CFinite_hcmod_iff]));
-qed "CInfinitesimal_subset_CFinite";
-
-Goal "x: CInfinitesimal ==> x * hcomplex_of_complex r : CInfinitesimal";
-by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult],
- simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
-qed "CInfinitesimal_hcomplex_of_complex_mult";
-
-Goal "x: CInfinitesimal ==> hcomplex_of_complex r * x: CInfinitesimal";
-by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
- simpset() addsimps [CInfinitesimal_hcmod_iff,hcmod_mult]));
-qed "CInfinitesimal_hcomplex_of_complex_mult2";
-
-
-(*--------------------------------------------------------------------------------------*)
-(* Infinitely close relation @c= *)
-(* -------------------------------------------------------------------------------------*)
-
-(*
-Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)";
-by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
-*)
-
-Goal "x:CInfinitesimal = (x @c= 0)";
-by (simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff,
- capprox_def]) 1);
-qed "mem_cinfmal_iff";
-
-Goalw [capprox_def,hcomplex_diff_def]
- " (x @c= y) = (x + -y @c= 0)";
-by (Simp_tac 1);
-qed "capprox_minus_iff";
-
-Goalw [capprox_def,hcomplex_diff_def]
- " (x @c= y) = (-y + x @c= 0)";
-by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
-qed "capprox_minus_iff2";
-
-Goalw [capprox_def] "x @c= x";
-by (Simp_tac 1);
-qed "capprox_refl";
-Addsimps [capprox_refl];
-
-Goalw [capprox_def,CInfinitesimal_def]
- "x @c= y ==> y @c= x";
-by (auto_tac (claset() addSDs [bspec],simpset() addsimps
- [hcmod_diff_commute]));
-qed "capprox_sym";
-
-Goalw [capprox_def] "[| x @c= y; y @c= z |] ==> x @c= z";
-by (dtac CInfinitesimal_add 1);
-by (assume_tac 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]));
-qed "capprox_trans";
-
-Goal "[| r @c= x; s @c= x |] ==> r @c= s";
-by (blast_tac (claset() addIs [capprox_sym, capprox_trans]) 1);
-qed "capprox_trans2";
-
-Goal "[| x @c= r; x @c= s|] ==> r @c= s";
-by (blast_tac (claset() addIs [capprox_sym, capprox_trans]) 1);
-qed "capprox_trans3";
-
-Goal "(number_of w @c= x) = (x @c= number_of w)";
-by (blast_tac (claset() addIs [capprox_sym]) 1);
-qed "number_of_capprox_reorient";
-Addsimps [number_of_capprox_reorient];
-
-Goal "(x-y : CInfinitesimal) = (x @c= y)";
-by (auto_tac (claset(),
- simpset() addsimps [hcomplex_diff_def, capprox_minus_iff RS sym,
- mem_cinfmal_iff]));
-qed "CInfinitesimal_capprox_minus";
-
-Goalw [cmonad_def] "(x @c= y) = (cmonad(x)=cmonad(y))";
-by (auto_tac (claset() addDs [capprox_sym]
- addSEs [capprox_trans,equalityCE],
- simpset()));
-qed "capprox_monad_iff";
-
-Goal "[| x: CInfinitesimal; y: CInfinitesimal |] ==> x @c= y";
-by (asm_full_simp_tac (simpset() addsimps [mem_cinfmal_iff]) 1);
-by (blast_tac (claset() addIs [capprox_trans, capprox_sym]) 1);
-qed "Infinitesimal_capprox";
-
-val prem1::prem2::rest =
-goalw thy [capprox_def,hcomplex_diff_def]
- "[| a @c= b; c @c= d |] ==> a+c @c= b+d";
-by (rtac (minus_add_distrib RS ssubst) 1);
-by (rtac (hcomplex_add_assoc RS ssubst) 1);
-by (res_inst_tac [("b1","c")] (add_left_commute RS subst) 1);
-by (rtac (hcomplex_add_assoc RS subst) 1);
-by (rtac ([prem1,prem2] MRS CInfinitesimal_add) 1);
-qed "capprox_add";
-
-Goal "a @c= b ==> -a @c= -b";
-by (rtac ((capprox_minus_iff RS iffD2) RS capprox_sym) 1);
-by (dtac (capprox_minus_iff RS iffD1) 1);
-by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
-qed "capprox_minus";
-
-Goal "-a @c= -b ==> a @c= b";
-by (auto_tac (claset() addDs [capprox_minus], simpset()));
-qed "capprox_minus2";
-
-Goal "(-a @c= -b) = (a @c= b)";
-by (blast_tac (claset() addIs [capprox_minus,capprox_minus2]) 1);
-qed "capprox_minus_cancel";
-Addsimps [capprox_minus_cancel];
-
-Goal "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d";
-by (blast_tac (claset() addSIs [capprox_add,capprox_minus]) 1);
-qed "capprox_add_minus";
-
-Goalw [capprox_def,hcomplex_diff_def]
- "[| a @c= b; c: CFinite|] ==> a*c @c= b*c";
-by (asm_full_simp_tac (HOL_ss addsimps [CInfinitesimal_CFinite_mult,
- minus_mult_left,hcomplex_add_mult_distrib RS sym]) 1);
-qed "capprox_mult1";
-
-Goal "[|a @c= b; c: CFinite|] ==> c*a @c= c*b";
-by (asm_simp_tac (simpset() addsimps [capprox_mult1,hcomplex_mult_commute]) 1);
-qed "capprox_mult2";
-
-Goal "[|u @c= v*x; x @c= y; v: CFinite|] ==> u @c= v*y";
-by (fast_tac (claset() addIs [capprox_mult2,capprox_trans]) 1);
-qed "capprox_mult_subst";
-
-Goal "[| u @c= x*v; x @c= y; v: CFinite |] ==> u @c= y*v";
-by (fast_tac (claset() addIs [capprox_mult1,capprox_trans]) 1);
-qed "capprox_mult_subst2";
-
-Goal "[| u @c= x*hcomplex_of_complex v; x @c= y |] ==> u @c= y*hcomplex_of_complex v";
-by (auto_tac (claset() addIs [capprox_mult_subst2], simpset()));
-qed "capprox_mult_subst_SComplex";
-
-Goalw [capprox_def] "a = b ==> a @c= b";
-by (Asm_simp_tac 1);
-qed "capprox_eq_imp";
-
-Goal "x: CInfinitesimal ==> -x @c= x";
-by (fast_tac (HOL_cs addIs [CInfinitesimal_minus_iff RS iffD2,
- mem_cinfmal_iff RS iffD1,capprox_trans2]) 1);
-qed "CInfinitesimal_minus_capprox";
-
-Goalw [capprox_def]
- "(EX y: CInfinitesimal. x - z = y) = (x @c= z)";
-by (Blast_tac 1);
-qed "bex_CInfinitesimal_iff";
-
-Goal "(EX y: CInfinitesimal. x = z + y) = (x @c= z)";
-by (asm_full_simp_tac (simpset() addsimps [bex_CInfinitesimal_iff RS sym]) 1);
-by (Force_tac 1);
-qed "bex_CInfinitesimal_iff2";
-
-Goal "[| y: CInfinitesimal; x + y = z |] ==> x @c= z";
-by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
-by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
-qed "CInfinitesimal_add_capprox";
-
-Goal "y: CInfinitesimal ==> x @c= x + y";
-by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
-by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
-qed "CInfinitesimal_add_capprox_self";
-
-Goal "y: CInfinitesimal ==> x @c= y + x";
-by (auto_tac (claset() addDs [CInfinitesimal_add_capprox_self],
- simpset() addsimps [hcomplex_add_commute]));
-qed "CInfinitesimal_add_capprox_self2";
-
-Goal "y: CInfinitesimal ==> x @c= x + -y";
-by (blast_tac (claset() addSIs [CInfinitesimal_add_capprox_self,
- CInfinitesimal_minus_iff RS iffD2]) 1);
-qed "CInfinitesimal_add_minus_capprox_self";
-
-Goal "[| y: CInfinitesimal; x+y @c= z|] ==> x @c= z";
-by (dres_inst_tac [("x","x")] (CInfinitesimal_add_capprox_self RS capprox_sym) 1);
-by (etac (capprox_trans3 RS capprox_sym) 1);
-by (assume_tac 1);
-qed "CInfinitesimal_add_cancel";
-
-Goal "[| y: CInfinitesimal; x @c= z + y|] ==> x @c= z";
-by (dres_inst_tac [("x","z")] (CInfinitesimal_add_capprox_self2 RS capprox_sym) 1);
-by (etac (capprox_trans3 RS capprox_sym) 1);
-by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
-by (etac capprox_sym 1);
-qed "CInfinitesimal_add_right_cancel";
-
-Goal "d + b @c= d + c ==> b @c= c";
-by (dtac (capprox_minus_iff RS iffD1) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [minus_add_distrib,capprox_minus_iff RS sym]
- @ add_ac) 1);
-qed "capprox_add_left_cancel";
-
-Goal "b + d @c= c + d ==> b @c= c";
-by (rtac capprox_add_left_cancel 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hcomplex_add_commute]) 1);
-qed "capprox_add_right_cancel";
-
-Goal "b @c= c ==> d + b @c= d + c";
-by (rtac (capprox_minus_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [capprox_minus_iff RS sym] @ add_ac) 1);
-qed "capprox_add_mono1";
-
-Goal "b @c= c ==> b + a @c= c + a";
-by (asm_simp_tac (simpset() addsimps
- [hcomplex_add_commute,capprox_add_mono1]) 1);
-qed "capprox_add_mono2";
-
-Goal "(a + b @c= a + c) = (b @c= c)";
-by (fast_tac (claset() addEs [capprox_add_left_cancel,
- capprox_add_mono1]) 1);
-qed "capprox_add_left_iff";
-
-AddIffs [capprox_add_left_iff];
-
-
-Goal "(b + a @c= c + a) = (b @c= c)";
-by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1);
-qed "capprox_add_right_iff";
-
-AddIffs [capprox_add_right_iff];
-
-Goal "[| x: CFinite; x @c= y |] ==> y: CFinite";
-by (dtac (bex_CInfinitesimal_iff2 RS iffD2) 1);
-by (Step_tac 1);
-by (dtac (CInfinitesimal_subset_CFinite RS subsetD
- RS (CFinite_minus_iff RS iffD2)) 1);
-by (dtac CFinite_add 1);
-by (assume_tac 1 THEN Auto_tac);
-qed "capprox_CFinite";
-
-Goal "x @c= hcomplex_of_complex D ==> x: CFinite";
-by (rtac (capprox_sym RSN (2,capprox_CFinite)) 1);
-by Auto_tac;
-qed "capprox_hcomplex_of_complex_CFinite";
-
-Goal "[|a @c= b; c @c= d; b: CFinite; d: CFinite|] ==> a*c @c= b*d";
-by (rtac capprox_trans 1);
-by (rtac capprox_mult2 2);
-by (rtac capprox_mult1 1);
-by (blast_tac (claset() addIs [capprox_CFinite, capprox_sym]) 2);
-by Auto_tac;
-qed "capprox_mult_CFinite";
-
-Goal "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |] \
-\ ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d";
-by (blast_tac (claset() addSIs [capprox_mult_CFinite,
- capprox_hcomplex_of_complex_CFinite,CFinite_hcomplex_of_complex]) 1);
-qed "capprox_mult_hcomplex_of_complex";
-
-Goal "[| a: SComplex; a ~= 0; a*x @c= 0 |] ==> x @c= 0";
-by (dtac (SComplex_inverse RS (SComplex_subset_CFinite RS subsetD)) 1);
-by (auto_tac (claset() addDs [capprox_mult2],
- simpset() addsimps [hcomplex_mult_assoc RS sym]));
-qed "capprox_SComplex_mult_cancel_zero";
-
-Goal "[| a: SComplex; x @c= 0 |] ==> x*a @c= 0";
-by (auto_tac (claset() addDs [(SComplex_subset_CFinite RS subsetD),
- capprox_mult1], simpset()));
-qed "capprox_mult_SComplex1";
-
-Goal "[| a: SComplex; x @c= 0 |] ==> a*x @c= 0";
-by (auto_tac (claset() addDs [(SComplex_subset_CFinite RS subsetD),
- capprox_mult2], simpset()));
-qed "capprox_mult_SComplex2";
-
-Goal "[|a : SComplex; a ~= 0 |] ==> (a*x @c= 0) = (x @c= 0)";
-by (blast_tac (claset() addIs [capprox_SComplex_mult_cancel_zero,
- capprox_mult_SComplex2]) 1);
-qed "capprox_mult_SComplex_zero_cancel_iff";
-Addsimps [capprox_mult_SComplex_zero_cancel_iff];
-
-Goal "[| a: SComplex; a ~= 0; a* w @c= a*z |] ==> w @c= z";
-by (dtac (SComplex_inverse RS (SComplex_subset_CFinite RS subsetD)) 1);
-by (auto_tac (claset() addDs [capprox_mult2],
- simpset() addsimps [hcomplex_mult_assoc RS sym]));
-qed "capprox_SComplex_mult_cancel";
-
-Goal "[| a: SComplex; a ~= 0|] ==> (a* w @c= a*z) = (w @c= z)";
-by (auto_tac (claset() addSIs [capprox_mult2,SComplex_subset_CFinite RS subsetD]
- addIs [capprox_SComplex_mult_cancel], simpset()));
-qed "capprox_SComplex_mult_cancel_iff1";
-Addsimps [capprox_SComplex_mult_cancel_iff1];
-
-Goal "(x @c= y) = (hcmod (y - x) @= 0)";
-by (rtac (capprox_minus_iff RS ssubst) 1);
-by (auto_tac (claset(),simpset() addsimps [capprox_def,
- CInfinitesimal_hcmod_iff,mem_infmal_iff,symmetric hcomplex_diff_def,
- hcmod_diff_commute]));
-qed "capprox_hcmod_approx_zero";
-
-Goal "(x @c= 0) = (hcmod x @= 0)";
-by (auto_tac (claset(),simpset() addsimps
- [capprox_hcmod_approx_zero]));
-qed "capprox_approx_zero_iff";
-
-Goal "(-x @c= 0) = (x @c= 0)";
-by (auto_tac (claset(),simpset() addsimps
- [capprox_hcmod_approx_zero]));
-qed "capprox_minus_zero_cancel_iff";
-Addsimps [capprox_minus_zero_cancel_iff];
-
-Goal "u @c= 0 ==> hcmod(x + u) - hcmod x : Infinitesimal";
-by (res_inst_tac [("e","hcmod u"),("e'","- hcmod u")] Infinitesimal_interval2 1);
-by (auto_tac (claset() addDs [capprox_approx_zero_iff RS iffD1],
- simpset() addsimps [mem_infmal_iff RS sym,hypreal_diff_def]));
-by (res_inst_tac [("c1","hcmod x")] (add_le_cancel_left RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [symmetric hypreal_diff_def]));
-qed "Infinitesimal_hcmod_add_diff";
-
-Goal "u @c= 0 ==> hcmod(x + u) @= hcmod x";
-by (rtac (approx_minus_iff RS iffD2) 1);
-by (auto_tac (claset() addIs [Infinitesimal_hcmod_add_diff],
- simpset() addsimps [mem_infmal_iff RS sym,symmetric hypreal_diff_def]));
-qed "approx_hcmod_add_hcmod";
-
-Goal "x @c= y ==> hcmod x @= hcmod y";
-by (auto_tac (claset() addIs [approx_hcmod_add_hcmod]
- addSDs [bex_CInfinitesimal_iff2 RS iffD2],simpset() addsimps [mem_cinfmal_iff]));
-qed "capprox_hcmod_approx";
-
-(*--------------------------------------------------------------------------------------*)
-(* zero is the only complex number that is also infinitesimal *)
-(*--------------------------------------------------------------------------------------*)
-
-Goal "[| x: SComplex; y: CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x";
-by (auto_tac (claset() addSIs [Infinitesimal_less_SReal,SComplex_hcmod_SReal],
- simpset() addsimps [CInfinitesimal_hcmod_iff]));
-qed "CInfinitesimal_less_SComplex";
-
-Goal "y: CInfinitesimal ==> ALL r: SComplex. 0 < hcmod r --> hcmod y < hcmod r";
-by (blast_tac (claset() addIs [CInfinitesimal_less_SComplex]) 1);
-qed "CInfinitesimal_less_SComplex2";
-
-Goal "SComplex Int CInfinitesimal = {0}";
-by (auto_tac (claset(),simpset() addsimps [SComplex_def,CInfinitesimal_hcmod_iff]));
-by (cut_inst_tac [("r","r")] SReal_hcmod_hcomplex_of_complex 1);
-by (dres_inst_tac [("A","Reals")] IntI 1 THEN assume_tac 1);
-by (subgoal_tac "hcmod (hcomplex_of_complex r) = 0" 1);
-by (Asm_full_simp_tac 1);
-by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
-by (rotate_tac 2 1);
-by (Asm_full_simp_tac 1);
-qed "SComplex_Int_CInfinitesimal_zero";
-
-Goal "[| x: SComplex; x: CInfinitesimal|] ==> x = 0";
-by (cut_facts_tac [SComplex_Int_CInfinitesimal_zero] 1);
-by (Blast_tac 1);
-qed "SComplex_CInfinitesimal_zero";
-
-Goal "[| x : SComplex; x ~= 0 |] ==> x : CFinite - CInfinitesimal";
-by (auto_tac (claset() addDs [SComplex_CInfinitesimal_zero,
- SComplex_subset_CFinite RS subsetD],
- simpset()));
-qed "SComplex_CFinite_diff_CInfinitesimal";
-
-Goal "hcomplex_of_complex x ~= 0 ==> hcomplex_of_complex x : CFinite - CInfinitesimal";
-by (rtac SComplex_CFinite_diff_CInfinitesimal 1);
-by Auto_tac;
-qed "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
-
-Goal "(hcomplex_of_complex x : CInfinitesimal) = (x=0)";
-by (auto_tac (claset(), simpset() addsimps [hcomplex_of_complex_zero]));
-by (rtac ccontr 1);
-by (rtac (hcomplex_of_complex_CFinite_diff_CInfinitesimal RS DiffD2) 1);
-by Auto_tac;
-qed "hcomplex_of_complex_CInfinitesimal_iff_0";
-AddIffs [hcomplex_of_complex_CInfinitesimal_iff_0];
-
-Goal "number_of w ~= (0::hcomplex) ==> number_of w ~: CInfinitesimal";
-by (fast_tac (claset() addDs [SComplex_number_of RS SComplex_CInfinitesimal_zero]) 1);
-qed "number_of_not_CInfinitesimal";
-Addsimps [number_of_not_CInfinitesimal];
-
-Goal "[| y: SComplex; x @c= y; y~= 0 |] ==> x ~= 0";
-by (auto_tac (claset() addDs [SComplex_CInfinitesimal_zero,
- capprox_sym RS (mem_cinfmal_iff RS iffD2)],simpset()));
-qed "capprox_SComplex_not_zero";
-
-Goal "[| x @c= y; y : CFinite - CInfinitesimal |] \
-\ ==> x : CFinite - CInfinitesimal";
-by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)],
- simpset() addsimps [mem_cinfmal_iff]));
-by (dtac capprox_trans3 1 THEN assume_tac 1);
-by (blast_tac (claset() addDs [capprox_sym]) 1);
-qed "CFinite_diff_CInfinitesimal_capprox";
-
-Goal "[| y ~= 0; y: CInfinitesimal; x/y : CFinite |] ==> x : CInfinitesimal";
-by (dtac CInfinitesimal_CFinite_mult2 1);
-by (assume_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 1);
-qed "CInfinitesimal_ratio";
-
-Goal "[|x: SComplex; y: SComplex|] ==> (x @c= y) = (x = y)";
-by Auto_tac;
-by (rewrite_goals_tac [capprox_def]);
-by (dres_inst_tac [("x","y")] SComplex_minus 1);
-by (dtac SComplex_add 1 THEN assume_tac 1);
-by (rtac (CLAIM "x - y = 0 ==> x = (y::hcomplex)") 1);
-by (rtac SComplex_CInfinitesimal_zero 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def]));
-qed "SComplex_capprox_iff";
-
-Goal "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))";
-by (rtac SComplex_capprox_iff 1);
-by Auto_tac;
-qed "number_of_capprox_iff";
-Addsimps [number_of_capprox_iff];
-
-Goal "(number_of w : CInfinitesimal) = (number_of w = (0::hcomplex))";
-by (rtac iffI 1);
-by (fast_tac (claset() addDs [SComplex_number_of RS SComplex_CInfinitesimal_zero]) 1);
-by (Asm_simp_tac 1);
-qed "number_of_CInfinitesimal_iff";
-Addsimps [number_of_CInfinitesimal_iff];
-
-Goal "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)";
-by Auto_tac;
-by (rtac (inj_hcomplex_of_complex RS injD) 1);
-by (rtac (SComplex_capprox_iff RS iffD1) 1);
-by Auto_tac;
-qed "hcomplex_of_complex_approx_iff";
-Addsimps [hcomplex_of_complex_approx_iff];
-
-Goal "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)";
-by (stac (hcomplex_of_complex_approx_iff RS sym) 1);
-by Auto_tac;
-qed "hcomplex_of_complex_capprox_number_of_iff";
-Addsimps [hcomplex_of_complex_capprox_number_of_iff];
-
-Goal "[| r: SComplex; s: SComplex; r @c= x; s @c= x|] ==> r = s";
-by (blast_tac (claset() addIs [(SComplex_capprox_iff RS iffD1),
- capprox_trans2]) 1);
-qed "capprox_unique_complex";
-
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) \
-\ ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @= \
-\ Abs_hypreal(hyprel `` {%n. Re(Y n)})";
-by (auto_tac (claset(),simpset() addsimps [approx_FreeUltrafilterNat_iff]));
-by (dtac (capprox_minus_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_minus,hcomplex_add,
- mem_cinfmal_iff RS sym,CInfinitesimal_hcmod_iff,hcmod,
- Infinitesimal_FreeUltrafilterNat_iff2]));
-by (dres_inst_tac [("x","m")] spec 1);
-by (Ultra_tac 1);
-by (rename_tac "Z x" 1);
-by (case_tac "X x" 1);
-by (case_tac "Y x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
- complex_mod] delsimps [realpow_Suc]));
-by (rtac order_le_less_trans 1 THEN assume_tac 2);
-by (dres_inst_tac [("t","Z x")] sym 1);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
-qed "hcomplex_capproxD1";
-
-(* same proof *)
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) \
-\ ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @= \
-\ Abs_hypreal(hyprel `` {%n. Im(Y n)})";
-by (auto_tac (claset(),simpset() addsimps [approx_FreeUltrafilterNat_iff]));
-by (dtac (capprox_minus_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_minus,hcomplex_add,
- mem_cinfmal_iff RS sym,CInfinitesimal_hcmod_iff,hcmod,
- Infinitesimal_FreeUltrafilterNat_iff2]));
-by (dres_inst_tac [("x","m")] spec 1);
-by (Ultra_tac 1);
-by (rename_tac "Z x" 1);
-by (case_tac "X x" 1);
-by (case_tac "Y x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
- complex_mod] delsimps [realpow_Suc]));
-by (rtac order_le_less_trans 1 THEN assume_tac 2);
-by (dres_inst_tac [("t","Z x")] sym 1);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
-qed "hcomplex_capproxD2";
-
-Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @= \
-\ Abs_hypreal(hyprel `` {%n. Re(Y n)}); \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) @= \
-\ Abs_hypreal(hyprel `` {%n. Im(Y n)}) \
-\ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})";
-by (dtac (approx_minus_iff RS iffD1) 1);
-by (dtac (approx_minus_iff RS iffD1) 1);
-by (rtac (capprox_minus_iff RS iffD2) 1);
-by (auto_tac (claset(),
- simpset() addsimps [mem_cinfmal_iff RS sym,
- mem_infmal_iff RS sym,hypreal_minus,hypreal_add,hcomplex_minus,
- hcomplex_add,CInfinitesimal_hcmod_iff,hcmod,
- Infinitesimal_FreeUltrafilterNat_iff]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by Auto_tac;
-by (dres_inst_tac [("x","u/2")] spec 1);
-by (dres_inst_tac [("x","u/2")] spec 1);
-by Safe_tac;
-by (TRYALL(Force_tac));
-by (ultra_tac (claset(),HOL_ss) 1);
-by (dtac sym 1 THEN dtac sym 1);
-by (case_tac "X x" 1);
-by (case_tac "Y x" 1);
-by (auto_tac (claset(),
- HOL_ss addsimps [complex_minus,complex_add,
- complex_mod, snd_conv, fst_conv,numeral_2_eq_2]));
-by (rename_tac "a b c d" 1);
-by (subgoal_tac "sqrt (abs(a + - c) ^ 2 + abs(b + - d) ^ 2) < u" 1);
-by (rtac lemma_sqrt_hcomplex_capprox 2);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1);
-qed "hcomplex_capproxI";
-
-Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) =\
-\ (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) & \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))";
-by (blast_tac (claset() addIs [hcomplex_capproxI,hcomplex_capproxD1,hcomplex_capproxD2]) 1);
-qed "capprox_approx_iff";
-
-Goal "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
- capprox_approx_iff]));
-qed "hcomplex_of_hypreal_capprox_iff";
-Addsimps [hcomplex_of_hypreal_capprox_iff];
-
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite \
-\ ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite";
-by (auto_tac (claset(),
- simpset() addsimps [CFinite_hcmod_iff,hcmod,HFinite_FreeUltrafilterNat_iff]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
-by (Ultra_tac 1);
-by (dtac sym 1 THEN case_tac "X x" 1);
-by (auto_tac (claset(),
- simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
-by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
-by (dtac order_less_le_trans 1 THEN assume_tac 1);
-by (dtac (real_sqrt_ge_abs1 RSN (2,order_less_le_trans)) 1);
-by (auto_tac ((claset(),simpset() addsimps [numeral_2_eq_2 RS sym]) addIffs [order_less_irrefl]));
-qed "CFinite_HFinite_Re";
-
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite \
-\ ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite";
-by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
- hcmod,HFinite_FreeUltrafilterNat_iff]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by (res_inst_tac [("x","u")] exI 1 THEN Auto_tac);
-by (Ultra_tac 1);
-by (dtac sym 1 THEN case_tac "X x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_mod] delsimps [realpow_Suc]));
-by (rtac ccontr 1 THEN dtac (linorder_not_less RS iffD1) 1);
-by (dtac order_less_le_trans 1 THEN assume_tac 1);
-by (dtac (real_sqrt_ge_abs2 RSN (2,order_less_le_trans)) 1);
-by (auto_tac (clasimpset() addIffs [order_less_irrefl]));
-qed "CFinite_HFinite_Im";
-
-Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite; \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite \
-\ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite";
-by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
- hcmod,HFinite_FreeUltrafilterNat_iff]));
-by (rename_tac "Y Z u v" 1);
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by (res_inst_tac [("x","2*(u + v)")] exI 1);
-by (Ultra_tac 1);
-by (dtac sym 1 THEN case_tac "X x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_mod,numeral_2_eq_2] delsimps [realpow_Suc]));
-by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
-by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
-by (subgoal_tac "sqrt (abs(Y x) ^ 2 + abs(Z x) ^ 2) < 2*u + 2*v" 1);
-by (rtac lemma_sqrt_hcomplex_capprox 2);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [power2_eq_square]) 1);
-qed "HFinite_Re_Im_CFinite";
-
-Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite) = \
-\ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : HFinite & \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : HFinite)";
-by (blast_tac (claset() addIs [HFinite_Re_Im_CFinite,CFinite_HFinite_Im,
- CFinite_HFinite_Re]) 1);
-qed "CFinite_HFinite_iff";
-
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex \
-\ ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals";
-by (auto_tac (claset(),simpset() addsimps [SComplex_def,
- hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
-by (res_inst_tac [("x","Re r")] exI 1);
-by (Ultra_tac 1);
-qed "SComplex_Re_SReal";
-
-Goal "Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex \
-\ ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals";
-by (auto_tac (claset(),simpset() addsimps [SComplex_def,
- hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
-by (res_inst_tac [("x","Im r")] exI 1);
-by (Ultra_tac 1);
-qed "SComplex_Im_SReal";
-
-Goal "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals; \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals \
-\ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex";
-by (auto_tac (claset(),simpset() addsimps [SComplex_def,
- hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
-by (res_inst_tac [("x","Complex r ra")] exI 1);
-by (Ultra_tac 1);
-qed "Reals_Re_Im_SComplex";
-
-Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \
-\ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Reals & \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Reals)";
-by (blast_tac (claset() addIs [SComplex_Re_SReal,SComplex_Im_SReal,
- Reals_Re_Im_SComplex]) 1);
-qed "SComplex_SReal_iff";
-
-val hcomplex_zero_num = thm"hcomplex_zero_num";
-
-Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CInfinitesimal) = \
-\ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : Infinitesimal & \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : Infinitesimal)";
-by (auto_tac (claset(),simpset() addsimps [mem_cinfmal_iff,
- mem_infmal_iff,hcomplex_zero_num,hypreal_zero_num,capprox_approx_iff]));
-qed "CInfinitesimal_Infinitesimal_iff";
-
-(*** more lemmas ****)
-Goal "(EX t. P t) = (EX X. P (Abs_hcomplex(hcomplexrel `` {X})))";
-by Auto_tac;
-by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1);
-by Auto_tac;
-qed "eq_Abs_hcomplex_EX";
-
-Goal "(EX t : A. P t) = (EX X. (Abs_hcomplex(hcomplexrel `` {X})) : A & \
-\ P (Abs_hcomplex(hcomplexrel `` {X})))";
-by Auto_tac;
-by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1);
-by Auto_tac;
-qed "eq_Abs_hcomplex_Bex";
-
-(* Here we go - easy proof now!! *)
-Goal "x:CFinite ==> EX t: SComplex. x @c= t";
-by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
-by (auto_tac (claset(),simpset() addsimps [CFinite_HFinite_iff,
- eq_Abs_hcomplex_Bex,SComplex_SReal_iff,capprox_approx_iff]));
-by (REPEAT(dtac st_part_Ex 1 THEN Step_tac 1));
-by (res_inst_tac [("z","t")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1);
-by Auto_tac;
-by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1);
-by Auto_tac;
-qed "stc_part_Ex";
-
-Goal "x:CFinite ==> EX! t. t : SComplex & x @c= t";
-by (dtac stc_part_Ex 1 THEN Step_tac 1);
-by (dtac capprox_sym 2 THEN dtac capprox_sym 2
- THEN dtac capprox_sym 2);
-by (auto_tac (claset() addSIs [capprox_unique_complex], simpset()));
-qed "stc_part_Ex1";
-
-Goalw [CFinite_def,CInfinite_def] "CFinite Int CInfinite = {}";
-by Auto_tac;
-qed "CFinite_Int_CInfinite_empty";
-Addsimps [CFinite_Int_CInfinite_empty];
-
-Goal "x: CFinite ==> x ~: CInfinite";
-by (EVERY1[Step_tac, dtac IntI, assume_tac]);
-by Auto_tac;
-qed "CFinite_not_CInfinite";
-
-Goal "x~: CFinite ==> x: CInfinite";
-by (auto_tac (claset() addIs [not_HFinite_HInfinite],
- simpset() addsimps [CFinite_hcmod_iff,CInfinite_hcmod_iff]));
-qed "not_CFinite_CInfinite";
-
-Goal "x : CInfinite | x : CFinite";
-by (blast_tac (claset() addIs [not_CFinite_CInfinite]) 1);
-qed "CInfinite_CFinite_disj";
-
-Goal "(x : CInfinite) = (x ~: CFinite)";
-by (blast_tac (claset() addDs [CFinite_not_CInfinite,
- not_CFinite_CInfinite]) 1);
-qed "CInfinite_CFinite_iff";
-
-Goal "(x : CFinite) = (x ~: CInfinite)";
-by (simp_tac (simpset() addsimps [CInfinite_CFinite_iff]) 1);
-qed "CFinite_CInfinite_iff";
-
-Goal "x ~: CInfinitesimal ==> x : CInfinite | x : CFinite - CInfinitesimal";
-by (fast_tac (claset() addIs [not_CFinite_CInfinite]) 1);
-qed "CInfinite_diff_CFinite_CInfinitesimal_disj";
-
-Goal "[| x : CFinite; x ~: CInfinitesimal |] ==> inverse x : CFinite";
-by (cut_inst_tac [("x","inverse x")] CInfinite_CFinite_disj 1);
-by (auto_tac (claset() addSDs [CInfinite_inverse_CInfinitesimal], simpset()));
-qed "CFinite_inverse";
-
-Goal "x : CFinite - CInfinitesimal ==> inverse x : CFinite";
-by (blast_tac (claset() addIs [CFinite_inverse]) 1);
-qed "CFinite_inverse2";
-
-Goal "x ~: CInfinitesimal ==> inverse(x) : CFinite";
-by (dtac CInfinite_diff_CFinite_CInfinitesimal_disj 1);
-by (blast_tac (claset() addIs [CFinite_inverse,
- CInfinite_inverse_CInfinitesimal,
- CInfinitesimal_subset_CFinite RS subsetD]) 1);
-qed "CInfinitesimal_inverse_CFinite";
-
-
-Goal "x : CFinite - CInfinitesimal ==> inverse x : CFinite - CInfinitesimal";
-by (auto_tac (claset() addIs [CInfinitesimal_inverse_CFinite], simpset()));
-by (dtac CInfinitesimal_CFinite_mult2 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [not_CInfinitesimal_not_zero]) 1);
-qed "CFinite_not_CInfinitesimal_inverse";
-
-Goal "[| x @c= y; y : CFinite - CInfinitesimal |] \
-\ ==> inverse x @c= inverse y";
-by (forward_tac [CFinite_diff_CInfinitesimal_capprox] 1);
-by (assume_tac 1);
-by (forward_tac [not_CInfinitesimal_not_zero2] 1);
-by (forw_inst_tac [("x","x")] not_CInfinitesimal_not_zero2 1);
-by (REPEAT(dtac CFinite_inverse2 1));
-by (dtac capprox_mult2 1 THEN assume_tac 1);
-by Auto_tac;
-by (dres_inst_tac [("c","inverse x")] capprox_mult1 1
- THEN assume_tac 1);
-by (auto_tac (claset() addIs [capprox_sym],
- simpset() addsimps [hcomplex_mult_assoc]));
-qed "capprox_inverse";
-
-bind_thm ("hcomplex_of_complex_capprox_inverse",
- hcomplex_of_complex_CFinite_diff_CInfinitesimal RSN (2, capprox_inverse));
-
-Goal "[| x: CFinite - CInfinitesimal; \
-\ h : CInfinitesimal |] ==> inverse(x + h) @c= inverse x";
-by (auto_tac (claset() addIs [capprox_inverse, capprox_sym,
- CInfinitesimal_add_capprox_self],
- simpset()));
-qed "inverse_add_CInfinitesimal_capprox";
-
-Goal "[| x: CFinite - CInfinitesimal; \
-\ h : CInfinitesimal |] ==> inverse(h + x) @c= inverse x";
-by (rtac (hcomplex_add_commute RS subst) 1);
-by (blast_tac (claset() addIs [inverse_add_CInfinitesimal_capprox]) 1);
-qed "inverse_add_CInfinitesimal_capprox2";
-
-Goal "[| x : CFinite - CInfinitesimal; \
-\ h : CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h";
-by (rtac capprox_trans2 1);
-by (auto_tac (claset() addIs [inverse_add_CInfinitesimal_capprox],
- simpset() addsimps [mem_cinfmal_iff,hcomplex_diff_def,
- capprox_minus_iff RS sym]));
-qed "inverse_add_CInfinitesimal_approx_CInfinitesimal";
-
-Goal "(x*x : CInfinitesimal) = (x : CInfinitesimal)";
-by (auto_tac (claset(), simpset() addsimps [CInfinitesimal_hcmod_iff,
- hcmod_mult]));
-qed "CInfinitesimal_square_iff";
-AddIffs [CInfinitesimal_square_iff];
-
-Goal "[| a: CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z";
-by (Step_tac 1);
-by (ftac CFinite_inverse 1 THEN assume_tac 1);
-by (dtac not_CInfinitesimal_not_zero 1);
-by (auto_tac (claset() addDs [capprox_mult2],
- simpset() addsimps [hcomplex_mult_assoc RS sym]));
-qed "capprox_CFinite_mult_cancel";
-
-Goal "a: CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)";
-by (auto_tac (claset() addIs [capprox_mult2,
- capprox_CFinite_mult_cancel], simpset()));
-qed "capprox_CFinite_mult_cancel_iff1";
-
-
-(*---------------------------------------------------------------------------*)
-(* Theorems about monads *)
-(*---------------------------------------------------------------------------*)
-
-Goalw [cmonad_def] "(x @c= y) = (cmonad(x)=cmonad(y))";
-by (auto_tac (claset() addDs [capprox_sym]
- addSEs [capprox_trans,equalityCE],
- simpset()));
-qed "capprox_cmonad_iff";
-
-Goal "e : CInfinitesimal ==> cmonad (x+e) = cmonad x";
-by (fast_tac (claset() addSIs [CInfinitesimal_add_capprox_self RS capprox_sym,
- capprox_cmonad_iff RS iffD1]) 1);
-qed "CInfinitesimal_cmonad_eq";
-
-Goalw [cmonad_def] "(u:cmonad x) = (-u:cmonad (-x))";
-by Auto_tac;
-qed "mem_cmonad_iff";
-
-Goalw [cmonad_def] "(x:CInfinitesimal) = (x:cmonad 0)";
-by (auto_tac (claset() addIs [capprox_sym],
- simpset() addsimps [mem_cinfmal_iff]));
-qed "CInfinitesimal_cmonad_zero_iff";
-
-Goal "(x:cmonad 0) = (-x:cmonad 0)";
-by (simp_tac (simpset() addsimps [CInfinitesimal_cmonad_zero_iff RS sym]) 1);
-qed "cmonad_zero_minus_iff";
-
-Goal "(x:cmonad 0) = (hcmod x:monad 0)";
-by (auto_tac (claset(), simpset() addsimps
- [CInfinitesimal_cmonad_zero_iff RS sym,
- CInfinitesimal_hcmod_iff,Infinitesimal_monad_zero_iff RS sym]));
-qed "cmonad_zero_hcmod_iff";
-
-Goalw [cmonad_def] "x:cmonad x";
-by (Simp_tac 1);
-qed "mem_cmonad_self";
-Addsimps [mem_cmonad_self];
-
-(*---------------------------------------------------------------------------*)
-(* Theorems about standard part *)
-(*---------------------------------------------------------------------------*)
-Goalw [stc_def] "x: CFinite ==> stc x @c= x";
-by (forward_tac [stc_part_Ex] 1 THEN Step_tac 1);
-by (rtac someI2 1);
-by (auto_tac (claset() addIs [capprox_sym], simpset()));
-qed "stc_capprox_self";
-
-Goalw [stc_def] "x: CFinite ==> stc x: SComplex";
-by (forward_tac [stc_part_Ex] 1 THEN Step_tac 1);
-by (rtac someI2 1);
-by (auto_tac (claset() addIs [capprox_sym], simpset()));
-qed "stc_SComplex";
-
-Goal "x: CFinite ==> stc x: CFinite";
-by (etac (stc_SComplex RS (SComplex_subset_CFinite RS subsetD)) 1);
-qed "stc_CFinite";
-
-Goalw [stc_def] "x: SComplex ==> stc x = x";
-by (rtac some_equality 1);
-by (auto_tac (claset() addIs [(SComplex_subset_CFinite RS subsetD)],simpset()));
-by (blast_tac (claset() addDs [SComplex_capprox_iff RS iffD1]) 1);
-qed "stc_SComplex_eq";
-Addsimps [stc_SComplex_eq];
-
-Goal "stc (hcomplex_of_complex x) = hcomplex_of_complex x";
-by Auto_tac;
-qed "stc_hcomplex_of_complex";
-
-Goal "[| x: CFinite; y: CFinite; stc x = stc y |] ==> x @c= y";
-by (auto_tac (claset() addSDs [stc_capprox_self]
- addSEs [capprox_trans3], simpset()));
-qed "stc_eq_capprox";
-
-Goal "[| x: CFinite; y: CFinite; x @c= y |] ==> stc x = stc y";
-by (EVERY1 [forward_tac [stc_capprox_self],
- forw_inst_tac [("x","y")] stc_capprox_self,
- dtac stc_SComplex,dtac stc_SComplex]);
-by (fast_tac (claset() addEs [capprox_trans,
- capprox_trans2,SComplex_capprox_iff RS iffD1]) 1);
-qed "capprox_stc_eq";
-
-Goal "[| x: CFinite; y: CFinite|] ==> (x @c= y) = (stc x = stc y)";
-by (blast_tac (claset() addIs [capprox_stc_eq,stc_eq_capprox]) 1);
-qed "stc_eq_capprox_iff";
-
-Goal "[| x: SComplex; e: CInfinitesimal |] ==> stc(x + e) = x";
-by (forward_tac [stc_SComplex_eq RS subst] 1);
-by (assume_tac 2);
-by (forward_tac [SComplex_subset_CFinite RS subsetD] 1);
-by (forward_tac [CInfinitesimal_subset_CFinite RS subsetD] 1);
-by (dtac stc_SComplex_eq 1);
-by (rtac capprox_stc_eq 1);
-by (auto_tac (claset() addIs [CFinite_add],
- simpset() addsimps [CInfinitesimal_add_capprox_self
- RS capprox_sym]));
-qed "stc_CInfinitesimal_add_SComplex";
-
-Goal "[| x: SComplex; e: CInfinitesimal |] ==> stc(e + x) = x";
-by (rtac (hcomplex_add_commute RS subst) 1);
-by (blast_tac (claset() addSIs [stc_CInfinitesimal_add_SComplex]) 1);
-qed "stc_CInfinitesimal_add_SComplex2";
-
-Goal "x: CFinite ==> EX e: CInfinitesimal. x = stc(x) + e";
-by (blast_tac (claset() addSDs [(stc_capprox_self RS
- capprox_sym),bex_CInfinitesimal_iff2 RS iffD2]) 1);
-qed "CFinite_stc_CInfinitesimal_add";
-
-Goal "[| x: CFinite; y: CFinite |] ==> stc (x + y) = stc(x) + stc(y)";
-by (forward_tac [CFinite_stc_CInfinitesimal_add] 1);
-by (forw_inst_tac [("x","y")] CFinite_stc_CInfinitesimal_add 1);
-by (Step_tac 1);
-by (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))" 1);
-by (dtac sym 2 THEN dtac sym 2);
-by (Asm_full_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
-by (REPEAT(dtac stc_SComplex 1));
-by (dtac SComplex_add 1 THEN assume_tac 1);
-by (dtac CInfinitesimal_add 1 THEN assume_tac 1);
-by (rtac (hcomplex_add_assoc RS subst) 1);
-by (blast_tac (claset() addSIs [stc_CInfinitesimal_add_SComplex2]) 1);
-qed "stc_add";
-
-Goal "stc (number_of w) = number_of w";
-by (rtac (SComplex_number_of RS stc_SComplex_eq) 1);
-qed "stc_number_of";
-Addsimps [stc_number_of];
-
-Goal "stc 0 = 0";
-by (Simp_tac 1);
-qed "stc_zero";
-Addsimps [stc_zero];
-
-Goal "stc 1 = 1";
-by (Simp_tac 1);
-qed "stc_one";
-Addsimps [stc_one];
-
-Goal "y: CFinite ==> stc(-y) = -stc(y)";
-by (forward_tac [CFinite_minus_iff RS iffD2] 1);
-by (rtac hcomplex_add_minus_eq_minus 1);
-by (dtac (stc_add RS sym) 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
-qed "stc_minus";
-
-Goalw [hcomplex_diff_def]
- "[| x: CFinite; y: CFinite |] ==> stc (x-y) = stc(x) - stc(y)";
-by (forw_inst_tac [("y1","y")] (stc_minus RS sym) 1);
-by (dres_inst_tac [("x1","y")] (CFinite_minus_iff RS iffD2) 1);
-by (auto_tac (claset() addIs [stc_add],simpset()));
-qed "stc_diff";
-
-Goal "[| x: CFinite; y: CFinite; \
-\ e: CInfinitesimal; \
-\ ea: CInfinitesimal |] \
-\ ==> e*y + x*ea + e*ea: CInfinitesimal";
-by (forw_inst_tac [("x","e"),("y","y")] CInfinitesimal_CFinite_mult 1);
-by (forw_inst_tac [("x","ea"),("y","x")] CInfinitesimal_CFinite_mult 2);
-by (dtac CInfinitesimal_mult 3);
-by (auto_tac (claset() addIs [CInfinitesimal_add],
- simpset() addsimps add_ac @ mult_ac));
-qed "lemma_stc_mult";
-
-Goal "[| x: CFinite; y: CFinite |] \
-\ ==> stc (x * y) = stc(x) * stc(y)";
-by (forward_tac [CFinite_stc_CInfinitesimal_add] 1);
-by (forw_inst_tac [("x","y")] CFinite_stc_CInfinitesimal_add 1);
-by (Step_tac 1);
-by (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))" 1);
-by (dtac sym 2 THEN dtac sym 2);
-by (Asm_full_simp_tac 2);
-by (thin_tac "x = stc x + e" 1);
-by (thin_tac "y = stc y + ea" 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hcomplex_add_mult_distrib,right_distrib]) 1);
-by (REPEAT(dtac stc_SComplex 1));
-by (full_simp_tac (simpset() addsimps [hcomplex_add_assoc]) 1);
-by (rtac stc_CInfinitesimal_add_SComplex 1);
-by (blast_tac (claset() addSIs [SComplex_mult]) 1);
-by (REPEAT(dtac (SComplex_subset_CFinite RS subsetD) 1));
-by (rtac (hcomplex_add_assoc RS subst) 1);
-by (blast_tac (claset() addSIs [lemma_stc_mult]) 1);
-qed "stc_mult";
-
-Goal "x: CInfinitesimal ==> stc x = 0";
-by (rtac (stc_zero RS subst) 1);
-by (rtac capprox_stc_eq 1);
-by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite RS subsetD],
- simpset() addsimps [mem_cinfmal_iff RS sym]));
-qed "stc_CInfinitesimal";
-
-Goal "stc(x) ~= 0 ==> x ~: CInfinitesimal";
-by (fast_tac (claset() addIs [stc_CInfinitesimal]) 1);
-qed "stc_not_CInfinitesimal";
-
-Goal "[| x: CFinite; stc x ~= 0 |] \
-\ ==> stc(inverse x) = inverse (stc x)";
-by (res_inst_tac [("c1","stc x")] (hcomplex_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [stc_mult RS sym, stc_not_CInfinitesimal,
- CFinite_inverse]));
-by (stac right_inverse 1);
-by Auto_tac;
-qed "stc_inverse";
-
-Goal "[| x: CFinite; y: CFinite; stc y ~= 0 |] \
-\ ==> stc(x/y) = (stc x) / (stc y)";
-by (auto_tac (claset(),
- simpset() addsimps [hcomplex_divide_def, stc_mult, stc_not_CInfinitesimal,
- CFinite_inverse, stc_inverse]));
-qed "stc_divide";
-Addsimps [stc_divide];
-
-Goal "x: CFinite ==> stc(stc(x)) = stc(x)";
-by (blast_tac (claset() addIs [stc_CFinite, stc_capprox_self,
- capprox_stc_eq]) 1);
-qed "stc_idempotent";
-Addsimps [stc_idempotent];
-
-Goal "z : HFinite ==> hcomplex_of_hypreal z : CFinite";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
- CFinite_HFinite_iff,symmetric hypreal_zero_def]));
-qed "CFinite_HFinite_hcomplex_of_hypreal";
-
-Goal "x : Reals ==> hcomplex_of_hypreal x : SComplex";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,
- SComplex_SReal_iff,symmetric hypreal_zero_def]));
-qed "SComplex_SReal_hcomplex_of_hypreal";
-
-Goalw [st_def,stc_def]
- "z : HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)";
-by (ftac st_part_Ex 1 THEN Step_tac 1);
-by (rtac someI2 1);
-by (auto_tac (claset() addIs [approx_sym],simpset()));
-by (dtac CFinite_HFinite_hcomplex_of_hypreal 1);
-by (ftac stc_part_Ex 1 THEN Step_tac 1);
-by (rtac someI2 1);
-by (auto_tac (claset() addIs [capprox_sym] addSIs [capprox_unique_complex]
- addDs [SComplex_SReal_hcomplex_of_hypreal],simpset()));
-qed "stc_hcomplex_of_hypreal";
-
-(*
-Goal "x: CFinite ==> hcmod(stc x) = st(hcmod x)";
-by (dtac stc_capprox_self 1);
-by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym]));
-
-
-approx_hcmod_add_hcmod
-*)
-
-(*---------------------------------------------------------------------------*)
-(* More nonstandard complex specific theorems *)
-(*---------------------------------------------------------------------------*)
-Goal "(hcnj z : CInfinitesimal) = (z : CInfinitesimal)";
-by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
-qed "CInfinitesimal_hcnj_iff";
-Addsimps [CInfinitesimal_hcnj_iff];
-
-Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : CInfinite) = \
-\ (Abs_hypreal(hyprel `` {%n. Re(X n)}) : HInfinite | \
-\ Abs_hypreal(hyprel `` {%n. Im(X n)}) : HInfinite)";
-by (auto_tac (claset(),simpset() addsimps [CInfinite_CFinite_iff,
- HInfinite_HFinite_iff,CFinite_HFinite_iff]));
-qed "CInfinite_HInfinite_iff";
-
-Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CInfinitesimal) = \
-\ (x : Infinitesimal & y : Infinitesimal)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
- hcomplex_of_hypreal,CInfinitesimal_Infinitesimal_iff]));
-qed "hcomplex_split_CInfinitesimal_iff";
-
-Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CFinite) = \
-\ (x : HFinite & y : HFinite)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
- hcomplex_of_hypreal,CFinite_HFinite_iff]));
-qed "hcomplex_split_CFinite_iff";
-
-Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : SComplex) = \
-\ (x : Reals & y : Reals)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
- hcomplex_of_hypreal,SComplex_SReal_iff]));
-qed "hcomplex_split_SComplex_iff";
-
-Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y : CInfinite) = \
-\ (x : HInfinite | y : HInfinite)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
- hcomplex_of_hypreal,CInfinite_HInfinite_iff]));
-qed "hcomplex_split_CInfinite_iff";
-
-Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c= \
-\ hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = \
-\ (x @= x' & y @= y')";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","x'")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y'")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [iii_def,hcomplex_add,hcomplex_mult,
- hcomplex_of_hypreal,capprox_approx_iff]));
-qed "hcomplex_split_capprox_iff";
-
-(*** More theorems ***)
-
-Goal "ALL n. cmod (X n - x) < inverse (real (Suc n)) ==> \
-\ Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x : CInfinitesimal";
-by (auto_tac (claset(),simpset() addsimps [hcomplex_diff,
- CInfinitesimal_hcmod_iff,hcomplex_of_complex_def,
- Infinitesimal_FreeUltrafilterNat_iff,hcmod]));
-by (rtac bexI 1 THEN Auto_tac);
-by (auto_tac (claset() addDs [FreeUltrafilterNat_inverse_real_of_posnat,
- FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
- addIs [order_less_trans, FreeUltrafilterNat_subset],
- simpset()));
-qed "complex_seq_to_hcomplex_CInfinitesimal";
-
-Goal "hcomplex_of_hypreal epsilon : CInfinitesimal";
-by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff]));
-qed "CInfinitesimal_hcomplex_of_hypreal_epsilon";
-Addsimps [CInfinitesimal_hcomplex_of_hypreal_epsilon];
-
-Goal "(hcomplex_of_complex z @c= 0) = (z = 0)";
-by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_zero RS sym]
- delsimps [hcomplex_of_complex_zero]));
-qed "hcomplex_of_complex_approx_zero_iff";
-
-Goal "(0 @c= hcomplex_of_complex z) = (z = 0)";
-by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_zero RS sym]
- delsimps [hcomplex_of_complex_zero]));
-qed "hcomplex_of_complex_approx_zero_iff2";
-
-Addsimps [hcomplex_of_complex_approx_zero_iff,hcomplex_of_complex_approx_zero_iff2];
-
-