1 (* Title: HOL/Real/Complex_Numbers.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer and Markus Wenzel, TU München |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 *) |
|
6 |
|
7 header {* Complex numbers *} |
|
8 |
|
9 theory Complex_Numbers = RealPow + Ring_and_Field: |
|
10 |
|
11 subsection {* Representation of complex numbers *} |
|
12 |
|
13 datatype complex = Complex real real |
|
14 |
|
15 consts Re :: "complex => real" |
|
16 primrec "Re (Complex x y) = x" |
|
17 |
|
18 consts Im :: "complex => real" |
|
19 primrec "Im (Complex x y) = y" |
|
20 |
|
21 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" |
|
22 by (induct z) simp |
|
23 |
|
24 instance complex :: zero .. |
|
25 instance complex :: one .. |
|
26 instance complex :: number .. |
|
27 instance complex :: plus .. |
|
28 instance complex :: minus .. |
|
29 instance complex :: times .. |
|
30 instance complex :: inverse .. |
|
31 |
|
32 defs (overloaded) |
|
33 zero_complex_def: "0 == Complex 0 0" |
|
34 one_complex_def: "1 == Complex 1 0" |
|
35 number_of_complex_def: "number_of b == Complex (number_of b) 0" |
|
36 add_complex_def: "z + w == Complex (Re z + Re w) (Im z + Im w)" |
|
37 minus_complex_def: "z - w == Complex (Re z - Re w) (Im z - Im w)" |
|
38 uminus_complex_def: "- z == Complex (- Re z) (- Im z)" |
|
39 mult_complex_def: "z * w == |
|
40 Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)" |
|
41 inverse_complex_def: "(z::complex) \<noteq> 0 ==> inverse z == |
|
42 Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) (- Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))" |
|
43 divide_complex_def: "(w::complex) \<noteq> 0 ==> z / (w::complex) == z * inverse w" |
|
44 |
|
45 lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w" |
|
46 by (induct z, induct w) simp |
|
47 |
|
48 lemma Re_zero [simp]: "Re 0 = 0" |
|
49 and Im_zero [simp]: "Im 0 = 0" |
|
50 by (simp_all add: zero_complex_def) |
|
51 |
|
52 lemma Re_one [simp]: "Re 1 = 1" |
|
53 and Im_one [simp]: "Im 1 = 0" |
|
54 by (simp_all add: one_complex_def) |
|
55 |
|
56 lemma Re_add [simp]: "Re (z + w) = Re z + Re w" |
|
57 by (simp add: add_complex_def) |
|
58 |
|
59 lemma Im_add [simp]: "Im (z + w) = Im z + Im w" |
|
60 by (simp add: add_complex_def) |
|
61 |
|
62 lemma Re_diff [simp]: "Re (z - w) = Re z - Re w" |
|
63 by (simp add: minus_complex_def) |
|
64 |
|
65 lemma Im_diff [simp]: "Im (z - w) = Im z - Im w" |
|
66 by (simp add: minus_complex_def) |
|
67 |
|
68 lemma Re_uminus [simp]: "Re (-z) = - Re z" |
|
69 by (simp add: uminus_complex_def) |
|
70 |
|
71 lemma Im_uminus [simp]: "Im (-z) = - Im z" |
|
72 by (simp add: uminus_complex_def) |
|
73 |
|
74 lemma Re_mult [simp]: "Re (z * w) = Re z * Re w - Im z * Im w" |
|
75 by (simp add: mult_complex_def) |
|
76 |
|
77 lemma Im_mult [simp]: "Im (z * w) = Re z * Im w + Im z * Re w" |
|
78 by (simp add: mult_complex_def) |
|
79 |
|
80 lemma zero_complex_iff: "(z = 0) = (Re z = 0 \<and> Im z = 0)" |
|
81 and one_complex_iff: "(z = 1) = (Re z = 1 \<and> Im z = 0)" |
|
82 by (auto simp add: complex_equality) |
|
83 |
|
84 |
|
85 subsection {* The field of complex numbers *} |
|
86 |
|
87 instance complex :: field |
|
88 proof |
|
89 fix z u v w :: complex |
|
90 show "(u + v) + w = u + (v + w)" |
|
91 by (simp add: add_complex_def) |
|
92 show "z + w = w + z" |
|
93 by (simp add: add_complex_def) |
|
94 show "0 + z = z" |
|
95 by (simp add: add_complex_def zero_complex_def) |
|
96 show "-z + z = 0" |
|
97 by (simp add: complex_equality minus_complex_def) |
|
98 show "z - w = z + -w" |
|
99 by (simp add: add_complex_def minus_complex_def uminus_complex_def) |
|
100 show "(u * v) * w = u * (v * w)" |
|
101 by (simp add: mult_complex_def mult_ac ring_distrib real_diff_def) (* FIXME *) |
|
102 show "z * w = w * z" |
|
103 by (simp add: mult_complex_def) |
|
104 show "1 * z = z" |
|
105 by (simp add: one_complex_def mult_complex_def) |
|
106 show "0 \<noteq> (1::complex)" --{*for some reason it has to be early*} |
|
107 by (simp add: zero_complex_def one_complex_def) |
|
108 show "(u + v) * w = u * w + v * w" |
|
109 by (simp add: add_complex_def mult_complex_def ring_distrib) |
|
110 show "z+u = z+v ==> u=v" |
|
111 proof - |
|
112 assume eq: "z+u = z+v" |
|
113 hence "(-z + z) + u = (-z + z) + v" by (simp add: eq add_complex_def) |
|
114 thus "u = v" by (simp add: add_complex_def) |
|
115 qed |
|
116 assume neq: "w \<noteq> 0" |
|
117 thus "z / w = z * inverse w" |
|
118 by (simp add: divide_complex_def) |
|
119 show "inverse w * w = 1" |
|
120 proof |
|
121 have neq': "Re w * Re w + Im w * Im w \<noteq> 0" |
|
122 proof - |
|
123 have ge: "0 \<le> Re w * Re w" "0 \<le> Im w * Im w" by simp_all |
|
124 from neq have "Re w \<noteq> 0 \<or> Im w \<noteq> 0" by (simp add: zero_complex_iff) |
|
125 hence "Re w * Re w \<noteq> 0 \<or> Im w * Im w \<noteq> 0" by simp |
|
126 thus ?thesis by rule (insert ge, arith+) |
|
127 qed |
|
128 with neq show "Re (inverse w * w) = Re 1" |
|
129 by (simp add: inverse_complex_def power2_eq_square add_divide_distrib [symmetric]) |
|
130 from neq show "Im (inverse w * w) = Im 1" |
|
131 by (simp add: inverse_complex_def power2_eq_square |
|
132 mult_ac add_divide_distrib [symmetric]) |
|
133 qed |
|
134 qed |
|
135 |
|
136 |
|
137 subsection {* Basic operations *} |
|
138 |
|
139 instance complex :: power .. |
|
140 primrec (power_complex) |
|
141 "z ^ 0 = 1" |
|
142 "z ^ Suc n = (z::complex) * (z ^ n)" |
|
143 |
|
144 lemma complex_power_two: "z\<twosuperior> = z * (z::complex)" |
|
145 by (simp add: complex_equality numeral_2_eq_2) |
|
146 |
|
147 |
|
148 constdefs |
|
149 im_unit :: complex ("\<i>") |
|
150 "\<i> == Complex 0 1" |
|
151 |
|
152 lemma im_unit_square: "\<i>\<twosuperior> = -1" |
|
153 by (simp add: im_unit_def complex_power_two mult_complex_def number_of_complex_def) |
|
154 |
|
155 |
|
156 constdefs |
|
157 conjg :: "complex => complex" |
|
158 "conjg z == Complex (Re z) (- Im z)" |
|
159 |
|
160 lemma Re_cong [simp]: "Re (conjg z) = Re z" |
|
161 by (simp add: conjg_def) |
|
162 |
|
163 lemma Im_cong [simp]: "Im (conjg z) = - Im z" |
|
164 by (simp add: conjg_def) |
|
165 |
|
166 lemma Re_conjg_self: "Re (z * conjg z) = (Re z)\<twosuperior> + (Im z)\<twosuperior>" |
|
167 by (simp add: power2_eq_square) |
|
168 |
|
169 lemma Im_conjg_self: "Im (z * conjg z) = 0" |
|
170 by simp |
|
171 |
|
172 |
|
173 subsection {* Embedding other number domains *} |
|
174 |
|
175 constdefs |
|
176 complex :: "'a => complex" |
|
177 "complex x == Complex (real x) 0"; |
|
178 |
|
179 lemma Re_complex [simp]: "Re (complex x) = real x" |
|
180 by (simp add: complex_def) |
|
181 |
|
182 end |
|