13957

1 
(* Title: Complex.thy


2 
Author: Jacques D. Fleuriot


3 
Copyright: 2001 University of Edinburgh


4 
Description: Complex numbers


5 
*)


6 


7 
Complex = HLog +


8 


9 
typedef complex = "{p::(real*real). True}"


10 


11 
instance


12 
complex :: {ord,zero,one,plus,minus,times,power,inverse}


13 


14 
consts


15 
"ii" :: complex ("ii")


16 


17 
constdefs


18 


19 
(* real and Imaginary parts *)


20 


21 
Re :: complex => real


22 
"Re(z) == fst(Rep_complex z)"


23 


24 
Im :: complex => real


25 
"Im(z) == snd(Rep_complex z)"


26 


27 
(* modulus *)


28 


29 
cmod :: complex => real


30 
"cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"


31 


32 
(* injection from reals *)


33 


34 
complex_of_real :: real => complex


35 
"complex_of_real r == Abs_complex(r,0::real)"


36 


37 
(* complex conjugate *)


38 


39 
cnj :: complex => complex


40 
"cnj z == Abs_complex(Re z, Im z)"


41 


42 
(* Argand *)


43 


44 
sgn :: complex => complex


45 
"sgn z == z / complex_of_real(cmod z)"


46 


47 
arg :: complex => real


48 
"arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & pi < a & a <= pi"


49 


50 
defs


51 


52 
complex_zero_def


53 
"0 == Abs_complex(0::real,0)"


54 


55 
complex_one_def


56 
"1 == Abs_complex(1,0::real)"


57 


58 
(* imaginary unit *)


59 


60 
i_def


61 
"ii == Abs_complex(0::real,1)"


62 


63 
(* negation *)


64 


65 
complex_minus_def


66 
" (z::complex) == Abs_complex(Re z, Im z)"


67 


68 


69 
(* inverse *)


70 
complex_inverse_def


71 
"inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2),


72 
Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))"


73 


74 
complex_add_def


75 
"w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))"


76 


77 
complex_diff_def


78 
"w  (z::complex) == w + (z::complex)"


79 


80 
complex_mult_def


81 
"w * (z::complex) == Abs_complex(Re(w) * Re(z)  Im(w) * Im(z),


82 
Re(w) * Im(z) + Im(w) * Re(z))"


83 


84 


85 
(* division *)


86 
complex_divide_def


87 
"w / (z::complex) == w * inverse z"


88 


89 


90 
primrec


91 
complexpow_0 "z ^ 0 = complex_of_real 1"


92 
complexpow_Suc "z ^ (Suc n) = (z::complex) * (z ^ n)"


93 


94 


95 
constdefs


96 


97 
(* abbreviation for (cos a + i sin a) *)


98 
cis :: real => complex


99 
"cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"


100 


101 
(* abbreviation for r*(cos a + i sin a) *)


102 
rcis :: [real, real] => complex


103 
"rcis r a == complex_of_real r * cis a"


104 


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


106 
expi :: complex => complex


107 
"expi z == complex_of_real(exp (Re z)) * cis (Im z)"


108 


109 
end


110 


111 
