# HG changeset patch # User paulson # Date 1077617759 -3600 # Node ID 1749bc19d51d0ea72b08afea88b7934ec7d3ccdb # Parent 91181ee5860cd5da7d96bd7761c9ed3865aa4fa4 converted NSCA to Isar script diff -r 91181ee5860c -r 1749bc19d51d src/HOL/Complex/NSCA.ML --- 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]; - -