|
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 |
|