src/HOL/Complex/NSComplex.thy

HOL-Real -> HOL-Complex

(*  Title:       NSComplex.thy
    Author:      Jacques D. Fleuriot
    Copyright:   2001  University of Edinburgh
    Description: Nonstandard Complex numbers
*)

NSComplex = NSInduct + 

constdefs
    hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
    "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) & 
                        {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"

typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"      (quotient_def)

instance
   hcomplex  :: {zero,one,plus,times,minus,power,inverse}
  
defs
  hcomplex_zero_def 
  "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
  
  hcomplex_one_def  
  "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"


  hcomplex_minus_def
  "- z == Abs_hcomplex(UN X: Rep_hcomplex(z). hcomplexrel `` {%n::nat. - (X n)})"

  hcomplex_diff_def
  "w - z == w + -(z::hcomplex)"
  
constdefs

  hcomplex_of_complex :: complex => hcomplex
  "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
 
  hcinv  :: hcomplex => hcomplex
  "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P). 
                    hcomplexrel `` {%n. inverse(X n)})"

  (*--- real and Imaginary parts ---*)
  
  hRe :: hcomplex => hypreal
  "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"

  hIm :: hcomplex => hypreal
  "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"   


  (*----------- modulus ------------*)

  hcmod :: hcomplex => hypreal
  "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
			  hyprel `` {%n. cmod (X n)})"

  (*------ imaginary unit ----------*)					 
			      
  iii :: hcomplex			      
  "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"

  (*------- complex conjugate ------*)

  hcnj :: hcomplex => hcomplex
  "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"

  (*------------ Argand -------------*)		       

  hsgn :: hcomplex => hcomplex
  "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"

  harg :: hcomplex => hypreal
  "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"

  (* abbreviation for (cos a + i sin a) *)
  hcis :: hypreal => hcomplex
  "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"

  (* abbreviation for r*(cos a + i sin a) *)
  hrcis :: [hypreal, hypreal] => hcomplex
  "hrcis r a == hcomplex_of_hypreal r * hcis a"

  (*----- injection from hyperreals -----*)			   
 
  hcomplex_of_hypreal :: hypreal => hcomplex
  "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
			       hcomplexrel `` {%n. complex_of_real (X n)})"

  (*------------ e ^ (x + iy) ------------*)

  hexpi :: hcomplex => hcomplex
  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
   

defs  


  (*----------- division ----------*)

  hcomplex_divide_def
  "w / (z::hcomplex) == w * inverse z"
    
  hcomplex_add_def
  "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
		      hcomplexrel `` {%n. X n + Y n})"

  hcomplex_mult_def
  "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
		      hcomplexrel `` {%n. X n * Y n})"    


primrec
     hcomplexpow_0   "z ^ 0       = 1"
     hcomplexpow_Suc "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"


consts
  "hcpow"  :: [hcomplex,hypnat] => hcomplex     (infixr 80)

defs
  (* hypernatural powers of nonstandard complex numbers *)
  hcpow_def
  "(z::hcomplex) hcpow (n::hypnat) 
      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
             hcomplexrel `` {%n. (X n) ^ (Y n)})"

end