Theory CStar

(*  Title:      HOL/Nonstandard_Analysis/CStar.thy
    Author:     Jacques D. Fleuriot
    Copyright:  2001 University of Edinburgh

section ‹Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions›

theory CStar
  imports NSCA

subsection ‹Properties of the *›-Transform Applied to Sets of Reals›

lemma STARC_hcomplex_of_complex_Int: "*s* X  SComplex = hcomplex_of_complex ` X"
  by (auto simp: Standard_def)

lemma lemma_not_hcomplexA: "x  hcomplex_of_complex ` A  y  A. x  hcomplex_of_complex y"
  by auto

subsection ‹Theorems about Nonstandard Extensions of Functions›

lemma starfunC_hcpow: "Z. ( *f* (λz. z ^ n)) Z = Z pow hypnat_of_nat n"
  by transfer (rule refl)

lemma starfunCR_cmod: "*f* cmod = hcmod"
  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)
(** 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"
  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"
  by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)