src/HOL/NSA/NSComplex.thy
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25)
changeset 47108 2a1953f0d20d
parent 44846 e9d1fcbc7d20
child 49962 a8cc904a6820
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
     1 (*  Title:      HOL/NSA/NSComplex.thy
     2     Author:     Jacques D. Fleuriot, University of Edinburgh
     3     Author:     Lawrence C Paulson
     4 *)
     5 
     6 header{*Nonstandard Complex Numbers*}
     7 
     8 theory NSComplex
     9 imports Complex 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   hexpi :: "hcomplex => hcomplex" where
    75   "hexpi = *f* expi"
    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 hexpi_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_hexpi [simp]: "x \<in> Standard \<Longrightarrow> hexpi 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 (rule complex_Re_zero)
   133 
   134 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
   135 by transfer (rule complex_Im_zero)
   136 
   137 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
   138 by transfer (rule complex_Re_one)
   139 
   140 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
   141 by transfer (rule complex_Im_one)
   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 (rule complex_Re_add)
   148 
   149 lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
   150 by transfer (rule complex_Im_add)
   151 
   152 subsection{*More Minus Laws*}
   153 
   154 lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
   155 by transfer (rule complex_Re_minus)
   156 
   157 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
   158 by transfer (rule complex_Im_minus)
   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 (rule Re)
   216 
   217 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
   218 by transfer (rule Im)
   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) ^ 2 + hIm(z) ^ 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) ^ 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 ^ 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 (rule neg_power_if)
   378 
   379 lemma hcpow_mult:
   380   "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
   381 by transfer (rule power_mult_distrib)
   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 ^ 2 + y ^ 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 (rule i_def [THEN meta_eq_to_obj_eq])
   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) =
   439       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
   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 
   450 lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
   451 by transfer simp
   452 
   453 lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
   454 by transfer simp
   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"
   462 by transfer (rule cos_arg_i_mult_zero)
   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 
   469 subsection{*Polar Form for Nonstandard Complex Numbers*}
   470 
   471 lemma complex_split_polar2:
   472      "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
   473 by (blast intro: complex_split_polar)
   474 
   475 lemma hcomplex_split_polar:
   476   "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   477 by transfer (rule complex_split_polar)
   478 
   479 lemma hcis_eq:
   480    "!!a. hcis a =
   481     (hcomplex_of_hypreal(( *f* cos) a) +
   482     iii * hcomplex_of_hypreal(( *f* sin) a))"
   483 by transfer (simp add: cis_def)
   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]:
   489   "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   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]:
   497   "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   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"
   506 by transfer (rule cmod_unit_one)
   507 
   508 lemma hcmod_complex_polar [simp]:
   509   "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   510       abs r"
   511 by transfer (rule cmod_complex_polar)
   512 
   513 lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
   514 by transfer (rule complex_mod_rcis)
   515 
   516 (*---------------------------------------------------------------------------*)
   517 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
   518 (*---------------------------------------------------------------------------*)
   519 
   520 lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a"
   521 by transfer (rule cis_rcis_eq)
   522 declare hcis_hrcis_eq [symmetric, simp]
   523 
   524 lemma hrcis_mult:
   525   "!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
   526 by transfer (rule rcis_mult)
   527 
   528 lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)"
   529 by transfer (rule cis_mult)
   530 
   531 lemma hcis_zero [simp]: "hcis 0 = 1"
   532 by transfer (rule cis_zero)
   533 
   534 lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0"
   535 by transfer (rule rcis_zero_mod)
   536 
   537 lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r"
   538 by transfer (rule rcis_zero_arg)
   539 
   540 lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x"
   541 by transfer (rule complex_i_mult_minus)
   542 
   543 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
   544 by simp
   545 
   546 lemma hcis_hypreal_of_nat_Suc_mult:
   547    "!!a. hcis (hypreal_of_nat (Suc n) * a) =
   548      hcis a * hcis (hypreal_of_nat n * a)"
   549 apply transfer
   550 apply (simp add: left_distrib cis_mult)
   551 done
   552 
   553 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
   554 apply transfer
   555 apply (fold real_of_nat_def)
   556 apply (rule DeMoivre)
   557 done
   558 
   559 lemma hcis_hypreal_of_hypnat_Suc_mult:
   560      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
   561       hcis a * hcis (hypreal_of_hypnat n * a)"
   562 by transfer (simp add: left_distrib cis_mult)
   563 
   564 lemma NSDeMoivre_ext:
   565   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
   566 by transfer (fold real_of_nat_def, rule DeMoivre)
   567 
   568 lemma NSDeMoivre2:
   569   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
   570 by transfer (fold real_of_nat_def, rule DeMoivre2)
   571 
   572 lemma DeMoivre2_ext:
   573   "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
   574 by transfer (fold real_of_nat_def, rule DeMoivre2)
   575 
   576 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
   577 by transfer (rule cis_inverse)
   578 
   579 lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
   580 by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
   581 
   582 lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
   583 by transfer (rule Re_cis)
   584 
   585 lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
   586 by transfer (rule Im_cis)
   587 
   588 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   589 by (simp add: NSDeMoivre)
   590 
   591 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   592 by (simp add: NSDeMoivre)
   593 
   594 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
   595 by (simp add: NSDeMoivre_ext)
   596 
   597 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
   598 by (simp add: NSDeMoivre_ext)
   599 
   600 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
   601 by transfer (rule exp_add)
   602 
   603 
   604 subsection{*@{term hcomplex_of_complex}: the Injection from
   605   type @{typ complex} to to @{typ hcomplex}*}
   606 
   607 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
   608 (* TODO: delete *)
   609 by (rule inj_star_of)
   610 
   611 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
   612 by (rule iii_def)
   613 
   614 lemma hRe_hcomplex_of_complex:
   615    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
   616 by transfer (rule refl)
   617 
   618 lemma hIm_hcomplex_of_complex:
   619    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
   620 by transfer (rule refl)
   621 
   622 lemma hcmod_hcomplex_of_complex:
   623      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
   624 by transfer (rule refl)
   625 
   626 
   627 subsection{*Numerals and Arithmetic*}
   628 
   629 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
   630      "hcomplex_of_hypreal (hypreal_of_real x) =  
   631       hcomplex_of_complex (complex_of_real x)"
   632 by transfer (rule refl)
   633 
   634 lemma hcomplex_hypreal_numeral:
   635   "hcomplex_of_complex (numeral w) = hcomplex_of_hypreal(numeral w)"
   636 by transfer (rule of_real_numeral [symmetric])
   637 
   638 lemma hcomplex_hypreal_neg_numeral:
   639   "hcomplex_of_complex (neg_numeral w) = hcomplex_of_hypreal(neg_numeral w)"
   640 by transfer (rule of_real_neg_numeral [symmetric])
   641 
   642 lemma hcomplex_numeral_hcnj [simp]:
   643      "hcnj (numeral v :: hcomplex) = numeral v"
   644 by transfer (rule complex_cnj_numeral)
   645 
   646 lemma hcomplex_numeral_hcmod [simp]:
   647       "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
   648 by transfer (rule norm_numeral)
   649 
   650 lemma hcomplex_neg_numeral_hcmod [simp]: 
   651       "hcmod(neg_numeral v :: hcomplex) = (numeral v :: hypreal)"
   652 by transfer (rule norm_neg_numeral)
   653 
   654 lemma hcomplex_numeral_hRe [simp]: 
   655       "hRe(numeral v :: hcomplex) = numeral v"
   656 by transfer (rule complex_Re_numeral)
   657 
   658 lemma hcomplex_numeral_hIm [simp]: 
   659       "hIm(numeral v :: hcomplex) = 0"
   660 by transfer (rule complex_Im_numeral)
   661 
   662 (* TODO: add neg_numeral rules above *)
   663 end