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)