author | wenzelm |
Wed, 26 Oct 2016 15:14:17 +0200 | |
changeset 64406 | 492de9062cd2 |
parent 63589 | 58aab4745e85 |
child 64435 | c93b0e6131c3 |
permissions | -rw-r--r-- |
62479 | 1 |
(* Title: HOL/Nonstandard_Analysis/NSComplex.thy |
41959 | 2 |
Author: Jacques D. Fleuriot, University of Edinburgh |
3 |
Author: Lawrence C Paulson |
|
27468 | 4 |
*) |
5 |
||
61975 | 6 |
section\<open>Nonstandard Complex Numbers\<close> |
27468 | 7 |
|
8 |
theory NSComplex |
|
51525 | 9 |
imports NSA |
27468 | 10 |
begin |
11 |
||
42463 | 12 |
type_synonym hcomplex = "complex star" |
27468 | 13 |
|
14 |
abbreviation |
|
15 |
hcomplex_of_complex :: "complex => complex star" where |
|
16 |
"hcomplex_of_complex == star_of" |
|
17 |
||
18 |
abbreviation |
|
19 |
hcmod :: "complex star => real star" where |
|
20 |
"hcmod == hnorm" |
|
21 |
||
22 |
||
23 |
(*--- real and Imaginary parts ---*) |
|
24 |
||
25 |
definition |
|
26 |
hRe :: "hcomplex => hypreal" where |
|
37765 | 27 |
"hRe = *f* Re" |
27468 | 28 |
|
29 |
definition |
|
30 |
hIm :: "hcomplex => hypreal" where |
|
37765 | 31 |
"hIm = *f* Im" |
27468 | 32 |
|
33 |
||
34 |
(*------ imaginary unit ----------*) |
|
35 |
||
36 |
definition |
|
37 |
iii :: hcomplex where |
|
63589 | 38 |
"iii = star_of \<i>" |
27468 | 39 |
|
40 |
(*------- complex conjugate ------*) |
|
41 |
||
42 |
definition |
|
43 |
hcnj :: "hcomplex => hcomplex" where |
|
37765 | 44 |
"hcnj = *f* cnj" |
27468 | 45 |
|
46 |
(*------------ Argand -------------*) |
|
47 |
||
48 |
definition |
|
49 |
hsgn :: "hcomplex => hcomplex" where |
|
37765 | 50 |
"hsgn = *f* sgn" |
27468 | 51 |
|
52 |
definition |
|
53 |
harg :: "hcomplex => hypreal" where |
|
37765 | 54 |
"harg = *f* arg" |
27468 | 55 |
|
56 |
definition |
|
57 |
(* abbreviation for (cos a + i sin a) *) |
|
58 |
hcis :: "hypreal => hcomplex" where |
|
37765 | 59 |
"hcis = *f* cis" |
27468 | 60 |
|
61 |
(*----- injection from hyperreals -----*) |
|
62 |
||
63 |
abbreviation |
|
64 |
hcomplex_of_hypreal :: "hypreal \<Rightarrow> hcomplex" where |
|
65 |
"hcomplex_of_hypreal \<equiv> of_hypreal" |
|
66 |
||
67 |
definition |
|
68 |
(* abbreviation for r*(cos a + i sin a) *) |
|
69 |
hrcis :: "[hypreal, hypreal] => hcomplex" where |
|
37765 | 70 |
"hrcis = *f2* rcis" |
27468 | 71 |
|
72 |
(*------------ e ^ (x + iy) ------------*) |
|
73 |
definition |
|
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
74 |
hExp :: "hcomplex => hcomplex" where |
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
75 |
"hExp = *f* exp" |
27468 | 76 |
|
77 |
definition |
|
78 |
HComplex :: "[hypreal,hypreal] => hcomplex" where |
|
37765 | 79 |
"HComplex = *f2* Complex" |
27468 | 80 |
|
81 |
lemmas hcomplex_defs [transfer_unfold] = |
|
82 |
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
|
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
83 |
hrcis_def hExp_def HComplex_def |
27468 | 84 |
|
85 |
lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard" |
|
86 |
by (simp add: hcomplex_defs) |
|
87 |
||
88 |
lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard" |
|
89 |
by (simp add: hcomplex_defs) |
|
90 |
||
91 |
lemma Standard_iii [simp]: "iii \<in> Standard" |
|
92 |
by (simp add: hcomplex_defs) |
|
93 |
||
94 |
lemma Standard_hcnj [simp]: "x \<in> Standard \<Longrightarrow> hcnj x \<in> Standard" |
|
95 |
by (simp add: hcomplex_defs) |
|
96 |
||
97 |
lemma Standard_hsgn [simp]: "x \<in> Standard \<Longrightarrow> hsgn x \<in> Standard" |
|
98 |
by (simp add: hcomplex_defs) |
|
99 |
||
100 |
lemma Standard_harg [simp]: "x \<in> Standard \<Longrightarrow> harg x \<in> Standard" |
|
101 |
by (simp add: hcomplex_defs) |
|
102 |
||
103 |
lemma Standard_hcis [simp]: "r \<in> Standard \<Longrightarrow> hcis r \<in> Standard" |
|
104 |
by (simp add: hcomplex_defs) |
|
105 |
||
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
106 |
lemma Standard_hExp [simp]: "x \<in> Standard \<Longrightarrow> hExp x \<in> Standard" |
27468 | 107 |
by (simp add: hcomplex_defs) |
108 |
||
109 |
lemma Standard_hrcis [simp]: |
|
110 |
"\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> hrcis r s \<in> Standard" |
|
111 |
by (simp add: hcomplex_defs) |
|
112 |
||
113 |
lemma Standard_HComplex [simp]: |
|
114 |
"\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard" |
|
115 |
by (simp add: hcomplex_defs) |
|
116 |
||
117 |
lemma hcmod_def: "hcmod = *f* cmod" |
|
118 |
by (rule hnorm_def) |
|
119 |
||
120 |
||
61975 | 121 |
subsection\<open>Properties of Nonstandard Real and Imaginary Parts\<close> |
27468 | 122 |
|
123 |
lemma hcomplex_hRe_hIm_cancel_iff: |
|
124 |
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
|
125 |
by transfer (rule complex_Re_Im_cancel_iff) |
|
126 |
||
127 |
lemma hcomplex_equality [intro?]: |
|
128 |
"!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w" |
|
129 |
by transfer (rule complex_equality) |
|
130 |
||
131 |
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
132 |
by transfer simp |
27468 | 133 |
|
134 |
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
135 |
by transfer simp |
27468 | 136 |
|
137 |
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
138 |
by transfer simp |
27468 | 139 |
|
140 |
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
141 |
by transfer simp |
27468 | 142 |
|
143 |
||
61975 | 144 |
subsection\<open>Addition for Nonstandard Complex Numbers\<close> |
27468 | 145 |
|
146 |
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
147 |
by transfer simp |
27468 | 148 |
|
149 |
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
150 |
by transfer simp |
27468 | 151 |
|
61975 | 152 |
subsection\<open>More Minus Laws\<close> |
27468 | 153 |
|
154 |
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
155 |
by transfer (rule uminus_complex.sel) |
27468 | 156 |
|
157 |
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
158 |
by transfer (rule uminus_complex.sel) |
27468 | 159 |
|
160 |
lemma hcomplex_add_minus_eq_minus: |
|
161 |
"x + y = (0::hcomplex) ==> x = -y" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34146
diff
changeset
|
162 |
apply (drule minus_unique) |
27468 | 163 |
apply (simp add: minus_equation_iff [of x y]) |
164 |
done |
|
165 |
||
44764
264436dd9491
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
huffman
parents:
44711
diff
changeset
|
166 |
lemma hcomplex_i_mult_eq [simp]: "iii * iii = -1" |
264436dd9491
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
huffman
parents:
44711
diff
changeset
|
167 |
by transfer (rule i_squared) |
27468 | 168 |
|
169 |
lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z" |
|
170 |
by transfer (rule complex_i_mult_minus) |
|
171 |
||
172 |
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0" |
|
173 |
by transfer (rule complex_i_not_zero) |
|
174 |
||
175 |
||
61975 | 176 |
subsection\<open>More Multiplication Laws\<close> |
27468 | 177 |
|
178 |
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z" |
|
179 |
by simp |
|
180 |
||
181 |
lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z" |
|
182 |
by simp |
|
183 |
||
184 |
lemma hcomplex_mult_left_cancel: |
|
185 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)" |
|
186 |
by simp |
|
187 |
||
188 |
lemma hcomplex_mult_right_cancel: |
|
189 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)" |
|
190 |
by simp |
|
191 |
||
192 |
||
61975 | 193 |
subsection\<open>Subraction and Division\<close> |
27468 | 194 |
|
195 |
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" |
|
196 |
(* TODO: delete *) |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34146
diff
changeset
|
197 |
by (rule diff_eq_eq) |
27468 | 198 |
|
199 |
||
61975 | 200 |
subsection\<open>Embedding Properties for @{term hcomplex_of_hypreal} Map\<close> |
27468 | 201 |
|
202 |
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z" |
|
203 |
by transfer (rule Re_complex_of_real) |
|
204 |
||
205 |
lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
|
206 |
by transfer (rule Im_complex_of_real) |
|
207 |
||
208 |
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
|
61981 | 209 |
"hcomplex_of_hypreal \<epsilon> \<noteq> 0" |
27468 | 210 |
by (simp add: hypreal_epsilon_not_zero) |
211 |
||
61975 | 212 |
subsection\<open>HComplex theorems\<close> |
27468 | 213 |
|
214 |
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
215 |
by transfer simp |
27468 | 216 |
|
217 |
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
218 |
by transfer simp |
27468 | 219 |
|
220 |
lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" |
|
221 |
by transfer (rule complex_surj) |
|
222 |
||
223 |
lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: |
|
224 |
"(\<And>x y. P (HComplex x y)) ==> P z" |
|
225 |
by (rule hcomplex_surj [THEN subst], blast) |
|
226 |
||
227 |
||
61975 | 228 |
subsection\<open>Modulus (Absolute Value) of Nonstandard Complex Number\<close> |
27468 | 229 |
|
230 |
lemma hcomplex_of_hypreal_abs: |
|
61945 | 231 |
"hcomplex_of_hypreal \<bar>x\<bar> = |
232 |
hcomplex_of_hypreal (hcmod (hcomplex_of_hypreal x))" |
|
27468 | 233 |
by simp |
234 |
||
235 |
lemma HComplex_inject [simp]: |
|
236 |
"!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')" |
|
237 |
by transfer (rule complex.inject) |
|
238 |
||
239 |
lemma HComplex_add [simp]: |
|
240 |
"!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)" |
|
241 |
by transfer (rule complex_add) |
|
242 |
||
243 |
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)" |
|
244 |
by transfer (rule complex_minus) |
|
245 |
||
246 |
lemma HComplex_diff [simp]: |
|
247 |
"!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)" |
|
248 |
by transfer (rule complex_diff) |
|
249 |
||
250 |
lemma HComplex_mult [simp]: |
|
251 |
"!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 = |
|
252 |
HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)" |
|
253 |
by transfer (rule complex_mult) |
|
254 |
||
255 |
(*HComplex_inverse is proved below*) |
|
256 |
||
257 |
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0" |
|
258 |
by transfer (rule complex_of_real_def) |
|
259 |
||
260 |
lemma HComplex_add_hcomplex_of_hypreal [simp]: |
|
261 |
"!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y" |
|
262 |
by transfer (rule Complex_add_complex_of_real) |
|
263 |
||
264 |
lemma hcomplex_of_hypreal_add_HComplex [simp]: |
|
265 |
"!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y" |
|
266 |
by transfer (rule complex_of_real_add_Complex) |
|
267 |
||
268 |
lemma HComplex_mult_hcomplex_of_hypreal: |
|
269 |
"!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)" |
|
270 |
by transfer (rule Complex_mult_complex_of_real) |
|
271 |
||
272 |
lemma hcomplex_of_hypreal_mult_HComplex: |
|
273 |
"!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)" |
|
274 |
by transfer (rule complex_of_real_mult_Complex) |
|
275 |
||
276 |
lemma i_hcomplex_of_hypreal [simp]: |
|
277 |
"!!r. iii * hcomplex_of_hypreal r = HComplex 0 r" |
|
278 |
by transfer (rule i_complex_of_real) |
|
279 |
||
280 |
lemma hcomplex_of_hypreal_i [simp]: |
|
281 |
"!!r. hcomplex_of_hypreal r * iii = HComplex 0 r" |
|
282 |
by transfer (rule complex_of_real_i) |
|
283 |
||
284 |
||
61975 | 285 |
subsection\<open>Conjugation\<close> |
27468 | 286 |
|
287 |
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" |
|
288 |
by transfer (rule complex_cnj_cancel_iff) |
|
289 |
||
290 |
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z" |
|
291 |
by transfer (rule complex_cnj_cnj) |
|
292 |
||
293 |
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]: |
|
294 |
"!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" |
|
295 |
by transfer (rule complex_cnj_complex_of_real) |
|
296 |
||
297 |
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z" |
|
298 |
by transfer (rule complex_mod_cnj) |
|
299 |
||
300 |
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z" |
|
301 |
by transfer (rule complex_cnj_minus) |
|
302 |
||
303 |
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)" |
|
304 |
by transfer (rule complex_cnj_inverse) |
|
305 |
||
306 |
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)" |
|
307 |
by transfer (rule complex_cnj_add) |
|
308 |
||
309 |
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)" |
|
310 |
by transfer (rule complex_cnj_diff) |
|
311 |
||
312 |
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)" |
|
313 |
by transfer (rule complex_cnj_mult) |
|
314 |
||
315 |
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)" |
|
316 |
by transfer (rule complex_cnj_divide) |
|
317 |
||
318 |
lemma hcnj_one [simp]: "hcnj 1 = 1" |
|
319 |
by transfer (rule complex_cnj_one) |
|
320 |
||
321 |
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" |
|
322 |
by transfer (rule complex_cnj_zero) |
|
323 |
||
324 |
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)" |
|
325 |
by transfer (rule complex_cnj_zero_iff) |
|
326 |
||
327 |
lemma hcomplex_mult_hcnj: |
|
53077 | 328 |
"!!z. z * hcnj z = hcomplex_of_hypreal ((hRe z)\<^sup>2 + (hIm z)\<^sup>2)" |
27468 | 329 |
by transfer (rule complex_mult_cnj) |
330 |
||
331 |
||
61975 | 332 |
subsection\<open>More Theorems about the Function @{term hcmod}\<close> |
27468 | 333 |
|
334 |
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: |
|
335 |
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" |
|
336 |
by simp |
|
337 |
||
338 |
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]: |
|
339 |
"hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" |
|
340 |
by simp |
|
341 |
||
53077 | 342 |
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = (hcmod z)\<^sup>2" |
27468 | 343 |
by transfer (rule complex_mod_mult_cnj) |
344 |
||
345 |
lemma hcmod_triangle_ineq2 [simp]: |
|
346 |
"!!a b. hcmod(b + a) - hcmod b \<le> hcmod a" |
|
347 |
by transfer (rule complex_mod_triangle_ineq2) |
|
348 |
||
349 |
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
|
350 |
by transfer (rule norm_diff_ineq) |
|
351 |
||
352 |
||
61975 | 353 |
subsection\<open>Exponentiation\<close> |
27468 | 354 |
|
355 |
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)" |
|
356 |
by (rule power_0) |
|
357 |
||
358 |
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" |
|
359 |
by (rule power_Suc) |
|
360 |
||
53077 | 361 |
lemma hcomplexpow_i_squared [simp]: "iii\<^sup>2 = -1" |
27468 | 362 |
by transfer (rule power2_i) |
363 |
||
364 |
lemma hcomplex_of_hypreal_pow: |
|
365 |
"!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n" |
|
366 |
by transfer (rule of_real_power) |
|
367 |
||
368 |
lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n" |
|
369 |
by transfer (rule complex_cnj_power) |
|
370 |
||
371 |
lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n" |
|
372 |
by transfer (rule norm_power) |
|
373 |
||
374 |
lemma hcpow_minus: |
|
375 |
"!!x n. (-x::hcomplex) pow n = |
|
376 |
(if ( *p* even) n then (x pow n) else -(x pow n))" |
|
58787 | 377 |
by transfer simp |
27468 | 378 |
|
379 |
lemma hcpow_mult: |
|
60867 | 380 |
"((r::hcomplex) * s) pow n = (r pow n) * (s pow n)" |
58787 | 381 |
by (fact hyperpow_mult) |
27468 | 382 |
|
383 |
lemma hcpow_zero2 [simp]: |
|
60867 | 384 |
"\<And>n. 0 pow (hSuc n) = (0::'a::semiring_1 star)" |
385 |
by transfer (rule power_0_Suc) |
|
27468 | 386 |
|
387 |
lemma hcpow_not_zero [simp,intro]: |
|
388 |
"!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)" |
|
60867 | 389 |
by (fact hyperpow_not_zero) |
27468 | 390 |
|
60867 | 391 |
lemma hcpow_zero_zero: |
392 |
"r pow n = (0::hcomplex) ==> r = 0" |
|
393 |
by (blast intro: ccontr dest: hcpow_not_zero) |
|
27468 | 394 |
|
61975 | 395 |
subsection\<open>The Function @{term hsgn}\<close> |
27468 | 396 |
|
397 |
lemma hsgn_zero [simp]: "hsgn 0 = 0" |
|
398 |
by transfer (rule sgn_zero) |
|
399 |
||
400 |
lemma hsgn_one [simp]: "hsgn 1 = 1" |
|
401 |
by transfer (rule sgn_one) |
|
402 |
||
403 |
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)" |
|
404 |
by transfer (rule sgn_minus) |
|
405 |
||
406 |
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
|
407 |
by transfer (rule sgn_eq) |
|
408 |
||
53077 | 409 |
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x\<^sup>2 + y\<^sup>2)" |
27468 | 410 |
by transfer (rule complex_norm) |
411 |
||
412 |
lemma hcomplex_eq_cancel_iff1 [simp]: |
|
413 |
"(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)" |
|
414 |
by (simp add: hcomplex_of_hypreal_eq) |
|
415 |
||
416 |
lemma hcomplex_eq_cancel_iff2 [simp]: |
|
417 |
"(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
|
418 |
by (simp add: hcomplex_of_hypreal_eq) |
|
419 |
||
420 |
lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)" |
|
421 |
by transfer (rule Complex_eq_0) |
|
422 |
||
423 |
lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)" |
|
424 |
by transfer (rule Complex_eq_1) |
|
425 |
||
426 |
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
427 |
by transfer (simp add: complex_eq_iff) |
27468 | 428 |
|
429 |
lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)" |
|
430 |
by transfer (rule Complex_eq_i) |
|
431 |
||
432 |
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z" |
|
433 |
by transfer (rule Re_sgn) |
|
434 |
||
435 |
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z" |
|
436 |
by transfer (rule Im_sgn) |
|
437 |
||
438 |
lemma HComplex_inverse: |
|
53077 | 439 |
"!!x y. inverse (HComplex x y) = HComplex (x/(x\<^sup>2 + y\<^sup>2)) (-y/(x\<^sup>2 + y\<^sup>2))" |
27468 | 440 |
by transfer (rule complex_inverse) |
441 |
||
442 |
lemma hRe_mult_i_eq[simp]: |
|
443 |
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0" |
|
444 |
by transfer simp |
|
445 |
||
446 |
lemma hIm_mult_i_eq [simp]: |
|
447 |
"!!y. hIm (iii * hcomplex_of_hypreal y) = y" |
|
448 |
by transfer simp |
|
449 |
||
61945 | 450 |
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = \<bar>y\<bar>" |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
451 |
by transfer (simp add: norm_complex_def) |
27468 | 452 |
|
61945 | 453 |
lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = \<bar>y\<bar>" |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
454 |
by transfer (simp add: norm_complex_def) |
27468 | 455 |
|
456 |
(*---------------------------------------------------------------------------*) |
|
457 |
(* harg *) |
|
458 |
(*---------------------------------------------------------------------------*) |
|
459 |
||
460 |
lemma cos_harg_i_mult_zero [simp]: |
|
461 |
"!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
462 |
by transfer simp |
27468 | 463 |
|
464 |
lemma hcomplex_of_hypreal_zero_iff [simp]: |
|
465 |
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)" |
|
466 |
by transfer (rule of_real_eq_0_iff) |
|
467 |
||
468 |
||
61975 | 469 |
subsection\<open>Polar Form for Nonstandard Complex Numbers\<close> |
27468 | 470 |
|
471 |
lemma complex_split_polar2: |
|
472 |
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
473 |
by (auto intro: complex_split_polar) |
27468 | 474 |
|
475 |
lemma hcomplex_split_polar: |
|
476 |
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
477 |
by transfer (simp add: complex_split_polar) |
27468 | 478 |
|
479 |
lemma hcis_eq: |
|
480 |
"!!a. hcis a = |
|
481 |
(hcomplex_of_hypreal(( *f* cos) a) + |
|
482 |
iii * hcomplex_of_hypreal(( *f* sin) a))" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
483 |
by transfer (simp add: complex_eq_iff) |
27468 | 484 |
|
485 |
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
|
486 |
by transfer (rule rcis_Ex) |
|
487 |
||
488 |
lemma hRe_hcomplex_polar [simp]: |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
489 |
"!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
27468 | 490 |
r * ( *f* cos) a" |
491 |
by transfer simp |
|
492 |
||
493 |
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a" |
|
494 |
by transfer (rule Re_rcis) |
|
495 |
||
496 |
lemma hIm_hcomplex_polar [simp]: |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
497 |
"!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = |
27468 | 498 |
r * ( *f* sin) a" |
499 |
by transfer simp |
|
500 |
||
501 |
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a" |
|
502 |
by transfer (rule Im_rcis) |
|
503 |
||
504 |
lemma hcmod_unit_one [simp]: |
|
505 |
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
506 |
by transfer (simp add: cmod_unit_one) |
27468 | 507 |
|
508 |
lemma hcmod_complex_polar [simp]: |
|
61945 | 509 |
"!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>" |
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
510 |
by transfer (simp add: cmod_complex_polar) |
27468 | 511 |
|
61945 | 512 |
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = \<bar>r\<bar>" |
27468 | 513 |
by transfer (rule complex_mod_rcis) |
514 |
||
515 |
(*---------------------------------------------------------------------------*) |
|
516 |
(* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
|
517 |
(*---------------------------------------------------------------------------*) |
|
518 |
||
519 |
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a" |
|
520 |
by transfer (rule cis_rcis_eq) |
|
521 |
declare hcis_hrcis_eq [symmetric, simp] |
|
522 |
||
523 |
lemma hrcis_mult: |
|
524 |
"!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
|
525 |
by transfer (rule rcis_mult) |
|
526 |
||
527 |
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)" |
|
528 |
by transfer (rule cis_mult) |
|
529 |
||
530 |
lemma hcis_zero [simp]: "hcis 0 = 1" |
|
531 |
by transfer (rule cis_zero) |
|
532 |
||
533 |
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0" |
|
534 |
by transfer (rule rcis_zero_mod) |
|
535 |
||
536 |
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r" |
|
537 |
by transfer (rule rcis_zero_arg) |
|
538 |
||
539 |
lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x" |
|
540 |
by transfer (rule complex_i_mult_minus) |
|
541 |
||
542 |
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
|
543 |
by simp |
|
544 |
||
545 |
lemma hcis_hypreal_of_nat_Suc_mult: |
|
546 |
"!!a. hcis (hypreal_of_nat (Suc n) * a) = |
|
547 |
hcis a * hcis (hypreal_of_nat n * a)" |
|
548 |
apply transfer |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47108
diff
changeset
|
549 |
apply (simp add: distrib_right cis_mult) |
27468 | 550 |
done |
551 |
||
552 |
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
|
553 |
apply transfer |
|
554 |
apply (rule DeMoivre) |
|
555 |
done |
|
556 |
||
557 |
lemma hcis_hypreal_of_hypnat_Suc_mult: |
|
558 |
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = |
|
559 |
hcis a * hcis (hypreal_of_hypnat n * a)" |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47108
diff
changeset
|
560 |
by transfer (simp add: distrib_right cis_mult) |
27468 | 561 |
|
562 |
lemma NSDeMoivre_ext: |
|
563 |
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
564 |
by transfer (rule DeMoivre) |
27468 | 565 |
|
566 |
lemma NSDeMoivre2: |
|
567 |
"!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
568 |
by transfer (rule DeMoivre2) |
27468 | 569 |
|
570 |
lemma DeMoivre2_ext: |
|
571 |
"!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
572 |
by transfer (rule DeMoivre2) |
27468 | 573 |
|
574 |
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)" |
|
575 |
by transfer (rule cis_inverse) |
|
576 |
||
577 |
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)" |
|
578 |
by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric]) |
|
579 |
||
580 |
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
581 |
by transfer simp |
27468 | 582 |
|
583 |
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" |
|
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
54489
diff
changeset
|
584 |
by transfer simp |
27468 | 585 |
|
586 |
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
|
587 |
by (simp add: NSDeMoivre) |
|
588 |
||
589 |
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
|
590 |
by (simp add: NSDeMoivre) |
|
591 |
||
592 |
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)" |
|
593 |
by (simp add: NSDeMoivre_ext) |
|
594 |
||
595 |
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)" |
|
596 |
by (simp add: NSDeMoivre_ext) |
|
597 |
||
59658
0cc388370041
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
paulson <lp15@cam.ac.uk>
parents:
58878
diff
changeset
|
598 |
lemma hExp_add: "!!a b. hExp(a + b) = hExp(a) * hExp(b)" |
44711 | 599 |
by transfer (rule exp_add) |
27468 | 600 |
|
601 |
||
61975 | 602 |
subsection\<open>@{term hcomplex_of_complex}: the Injection from |
603 |
type @{typ complex} to to @{typ hcomplex}\<close> |
|
27468 | 604 |
|
63589 | 605 |
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex \<i>" |
27468 | 606 |
by (rule iii_def) |
607 |
||
608 |
lemma hRe_hcomplex_of_complex: |
|
609 |
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
|
610 |
by transfer (rule refl) |
|
611 |
||
612 |
lemma hIm_hcomplex_of_complex: |
|
613 |
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
|
614 |
by transfer (rule refl) |
|
615 |
||
616 |
lemma hcmod_hcomplex_of_complex: |
|
617 |
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
|
618 |
by transfer (rule refl) |
|
619 |
||
620 |
||
61975 | 621 |
subsection\<open>Numerals and Arithmetic\<close> |
27468 | 622 |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
623 |
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
624 |
"hcomplex_of_hypreal (hypreal_of_real x) = |
27468 | 625 |
hcomplex_of_complex (complex_of_real x)" |
626 |
by transfer (rule refl) |
|
627 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
628 |
lemma hcomplex_hypreal_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
629 |
"hcomplex_of_complex (numeral w) = hcomplex_of_hypreal(numeral w)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
630 |
by transfer (rule of_real_numeral [symmetric]) |
27468 | 631 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
632 |
lemma hcomplex_hypreal_neg_numeral: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53077
diff
changeset
|
633 |
"hcomplex_of_complex (- numeral w) = hcomplex_of_hypreal(- numeral w)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
634 |
by transfer (rule of_real_neg_numeral [symmetric]) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
635 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
636 |
lemma hcomplex_numeral_hcnj [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
637 |
"hcnj (numeral v :: hcomplex) = numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
638 |
by transfer (rule complex_cnj_numeral) |
27468 | 639 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
640 |
lemma hcomplex_numeral_hcmod [simp]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
641 |
"hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
642 |
by transfer (rule norm_numeral) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
643 |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
644 |
lemma hcomplex_neg_numeral_hcmod [simp]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53077
diff
changeset
|
645 |
"hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
646 |
by transfer (rule norm_neg_numeral) |
27468 | 647 |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
648 |
lemma hcomplex_numeral_hRe [simp]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
649 |
"hRe(numeral v :: hcomplex) = numeral v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
650 |
by transfer (rule complex_Re_numeral) |
27468 | 651 |
|
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
59730
diff
changeset
|
652 |
lemma hcomplex_numeral_hIm [simp]: |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
653 |
"hIm(numeral v :: hcomplex) = 0" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44846
diff
changeset
|
654 |
by transfer (rule complex_Im_numeral) |
27468 | 655 |
|
656 |
end |