# HG changeset patch # User huffman # Date 1166041556 -3600 # Node ID 54018ed3b99d857b88f878784a8002838bbf7d00 # Parent f9243336f54e6311457a9ba7610b120662c21c78 added lemmas about hRe, hIm, HComplex; removed all uses of star_n diff -r f9243336f54e -r 54018ed3b99d src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Wed Dec 13 20:38:24 2006 +0100 +++ b/src/HOL/Complex/CLim.thy Wed Dec 13 21:25:56 2006 +0100 @@ -88,12 +88,6 @@ lemma starfun_norm: "( *f* (\x. norm (f x))) = (\x. hnorm (( *f* f) x))" by transfer (rule refl) -lemma starfun_Re: "( *f* (\x. Re (f x))) = (\x. hRe (( *f* f) x))" -by transfer (rule refl) - -lemma starfun_Im: "( *f* (\x. Im (f x))) = (\x. hIm (( *f* f) x))" -by transfer (rule refl) - lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)" by transfer (rule refl) @@ -122,7 +116,7 @@ apply (auto intro: NSLIM_Re NSLIM_Im) apply (auto simp add: NSLIM_def starfun_Re starfun_Im) apply (auto dest!: spec) -apply (simp add: starfunC_approx_Re_Im_iff starfun_Re starfun_Im) +apply (simp add: hcomplex_approx_iff) done lemma LIM_CRLIM_Re_Im_iff: diff -r f9243336f54e -r 54018ed3b99d src/HOL/Complex/CStar.thy --- a/src/HOL/Complex/CStar.thy Wed Dec 13 20:38:24 2006 +0100 +++ b/src/HOL/Complex/CStar.thy Wed Dec 13 21:25:56 2006 +0100 @@ -22,41 +22,38 @@ subsection{*Theorems about Nonstandard Extensions of Functions*} -lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" -apply (cases Z) -apply (simp add: hcpow starfun hypnat_of_nat_eq) -done +lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" +by transfer (rule refl) lemma starfunCR_cmod: "*f* cmod = hcmod" -apply (rule ext) -apply (rule_tac x = x in star_cases) -apply (simp add: starfun hcmod) -done +by transfer (rule refl) subsection{*Internal Functions - Some Redundancy With *f* Now*} (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) - +(* lemma starfun_n_diff: "( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z" apply (cases z) apply (simp add: starfun_n star_n_diff) done +*) +(** composition: ( *fn) o ( *gn) = *(fn o gn) **) -(** composition: ( *fn) o ( *gn) = *(fn o gn) **) +lemma starfun_Re: "( *f* (\x. Re (f x))) = (\x. hRe (( *f* f) x))" +by transfer (rule refl) + +lemma starfun_Im: "( *f* (\x. Im (f x))) = (\x. hIm (( *f* f) x))" +by transfer (rule refl) lemma starfunC_eq_Re_Im_iff: "(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) & (( *f* (%x. Im(f x))) x = hIm (z)))" -apply (cases x, cases z) -apply (auto simp add: starfun hIm hRe complex_Re_Im_cancel_iff star_n_eq_iff, ultra+) -done +by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im) lemma starfunC_approx_Re_Im_iff: "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & (( *f* (%x. Im(f x))) x @= hIm (z)))" -apply (cases x, cases z) -apply (simp add: starfun hIm hRe approx_approx_iff) -done +by (simp add: hcomplex_approx_iff starfun_Re starfun_Im) end diff -r f9243336f54e -r 54018ed3b99d src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Wed Dec 13 20:38:24 2006 +0100 +++ b/src/HOL/Complex/NSCA.thy Wed Dec 13 21:25:56 2006 +0100 @@ -312,170 +312,133 @@ "[| r \ SComplex; s \ SComplex; r @= x; s @= x|] ==> r = s" by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) -lemma hcomplex_approxD1: - "star_n X @= star_n Y - ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" -apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) -apply (drule approx_minus_iff [THEN iffD1]) -apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) -apply (drule_tac x = m in spec) -apply (erule ultra, rule FreeUltrafilterNat_all, clarify) -apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) -apply (case_tac "X n") -apply (case_tac "Y n") -apply (auto simp add: complex_diff complex_mod - simp del: realpow_Suc) +subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *} + +lemma abs_Re_le_cmod: "\Re x\ \ cmod x" +by (induct x) simp + +lemma abs_Im_le_cmod: "\Im x\ \ cmod x" +by (induct x) simp + +lemma abs_hRe_le_hcmod: "\x. \hRe x\ \ hcmod x" +by transfer (rule abs_Re_le_cmod) + +lemma abs_hIm_le_hcmod: "\x. \hIm x\ \ hcmod x" +by transfer (rule abs_Im_le_cmod) + +lemma Infinitesimal_hRe: "x \ Infinitesimal \ hRe x \ Infinitesimal" +apply (rule InfinitesimalI2, simp) +apply (rule order_le_less_trans [OF abs_hRe_le_hcmod]) +apply (erule (1) InfinitesimalD2) +done + +lemma Infinitesimal_hIm: "x \ Infinitesimal \ hIm x \ Infinitesimal" +apply (rule InfinitesimalI2, simp) +apply (rule order_le_less_trans [OF abs_hIm_le_hcmod]) +apply (erule (1) InfinitesimalD2) +done + +lemma real_sqrt_lessI: "\0 \ x; 0 < u; x < u\\ \ sqrt x < u" +by (frule (1) real_sqrt_less_mono) simp + +lemma hypreal_sqrt_lessI: + "\x u. \0 \ x; 0 < u; x < u\\ \ ( *f* sqrt) x < u" +by transfer (rule real_sqrt_lessI) + +lemma hypreal_sqrt_ge_zero: "\x. 0 \ x \ 0 \ ( *f* sqrt) x" +by transfer (rule real_sqrt_ge_zero) + +lemma Infinitesimal_sqrt: + "\x \ Infinitesimal; 0 \ x\ \ ( *f* sqrt) x \ Infinitesimal" +apply (rule InfinitesimalI2) +apply (drule_tac r="r\" in InfinitesimalD2, simp) +apply (simp add: hypreal_sqrt_ge_zero) +apply (rule hypreal_sqrt_lessI, simp_all) done -(* same proof *) -lemma hcomplex_approxD2: - "star_n X @= star_n Y - ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" -apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) -apply (drule approx_minus_iff [THEN iffD1]) -apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) -apply (drule_tac x = m in spec) -apply (erule ultra, rule FreeUltrafilterNat_all, clarify) -apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) -apply (case_tac "X n") -apply (case_tac "Y n") -apply (auto simp add: complex_diff complex_mod - simp del: realpow_Suc) +lemma Infinitesimal_HComplex: + "\x \ Infinitesimal; y \ Infinitesimal\ \ HComplex x y \ Infinitesimal" +apply (rule Infinitesimal_hcmod_iff [THEN iffD2]) +apply (simp add: hcmod_i) +apply (rule Infinitesimal_sqrt) +apply (rule Infinitesimal_add) +apply (erule Infinitesimal_hrealpow, simp) +apply (erule Infinitesimal_hrealpow, simp) +apply (rule add_nonneg_nonneg) +apply (rule zero_le_power2) +apply (rule zero_le_power2) +done + +lemma hcomplex_Infinitesimal_iff: + "(x \ Infinitesimal) = (hRe x \ Infinitesimal \ hIm x \ Infinitesimal)" +apply (safe intro!: Infinitesimal_hRe Infinitesimal_hIm) +apply (drule (1) Infinitesimal_HComplex, simp) done -lemma hcomplex_approxI: - "[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); - star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) - |] ==> star_n X @= star_n Y" -apply (drule approx_minus_iff [THEN iffD1]) -apply (drule approx_minus_iff [THEN iffD1]) -apply (rule approx_minus_iff [THEN iffD2]) -apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_diff Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) -apply (drule_tac x = "u/2" in spec) -apply (drule_tac x = "u/2" in spec, auto, ultra) -apply (case_tac "X x") -apply (case_tac "Y x") -apply (auto simp add: complex_diff complex_mod snd_conv fst_conv numeral_2_eq_2) -apply (rename_tac a b c d) -apply (subgoal_tac "sqrt (abs (a - c) ^ 2 + abs (b - d) ^ 2) < u") -apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) -apply (simp add: power2_eq_square) +lemma hRe_diff [simp]: "\x y. hRe (x - y) = hRe x - hRe y" +by transfer (rule complex_Re_diff) + +lemma hIm_diff [simp]: "\x y. hIm (x - y) = hIm x - hIm y" +by transfer (rule complex_Im_diff) + +lemma approx_hRe: "x \ y \ hRe x \ hRe y" +unfolding approx_def by (drule Infinitesimal_hRe) simp + +lemma approx_hIm: "x \ y \ hIm x \ hIm y" +unfolding approx_def by (drule Infinitesimal_hIm) simp + +lemma approx_HComplex: + "\a \ b; c \ d\ \ HComplex a c \ HComplex b d" +unfolding approx_def by (simp add: Infinitesimal_HComplex) + +lemma hcomplex_approx_iff: + "(x \ y) = (hRe x \ hRe y \ hIm x \ hIm y)" +unfolding approx_def by (simp add: hcomplex_Infinitesimal_iff) + +lemma HFinite_hRe: "x \ HFinite \ hRe x \ HFinite" +apply (auto simp add: HFinite_def SReal_def) +apply (rule_tac x="star_of r" in exI, simp) +apply (erule order_le_less_trans [OF abs_hRe_le_hcmod]) done -lemma approx_approx_iff: - "(star_n X @= star_n Y) = - (star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)) & - star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)))" -apply (blast intro: hcomplex_approxI hcomplex_approxD1 hcomplex_approxD2) +lemma HFinite_hIm: "x \ HFinite \ hIm x \ HFinite" +apply (auto simp add: HFinite_def SReal_def) +apply (rule_tac x="star_of r" in exI, simp) +apply (erule order_le_less_trans [OF abs_hIm_le_hcmod]) done +lemma HFinite_HComplex: + "\x \ HFinite; y \ HFinite\ \ HComplex x y \ HFinite" +apply (subgoal_tac "HComplex x 0 + HComplex 0 y \ HFinite", simp) +apply (rule HFinite_add) +apply (simp add: HFinite_hcmod_iff hcmod_i) +apply (simp add: HFinite_hcmod_iff hcmod_i) +done + +lemma hcomplex_HFinite_iff: + "(x \ HFinite) = (hRe x \ HFinite \ hIm x \ HFinite)" +apply (safe intro!: HFinite_hRe HFinite_hIm) +apply (drule (1) HFinite_HComplex, simp) +done + +lemma hcomplex_HInfinite_iff: + "(x \ HInfinite) = (hRe x \ HInfinite \ hIm x \ HInfinite)" +by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff) + lemma hcomplex_of_hypreal_approx_iff [simp]: "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" -apply (cases x, cases z) -apply (simp add: hcomplex_of_hypreal approx_approx_iff) -done - -lemma HFinite_HFinite_Re: - "star_n X \ HFinite - ==> star_n (%n. Re(X n)) \ HFinite" -apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) -apply (rule_tac x = u in exI, ultra) -apply (case_tac "X x") -apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) -apply (rule ccontr, drule linorder_not_less [THEN iffD1]) -apply (drule order_less_le_trans, assumption) -apply (drule real_sqrt_ge_abs1 [THEN [2] order_less_le_trans]) -apply (auto simp add: numeral_2_eq_2 [symmetric]) -done - -lemma HFinite_HFinite_Im: - "star_n X \ HFinite - ==> star_n (%n. Im(X n)) \ HFinite" -apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) -apply (rule_tac x = u in exI, ultra) -apply (case_tac "X x") -apply (auto simp add: complex_mod simp del: realpow_Suc) -apply (rule ccontr, drule linorder_not_less [THEN iffD1]) -apply (drule order_less_le_trans, assumption) -apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) -done - -lemma HFinite_Re_Im_HFinite: - "[| star_n (%n. Re(X n)) \ HFinite; - star_n (%n. Im(X n)) \ HFinite - |] ==> star_n X \ HFinite" -apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) -apply (rename_tac u v) -apply (rule_tac x = "2* (u + v) " in exI) -apply ultra -apply (case_tac "X x") -apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) -apply (subgoal_tac "0 < u") - prefer 2 apply arith -apply (subgoal_tac "0 < v") - prefer 2 apply arith -apply (subgoal_tac "sqrt (abs (Re (X x)) ^ 2 + abs (Im (X x)) ^ 2) < 2*u + 2*v") -apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) -apply (simp add: power2_eq_square) -done +by (simp add: hcomplex_approx_iff) -lemma HFinite_HFinite_iff: - "(star_n X \ HFinite) = - (star_n (%n. Re(X n)) \ HFinite & - star_n (%n. Im(X n)) \ HFinite)" -by (blast intro: HFinite_Re_Im_HFinite HFinite_HFinite_Im HFinite_HFinite_Re) - -lemma SComplex_Re_SReal: - "star_n X \ SComplex - ==> star_n (%n. Re(X n)) \ Reals" -apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff) -apply (rule_tac x = "Re x" in exI, ultra) -done - -lemma SComplex_Im_SReal: - "star_n X \ SComplex - ==> star_n (%n. Im(X n)) \ Reals" -apply (auto simp add: Standard_def SReal_def star_of_def star_n_eq_iff) -apply (rule_tac x = "Im x" in exI, ultra) -done - -lemma Reals_Re_Im_SComplex: - "[| star_n (%n. Re(X n)) \ Reals; - star_n (%n. Im(X n)) \ Reals - |] ==> star_n X \ SComplex" -apply (auto simp add: Standard_def image_def SReal_def star_of_def star_n_eq_iff) -apply (rule_tac x = "Complex r ra" in exI, ultra) -done - -lemma SComplex_SReal_iff: - "(star_n X \ SComplex) = - (star_n (%n. Re(X n)) \ Reals & - star_n (%n. Im(X n)) \ Reals)" -by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) - -lemma Infinitesimal_Infinitesimal_iff: - "(star_n X \ Infinitesimal) = - (star_n (%n. Re(X n)) \ Infinitesimal & - star_n (%n. Im(X n)) \ Infinitesimal)" -by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) - -lemma eq_Abs_star_EX: - "(\t. P t) = (\X. P (star_n X))" -by (rule ex_star_eq) - -lemma eq_Abs_star_Bex: - "(\t \ A. P t) = (\X. star_n X \ A & P (star_n X))" -by (simp add: Bex_def ex_star_eq) +lemma Standard_HComplex: + "\x \ Standard; y \ Standard\ \ HComplex x y \ Standard" +by (simp add: HComplex_def) (* Here we go - easy proof now!! *) lemma stc_part_Ex: "x:HFinite ==> \t \ SComplex. x @= t" -apply (cases x) -apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) -apply (drule st_part_Ex, safe)+ -apply (rule_tac x = t in star_cases) -apply (rule_tac x = ta in star_cases, auto) -apply (rule_tac x = "%n. Complex (Xa n) (Xb n) " in exI) -apply auto +apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff) +apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI) +apply (simp add: st_approx_self [THEN approx_sym]) +apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard]) done lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \ SComplex & x @= t" @@ -607,9 +570,7 @@ lemma HFinite_HFinite_hcomplex_of_hypreal: "z \ HFinite ==> hcomplex_of_hypreal z \ HFinite" -apply (cases z) -apply (simp add: hcomplex_of_hypreal HFinite_HFinite_iff star_n_zero_num [symmetric]) -done +by (simp add: hcomplex_HFinite_iff) lemma SComplex_SReal_hcomplex_of_hypreal: "x \ Reals ==> hcomplex_of_hypreal x \ SComplex" @@ -637,54 +598,6 @@ "(hcnj z \ Infinitesimal) = (z \ Infinitesimal)" by (simp add: Infinitesimal_hcmod_iff) -lemma HInfinite_HInfinite_iff: - "(star_n X \ HInfinite) = - (star_n (%n. Re(X n)) \ HInfinite | - star_n (%n. Im(X n)) \ HInfinite)" -by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) - -text{*These theorems should probably be deleted*} -lemma hcomplex_split_Infinitesimal_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ Infinitesimal) = - (x \ Infinitesimal & y \ Infinitesimal)" -apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) -done - -lemma hcomplex_split_HFinite_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ HFinite) = - (x \ HFinite & y \ HFinite)" -apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) -done - -lemma hcomplex_split_SComplex_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ SComplex) = - (x \ Reals & y \ Reals)" -apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) -done - -lemma hcomplex_split_HInfinite_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ HInfinite) = - (x \ HInfinite | y \ HInfinite)" -apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) -done - -lemma hcomplex_split_approx_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= - hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = - (x @= x' & y @= y')" -apply (cases x, cases y, cases x', cases y') -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) -done - -lemma complex_seq_to_hcomplex_Infinitesimal: - "\n. cmod (X n - x) < inverse (real (Suc n)) ==> - star_n X - hcomplex_of_complex x \ Infinitesimal" -by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) - lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: "hcomplex_of_hypreal epsilon \ Infinitesimal" by (simp add: Infinitesimal_hcmod_iff) diff -r f9243336f54e -r 54018ed3b99d src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Wed Dec 13 20:38:24 2006 +0100 +++ b/src/HOL/Complex/NSComplex.thy Wed Dec 13 21:25:56 2006 +0100 @@ -88,18 +88,48 @@ hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def +lemma Standard_hRe [simp]: "x \ Standard \ hRe x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hIm [simp]: "x \ Standard \ hIm x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_iii [simp]: "iii \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hcnj [simp]: "x \ Standard \ hcnj x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hsgn [simp]: "x \ Standard \ hsgn x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_harg [simp]: "x \ Standard \ harg x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hcis [simp]: "r \ Standard \ hcis r \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hexpi [simp]: "x \ Standard \ hexpi x \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hrcis [simp]: + "\r \ Standard; s \ Standard\ \ hrcis r s \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_HComplex [simp]: + "\r \ Standard; s \ Standard\ \ HComplex r s \ Standard" +by (simp add: hcomplex_defs) + +lemma Standard_hcomplex_of_hypreal [simp]: + "r \ Standard \ hcomplex_of_hypreal r \ Standard" +by (simp add: hcomplex_defs) + lemma hcmod_def: "hcmod = *f* cmod" by (rule hnorm_def) subsection{*Properties of Nonstandard Real and Imaginary Parts*} -lemma hRe: "hRe (star_n X) = star_n (%n. Re(X n))" -by (simp add: hRe_def starfun) - -lemma hIm: "hIm (star_n X) = star_n (%n. Im(X n))" -by (simp add: hIm_def starfun) - lemma hcomplex_hRe_hIm_cancel_iff: "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" by transfer (rule complex_Re_Im_cancel_iff) @@ -181,10 +211,6 @@ subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} -lemma hcomplex_of_hypreal: - "hcomplex_of_hypreal (star_n X) = star_n (%n. complex_of_real (X n))" -by (simp add: hcomplex_of_hypreal_def starfun) - lemma hcomplex_of_hypreal_cancel_iff [iff]: "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" by transfer (rule of_real_eq_iff) @@ -229,10 +255,13 @@ lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" by transfer (rule Im_complex_of_real) +lemma hcomplex_of_hypreal_zero_iff [simp]: + "\x. (hcomplex_of_hypreal x = 0) = (x = 0)" +by transfer (rule of_real_eq_0_iff) + lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal epsilon \ 0" -by (simp add: hcomplex_of_hypreal epsilon_def star_n_zero_num star_n_eq_iff) - +by (simp add: hypreal_epsilon_not_zero) subsection{*HComplex theorems*} @@ -242,12 +271,6 @@ lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" by transfer (rule Im) -text{*Relates the two nonstandard constructions*} -lemma HComplex_eq_Abs_star_Complex: - "HComplex (star_n X) (star_n Y) = - star_n (%n::nat. Complex (X n) (Y n))" -by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) - lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" by transfer (rule complex_surj) @@ -258,9 +281,6 @@ subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} -lemma hcmod: "hcmod (star_n X) = star_n (%n. cmod (X n))" -by (simp add: hcmod_def starfun) - lemma hcmod_zero [simp]: "hcmod(0) = 0" by (rule hnorm_zero) @@ -328,9 +348,6 @@ subsection{*Conjugation*} -lemma hcnj: "hcnj (star_n X) = star_n (%n. cnj(X n))" -by (simp add: hcnj_def starfun) - lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" by transfer (rule complex_cnj_cancel_iff) @@ -445,9 +462,6 @@ subsection{*A Few Nonlinear Theorems*} -lemma hcpow: "star_n X hcpow star_n Y = star_n (%n. X n ^ Y n)" -by (simp add: hcpow_def starfun2_star_n) - lemma hcomplex_of_hypreal_hyperpow: "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" by transfer (rule complex_of_real_pow) @@ -505,14 +519,8 @@ lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" by (blast intro: ccontr dest: hcpow_not_zero) -lemma star_n_divide: "star_n X / star_n Y = star_n (%n. X n / Y n)" -by (simp add: star_divide_def starfun2_star_n) - subsection{*The Function @{term hsgn}*} -lemma hsgn: "hsgn (star_n X) = star_n (%n. sgn (X n))" -by (simp add: hsgn_def starfun) - lemma hsgn_zero [simp]: "hsgn 0 = 0" by transfer (rule sgn_zero) @@ -587,9 +595,6 @@ (* harg *) (*---------------------------------------------------------------------------*) -lemma harg: "harg (star_n X) = star_n (%n. arg (X n))" -by (simp add: harg_def starfun) - lemma cos_harg_i_mult_zero_pos: "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" by transfer (rule cos_arg_i_mult_zero_pos) @@ -613,30 +618,16 @@ "\n. \r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" by (blast intro: complex_split_polar) -lemma lemma_hypreal_P_EX2: - "(\(x::hypreal) y. P x y) = - (\f g. P (star_n f) (star_n g))" -apply auto -apply (rule_tac x = x in star_cases) -apply (rule_tac x = y in star_cases, auto) -done - lemma hcomplex_split_polar: "!!z. \r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" by transfer (rule complex_split_polar) -lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))" -by (simp add: hcis_def starfun) - lemma hcis_eq: "!!a. hcis a = (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" by transfer (simp add: cis_def) -lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))" -by (simp add: hrcis_def starfun2_star_n) - lemma hrcis_Ex: "!!z. \r a. z = hrcis r a" by transfer (rule rcis_Ex)