src/HOL/NSA/NSComplex.thy
author paulson <lp15@cam.ac.uk>
Sat Apr 11 11:56:40 2015 +0100 (2015-04-11)
changeset 60017 b785d6d06430
parent 59730 b7c394c7a619
child 60867 86e7560e07d0
permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
     1 (*  Title:      HOL/NSA/NSComplex.thy
     2     Author:     Jacques D. Fleuriot, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4 *)
     5 
     6 section{*Nonstandard Complex Numbers*}
     7 
     8 theory NSComplex
     9 imports NSA
    10 begin
    11 
    12 type_synonym hcomplex = "complex star"
    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
    27   "hRe = *f* Re"
    28 
    29 definition
    30   hIm :: "hcomplex => hypreal" where
    31   "hIm = *f* Im"
    32 
    33 
    34   (*------ imaginary unit ----------*)
    35 
    36 definition
    37   iii :: hcomplex where
    38   "iii = star_of ii"
    39 
    40   (*------- complex conjugate ------*)
    41 
    42 definition
    43   hcnj :: "hcomplex => hcomplex" where
    44   "hcnj = *f* cnj"
    45 
    46   (*------------ Argand -------------*)
    47 
    48 definition
    49   hsgn :: "hcomplex => hcomplex" where
    50   "hsgn = *f* sgn"
    51 
    52 definition
    53   harg :: "hcomplex => hypreal" where
    54   "harg = *f* arg"
    55 
    56 definition
    57   (* abbreviation for (cos a + i sin a) *)
    58   hcis :: "hypreal => hcomplex" where
    59   "hcis = *f* cis"
    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
    70   "hrcis = *f2* rcis"
    71 
    72   (*------------ e ^ (x + iy) ------------*)
    73 definition
    74   hExp :: "hcomplex => hcomplex" where
    75   "hExp = *f* exp"
    76 
    77 definition
    78   HComplex :: "[hypreal,hypreal] => hcomplex" where
    79   "HComplex = *f2* Complex"
    80 
    81 lemmas hcomplex_defs [transfer_unfold] =
    82   hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
    83   hrcis_def hExp_def HComplex_def
    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 
   106 lemma Standard_hExp [simp]: "x \<in> Standard \<Longrightarrow> hExp x \<in> Standard"
   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 
   121 subsection{*Properties of Nonstandard Real and Imaginary Parts*}
   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"
   132 by transfer simp
   133 
   134 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
   135 by transfer simp
   136 
   137 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
   138 by transfer simp
   139 
   140 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
   141 by transfer simp
   142 
   143 
   144 subsection{*Addition for Nonstandard Complex Numbers*}
   145 
   146 lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
   147 by transfer simp
   148 
   149 lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
   150 by transfer simp
   151 
   152 subsection{*More Minus Laws*}
   153 
   154 lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
   155 by transfer (rule uminus_complex.sel)
   156 
   157 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
   158 by transfer (rule uminus_complex.sel)
   159 
   160 lemma hcomplex_add_minus_eq_minus:
   161       "x + y = (0::hcomplex) ==> x = -y"
   162 apply (drule minus_unique)
   163 apply (simp add: minus_equation_iff [of x y])
   164 done
   165 
   166 lemma hcomplex_i_mult_eq [simp]: "iii * iii = -1"
   167 by transfer (rule i_squared)
   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 
   176 subsection{*More Multiplication Laws*}
   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 
   193 subsection{*Subraction and Division*}
   194 
   195 lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
   196 (* TODO: delete *)
   197 by (rule diff_eq_eq)
   198 
   199 
   200 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
   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]:
   209      "hcomplex_of_hypreal epsilon \<noteq> 0"
   210 by (simp add: hypreal_epsilon_not_zero)
   211 
   212 subsection{*HComplex theorems*}
   213 
   214 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
   215 by transfer simp
   216 
   217 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
   218 by transfer simp
   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 
   228 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   229 
   230 lemma hcomplex_of_hypreal_abs:
   231      "hcomplex_of_hypreal (abs x) =
   232       hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   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 
   285 subsection{*Conjugation*}
   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:
   328      "!!z. z * hcnj z = hcomplex_of_hypreal ((hRe z)\<^sup>2 + (hIm z)\<^sup>2)"
   329 by transfer (rule complex_mult_cnj)
   330 
   331 
   332 subsection{*More Theorems about the Function @{term hcmod}*}
   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 
   342 lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = (hcmod z)\<^sup>2"
   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 
   353 subsection{*Exponentiation*}
   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 
   361 lemma hcomplexpow_i_squared [simp]: "iii\<^sup>2 = -1"
   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))"
   377 by transfer simp
   378 
   379 lemma hcpow_mult:
   380   "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
   381   by (fact hyperpow_mult)
   382 
   383 lemma hcpow_zero2 [simp]:
   384   "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
   385 by transfer (rule power_0_Suc)
   386 
   387 lemma hcpow_not_zero [simp,intro]:
   388   "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
   389 by (rule hyperpow_not_zero)
   390 
   391 lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
   392 by (blast intro: ccontr dest: hcpow_not_zero)
   393 
   394 subsection{*The Function @{term hsgn}*}
   395 
   396 lemma hsgn_zero [simp]: "hsgn 0 = 0"
   397 by transfer (rule sgn_zero)
   398 
   399 lemma hsgn_one [simp]: "hsgn 1 = 1"
   400 by transfer (rule sgn_one)
   401 
   402 lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)"
   403 by transfer (rule sgn_minus)
   404 
   405 lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
   406 by transfer (rule sgn_eq)
   407 
   408 lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x\<^sup>2 + y\<^sup>2)"
   409 by transfer (rule complex_norm)
   410 
   411 lemma hcomplex_eq_cancel_iff1 [simp]:
   412      "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
   413 by (simp add: hcomplex_of_hypreal_eq)
   414 
   415 lemma hcomplex_eq_cancel_iff2 [simp]:
   416      "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   417 by (simp add: hcomplex_of_hypreal_eq)
   418 
   419 lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)"
   420 by transfer (rule Complex_eq_0)
   421 
   422 lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)"
   423 by transfer (rule Complex_eq_1)
   424 
   425 lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
   426 by transfer (simp add: complex_eq_iff)
   427 
   428 lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)"
   429 by transfer (rule Complex_eq_i)
   430 
   431 lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z"
   432 by transfer (rule Re_sgn)
   433 
   434 lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
   435 by transfer (rule Im_sgn)
   436 
   437 lemma HComplex_inverse:
   438      "!!x y. inverse (HComplex x y) = HComplex (x/(x\<^sup>2 + y\<^sup>2)) (-y/(x\<^sup>2 + y\<^sup>2))"
   439 by transfer (rule complex_inverse)
   440 
   441 lemma hRe_mult_i_eq[simp]:
   442     "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
   443 by transfer simp
   444 
   445 lemma hIm_mult_i_eq [simp]:
   446     "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
   447 by transfer simp
   448 
   449 lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
   450 by transfer (simp add: norm_complex_def)
   451 
   452 lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
   453 by transfer (simp add: norm_complex_def)
   454 
   455 (*---------------------------------------------------------------------------*)
   456 (*  harg                                                                     *)
   457 (*---------------------------------------------------------------------------*)
   458 
   459 lemma cos_harg_i_mult_zero [simp]:
   460      "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   461 by transfer simp
   462 
   463 lemma hcomplex_of_hypreal_zero_iff [simp]:
   464      "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
   465 by transfer (rule of_real_eq_0_iff)
   466 
   467 
   468 subsection{*Polar Form for Nonstandard Complex Numbers*}
   469 
   470 lemma complex_split_polar2:
   471      "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
   472 by (auto intro: complex_split_polar)
   473 
   474 lemma hcomplex_split_polar:
   475   "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   476 by transfer (simp add: complex_split_polar)
   477 
   478 lemma hcis_eq:
   479    "!!a. hcis a =
   480     (hcomplex_of_hypreal(( *f* cos) a) +
   481     iii * hcomplex_of_hypreal(( *f* sin) a))"
   482 by transfer (simp add: complex_eq_iff)
   483 
   484 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
   485 by transfer (rule rcis_Ex)
   486 
   487 lemma hRe_hcomplex_polar [simp]:
   488   "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   489       r * ( *f* cos) a"
   490 by transfer simp
   491 
   492 lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a"
   493 by transfer (rule Re_rcis)
   494 
   495 lemma hIm_hcomplex_polar [simp]:
   496   "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   497       r * ( *f* sin) a"
   498 by transfer simp
   499 
   500 lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a"
   501 by transfer (rule Im_rcis)
   502 
   503 lemma hcmod_unit_one [simp]:
   504      "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
   505 by transfer (simp add: cmod_unit_one)
   506 
   507 lemma hcmod_complex_polar [simp]:
   508   "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   509       abs r"
   510 by transfer (simp add: cmod_complex_polar)
   511 
   512 lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
   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
   549 apply (simp add: distrib_right cis_mult)
   550 done
   551 
   552 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
   553 apply transfer
   554 apply (fold real_of_nat_def)
   555 apply (rule DeMoivre)
   556 done
   557 
   558 lemma hcis_hypreal_of_hypnat_Suc_mult:
   559      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
   560       hcis a * hcis (hypreal_of_hypnat n * a)"
   561 by transfer (simp add: distrib_right cis_mult)
   562 
   563 lemma NSDeMoivre_ext:
   564   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
   565 by transfer (fold real_of_nat_def, rule DeMoivre)
   566 
   567 lemma NSDeMoivre2:
   568   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
   569 by transfer (fold real_of_nat_def, rule DeMoivre2)
   570 
   571 lemma DeMoivre2_ext:
   572   "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
   573 by transfer (fold real_of_nat_def, rule DeMoivre2)
   574 
   575 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
   576 by transfer (rule cis_inverse)
   577 
   578 lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
   579 by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
   580 
   581 lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
   582 by transfer simp
   583 
   584 lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
   585 by transfer simp
   586 
   587 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   588 by (simp add: NSDeMoivre)
   589 
   590 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   591 by (simp add: NSDeMoivre)
   592 
   593 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
   594 by (simp add: NSDeMoivre_ext)
   595 
   596 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
   597 by (simp add: NSDeMoivre_ext)
   598 
   599 lemma hExp_add: "!!a b. hExp(a + b) = hExp(a) * hExp(b)"
   600 by transfer (rule exp_add)
   601 
   602 
   603 subsection{*@{term hcomplex_of_complex}: the Injection from
   604   type @{typ complex} to to @{typ hcomplex}*}
   605 
   606 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
   607 by (rule iii_def)
   608 
   609 lemma hRe_hcomplex_of_complex:
   610    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
   611 by transfer (rule refl)
   612 
   613 lemma hIm_hcomplex_of_complex:
   614    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
   615 by transfer (rule refl)
   616 
   617 lemma hcmod_hcomplex_of_complex:
   618      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
   619 by transfer (rule refl)
   620 
   621 
   622 subsection{*Numerals and Arithmetic*}
   623 
   624 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
   625      "hcomplex_of_hypreal (hypreal_of_real x) =
   626       hcomplex_of_complex (complex_of_real x)"
   627 by transfer (rule refl)
   628 
   629 lemma hcomplex_hypreal_numeral:
   630   "hcomplex_of_complex (numeral w) = hcomplex_of_hypreal(numeral w)"
   631 by transfer (rule of_real_numeral [symmetric])
   632 
   633 lemma hcomplex_hypreal_neg_numeral:
   634   "hcomplex_of_complex (- numeral w) = hcomplex_of_hypreal(- numeral w)"
   635 by transfer (rule of_real_neg_numeral [symmetric])
   636 
   637 lemma hcomplex_numeral_hcnj [simp]:
   638      "hcnj (numeral v :: hcomplex) = numeral v"
   639 by transfer (rule complex_cnj_numeral)
   640 
   641 lemma hcomplex_numeral_hcmod [simp]:
   642       "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
   643 by transfer (rule norm_numeral)
   644 
   645 lemma hcomplex_neg_numeral_hcmod [simp]:
   646       "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
   647 by transfer (rule norm_neg_numeral)
   648 
   649 lemma hcomplex_numeral_hRe [simp]:
   650       "hRe(numeral v :: hcomplex) = numeral v"
   651 by transfer (rule complex_Re_numeral)
   652 
   653 lemma hcomplex_numeral_hIm [simp]:
   654       "hIm(numeral v :: hcomplex) = 0"
   655 by transfer (rule complex_Im_numeral)
   656 
   657 end