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