src/HOL/NSA/NSComplex.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 37765 26bdfb7b680b
child 41959 b460124855b8
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Title:       NSComplex.thy
     2     Author:      Jacques D. Fleuriot
     3     Copyright:   2001  University of Edinburgh
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     5 *)
     6 
     7 header{*Nonstandard Complex Numbers*}
     8 
     9 theory NSComplex
    10 imports Complex NSA
    11 begin
    12 
    13 types hcomplex = "complex star"
    14 
    15 abbreviation
    16   hcomplex_of_complex :: "complex => complex star" where
    17   "hcomplex_of_complex == star_of"
    18 
    19 abbreviation
    20   hcmod :: "complex star => real star" where
    21   "hcmod == hnorm"
    22 
    23 
    24   (*--- real and Imaginary parts ---*)
    25 
    26 definition
    27   hRe :: "hcomplex => hypreal" where
    28   "hRe = *f* Re"
    29 
    30 definition
    31   hIm :: "hcomplex => hypreal" where
    32   "hIm = *f* Im"
    33 
    34 
    35   (*------ imaginary unit ----------*)
    36 
    37 definition
    38   iii :: hcomplex where
    39   "iii = star_of ii"
    40 
    41   (*------- complex conjugate ------*)
    42 
    43 definition
    44   hcnj :: "hcomplex => hcomplex" where
    45   "hcnj = *f* cnj"
    46 
    47   (*------------ Argand -------------*)
    48 
    49 definition
    50   hsgn :: "hcomplex => hcomplex" where
    51   "hsgn = *f* sgn"
    52 
    53 definition
    54   harg :: "hcomplex => hypreal" where
    55   "harg = *f* arg"
    56 
    57 definition
    58   (* abbreviation for (cos a + i sin a) *)
    59   hcis :: "hypreal => hcomplex" where
    60   "hcis = *f* cis"
    61 
    62   (*----- injection from hyperreals -----*)
    63 
    64 abbreviation
    65   hcomplex_of_hypreal :: "hypreal \<Rightarrow> hcomplex" where
    66   "hcomplex_of_hypreal \<equiv> of_hypreal"
    67 
    68 definition
    69   (* abbreviation for r*(cos a + i sin a) *)
    70   hrcis :: "[hypreal, hypreal] => hcomplex" where
    71   "hrcis = *f2* rcis"
    72 
    73   (*------------ e ^ (x + iy) ------------*)
    74 definition
    75   hexpi :: "hcomplex => hcomplex" where
    76   "hexpi = *f* expi"
    77 
    78 definition
    79   HComplex :: "[hypreal,hypreal] => hcomplex" where
    80   "HComplex = *f2* Complex"
    81 
    82 lemmas hcomplex_defs [transfer_unfold] =
    83   hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
    84   hrcis_def hexpi_def HComplex_def
    85 
    86 lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard"
    87 by (simp add: hcomplex_defs)
    88 
    89 lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard"
    90 by (simp add: hcomplex_defs)
    91 
    92 lemma Standard_iii [simp]: "iii \<in> Standard"
    93 by (simp add: hcomplex_defs)
    94 
    95 lemma Standard_hcnj [simp]: "x \<in> Standard \<Longrightarrow> hcnj x \<in> Standard"
    96 by (simp add: hcomplex_defs)
    97 
    98 lemma Standard_hsgn [simp]: "x \<in> Standard \<Longrightarrow> hsgn x \<in> Standard"
    99 by (simp add: hcomplex_defs)
   100 
   101 lemma Standard_harg [simp]: "x \<in> Standard \<Longrightarrow> harg x \<in> Standard"
   102 by (simp add: hcomplex_defs)
   103 
   104 lemma Standard_hcis [simp]: "r \<in> Standard \<Longrightarrow> hcis r \<in> Standard"
   105 by (simp add: hcomplex_defs)
   106 
   107 lemma Standard_hexpi [simp]: "x \<in> Standard \<Longrightarrow> hexpi x \<in> Standard"
   108 by (simp add: hcomplex_defs)
   109 
   110 lemma Standard_hrcis [simp]:
   111   "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> hrcis r s \<in> Standard"
   112 by (simp add: hcomplex_defs)
   113 
   114 lemma Standard_HComplex [simp]:
   115   "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard"
   116 by (simp add: hcomplex_defs)
   117 
   118 lemma hcmod_def: "hcmod = *f* cmod"
   119 by (rule hnorm_def)
   120 
   121 
   122 subsection{*Properties of Nonstandard Real and Imaginary Parts*}
   123 
   124 lemma hcomplex_hRe_hIm_cancel_iff:
   125      "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
   126 by transfer (rule complex_Re_Im_cancel_iff)
   127 
   128 lemma hcomplex_equality [intro?]:
   129   "!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w"
   130 by transfer (rule complex_equality)
   131 
   132 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
   133 by transfer (rule complex_Re_zero)
   134 
   135 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
   136 by transfer (rule complex_Im_zero)
   137 
   138 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
   139 by transfer (rule complex_Re_one)
   140 
   141 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
   142 by transfer (rule complex_Im_one)
   143 
   144 
   145 subsection{*Addition for Nonstandard Complex Numbers*}
   146 
   147 lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
   148 by transfer (rule complex_Re_add)
   149 
   150 lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
   151 by transfer (rule complex_Im_add)
   152 
   153 subsection{*More Minus Laws*}
   154 
   155 lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
   156 by transfer (rule complex_Re_minus)
   157 
   158 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
   159 by transfer (rule complex_Im_minus)
   160 
   161 lemma hcomplex_add_minus_eq_minus:
   162       "x + y = (0::hcomplex) ==> x = -y"
   163 apply (drule minus_unique)
   164 apply (simp add: minus_equation_iff [of x y])
   165 done
   166 
   167 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
   168 by transfer (rule i_mult_eq2)
   169 
   170 lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
   171 by transfer (rule complex_i_mult_minus)
   172 
   173 lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
   174 by transfer (rule complex_i_not_zero)
   175 
   176 
   177 subsection{*More Multiplication Laws*}
   178 
   179 lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
   180 by simp
   181 
   182 lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
   183 by simp
   184 
   185 lemma hcomplex_mult_left_cancel:
   186      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
   187 by simp
   188 
   189 lemma hcomplex_mult_right_cancel:
   190      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   191 by simp
   192 
   193 
   194 subsection{*Subraction and Division*}
   195 
   196 lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
   197 (* TODO: delete *)
   198 by (rule diff_eq_eq)
   199 
   200 
   201 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
   202 
   203 lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
   204 by transfer (rule Re_complex_of_real)
   205 
   206 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0"
   207 by transfer (rule Im_complex_of_real)
   208 
   209 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
   210      "hcomplex_of_hypreal epsilon \<noteq> 0"
   211 by (simp add: hypreal_epsilon_not_zero)
   212 
   213 subsection{*HComplex theorems*}
   214 
   215 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
   216 by transfer (rule Re)
   217 
   218 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
   219 by transfer (rule Im)
   220 
   221 lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z"
   222 by transfer (rule complex_surj)
   223 
   224 lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]:
   225      "(\<And>x y. P (HComplex x y)) ==> P z"
   226 by (rule hcomplex_surj [THEN subst], blast)
   227 
   228 
   229 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   230 
   231 lemma hcomplex_of_hypreal_abs:
   232      "hcomplex_of_hypreal (abs x) =
   233       hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   234 by simp
   235 
   236 lemma HComplex_inject [simp]:
   237   "!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
   238 by transfer (rule complex.inject)
   239 
   240 lemma HComplex_add [simp]:
   241   "!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
   242 by transfer (rule complex_add)
   243 
   244 lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
   245 by transfer (rule complex_minus)
   246 
   247 lemma HComplex_diff [simp]:
   248   "!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
   249 by transfer (rule complex_diff)
   250 
   251 lemma HComplex_mult [simp]:
   252   "!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
   253    HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
   254 by transfer (rule complex_mult)
   255 
   256 (*HComplex_inverse is proved below*)
   257 
   258 lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
   259 by transfer (rule complex_of_real_def)
   260 
   261 lemma HComplex_add_hcomplex_of_hypreal [simp]:
   262      "!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
   263 by transfer (rule Complex_add_complex_of_real)
   264 
   265 lemma hcomplex_of_hypreal_add_HComplex [simp]:
   266      "!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
   267 by transfer (rule complex_of_real_add_Complex)
   268 
   269 lemma HComplex_mult_hcomplex_of_hypreal:
   270      "!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
   271 by transfer (rule Complex_mult_complex_of_real)
   272 
   273 lemma hcomplex_of_hypreal_mult_HComplex:
   274      "!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
   275 by transfer (rule complex_of_real_mult_Complex)
   276 
   277 lemma i_hcomplex_of_hypreal [simp]:
   278      "!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
   279 by transfer (rule i_complex_of_real)
   280 
   281 lemma hcomplex_of_hypreal_i [simp]:
   282      "!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
   283 by transfer (rule complex_of_real_i)
   284 
   285 
   286 subsection{*Conjugation*}
   287 
   288 lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
   289 by transfer (rule complex_cnj_cancel_iff)
   290 
   291 lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
   292 by transfer (rule complex_cnj_cnj)
   293 
   294 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
   295      "!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   296 by transfer (rule complex_cnj_complex_of_real)
   297 
   298 lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
   299 by transfer (rule complex_mod_cnj)
   300 
   301 lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
   302 by transfer (rule complex_cnj_minus)
   303 
   304 lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
   305 by transfer (rule complex_cnj_inverse)
   306 
   307 lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
   308 by transfer (rule complex_cnj_add)
   309 
   310 lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
   311 by transfer (rule complex_cnj_diff)
   312 
   313 lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
   314 by transfer (rule complex_cnj_mult)
   315 
   316 lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
   317 by transfer (rule complex_cnj_divide)
   318 
   319 lemma hcnj_one [simp]: "hcnj 1 = 1"
   320 by transfer (rule complex_cnj_one)
   321 
   322 lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
   323 by transfer (rule complex_cnj_zero)
   324 
   325 lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
   326 by transfer (rule complex_cnj_zero_iff)
   327 
   328 lemma hcomplex_mult_hcnj:
   329      "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   330 by transfer (rule complex_mult_cnj)
   331 
   332 
   333 subsection{*More Theorems about the Function @{term hcmod}*}
   334 
   335 lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
   336      "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
   337 by simp
   338 
   339 lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
   340      "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
   341 by simp
   342 
   343 lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
   344 by transfer (rule complex_mod_mult_cnj)
   345 
   346 lemma hcmod_triangle_ineq2 [simp]:
   347   "!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
   348 by transfer (rule complex_mod_triangle_ineq2)
   349 
   350 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
   351 by transfer (rule norm_diff_ineq)
   352 
   353 
   354 subsection{*Exponentiation*}
   355 
   356 lemma hcomplexpow_0 [simp]:   "z ^ 0       = (1::hcomplex)"
   357 by (rule power_0)
   358 
   359 lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
   360 by (rule power_Suc)
   361 
   362 lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
   363 by transfer (rule power2_i)
   364 
   365 lemma hcomplex_of_hypreal_pow:
   366      "!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
   367 by transfer (rule of_real_power)
   368 
   369 lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n"
   370 by transfer (rule complex_cnj_power)
   371 
   372 lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n"
   373 by transfer (rule norm_power)
   374 
   375 lemma hcpow_minus:
   376      "!!x n. (-x::hcomplex) pow n =
   377       (if ( *p* even) n then (x pow n) else -(x pow n))"
   378 by transfer (rule neg_power_if)
   379 
   380 lemma hcpow_mult:
   381   "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
   382 by transfer (rule power_mult_distrib)
   383 
   384 lemma hcpow_zero2 [simp]:
   385   "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
   386 by transfer (rule power_0_Suc)
   387 
   388 lemma hcpow_not_zero [simp,intro]:
   389   "!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
   390 by (rule hyperpow_not_zero)
   391 
   392 lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
   393 by (blast intro: ccontr dest: hcpow_not_zero)
   394 
   395 subsection{*The Function @{term hsgn}*}
   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 
   409 lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
   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"
   427 by transfer (rule i_def [THEN meta_eq_to_obj_eq])
   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_complex_split:
   439      "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   440       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
   441       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
   442 by transfer (rule complex_inverse_complex_split)
   443 
   444 lemma HComplex_inverse:
   445      "!!x y. inverse (HComplex x y) =
   446       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
   447 by transfer (rule complex_inverse)
   448 
   449 lemma hRe_mult_i_eq[simp]:
   450     "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
   451 by transfer simp
   452 
   453 lemma hIm_mult_i_eq [simp]:
   454     "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
   455 by transfer simp
   456 
   457 lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
   458 by transfer simp
   459 
   460 lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
   461 by transfer simp
   462 
   463 (*---------------------------------------------------------------------------*)
   464 (*  harg                                                                     *)
   465 (*---------------------------------------------------------------------------*)
   466 
   467 lemma cos_harg_i_mult_zero_pos:
   468      "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   469 by transfer (rule cos_arg_i_mult_zero_pos)
   470 
   471 lemma cos_harg_i_mult_zero_neg:
   472      "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   473 by transfer (rule cos_arg_i_mult_zero_neg)
   474 
   475 lemma cos_harg_i_mult_zero [simp]:
   476      "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   477 by transfer (rule cos_arg_i_mult_zero)
   478 
   479 lemma hcomplex_of_hypreal_zero_iff [simp]:
   480      "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
   481 by transfer (rule of_real_eq_0_iff)
   482 
   483 
   484 subsection{*Polar Form for Nonstandard Complex Numbers*}
   485 
   486 lemma complex_split_polar2:
   487      "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
   488 by (blast intro: complex_split_polar)
   489 
   490 lemma hcomplex_split_polar:
   491   "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   492 by transfer (rule complex_split_polar)
   493 
   494 lemma hcis_eq:
   495    "!!a. hcis a =
   496     (hcomplex_of_hypreal(( *f* cos) a) +
   497     iii * hcomplex_of_hypreal(( *f* sin) a))"
   498 by transfer (simp add: cis_def)
   499 
   500 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
   501 by transfer (rule rcis_Ex)
   502 
   503 lemma hRe_hcomplex_polar [simp]:
   504   "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   505       r * ( *f* cos) a"
   506 by transfer simp
   507 
   508 lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a"
   509 by transfer (rule Re_rcis)
   510 
   511 lemma hIm_hcomplex_polar [simp]:
   512   "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   513       r * ( *f* sin) a"
   514 by transfer simp
   515 
   516 lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a"
   517 by transfer (rule Im_rcis)
   518 
   519 lemma hcmod_unit_one [simp]:
   520      "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
   521 by transfer (rule cmod_unit_one)
   522 
   523 lemma hcmod_complex_polar [simp]:
   524   "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   525       abs r"
   526 by transfer (rule cmod_complex_polar)
   527 
   528 lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
   529 by transfer (rule complex_mod_rcis)
   530 
   531 (*---------------------------------------------------------------------------*)
   532 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
   533 (*---------------------------------------------------------------------------*)
   534 
   535 lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a"
   536 by transfer (rule cis_rcis_eq)
   537 declare hcis_hrcis_eq [symmetric, simp]
   538 
   539 lemma hrcis_mult:
   540   "!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
   541 by transfer (rule rcis_mult)
   542 
   543 lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)"
   544 by transfer (rule cis_mult)
   545 
   546 lemma hcis_zero [simp]: "hcis 0 = 1"
   547 by transfer (rule cis_zero)
   548 
   549 lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0"
   550 by transfer (rule rcis_zero_mod)
   551 
   552 lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r"
   553 by transfer (rule rcis_zero_arg)
   554 
   555 lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x"
   556 by transfer (rule complex_i_mult_minus)
   557 
   558 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
   559 by simp
   560 
   561 lemma hcis_hypreal_of_nat_Suc_mult:
   562    "!!a. hcis (hypreal_of_nat (Suc n) * a) =
   563      hcis a * hcis (hypreal_of_nat n * a)"
   564 apply transfer
   565 apply (fold real_of_nat_def)
   566 apply (rule cis_real_of_nat_Suc_mult)
   567 done
   568 
   569 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
   570 apply transfer
   571 apply (fold real_of_nat_def)
   572 apply (rule DeMoivre)
   573 done
   574 
   575 lemma hcis_hypreal_of_hypnat_Suc_mult:
   576      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
   577       hcis a * hcis (hypreal_of_hypnat n * a)"
   578 by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
   579 
   580 lemma NSDeMoivre_ext:
   581   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
   582 by transfer (fold real_of_nat_def, rule DeMoivre)
   583 
   584 lemma NSDeMoivre2:
   585   "!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
   586 by transfer (fold real_of_nat_def, rule DeMoivre2)
   587 
   588 lemma DeMoivre2_ext:
   589   "!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
   590 by transfer (fold real_of_nat_def, rule DeMoivre2)
   591 
   592 lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
   593 by transfer (rule cis_inverse)
   594 
   595 lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
   596 by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
   597 
   598 lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
   599 by transfer (rule Re_cis)
   600 
   601 lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
   602 by transfer (rule Im_cis)
   603 
   604 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   605 by (simp add: NSDeMoivre)
   606 
   607 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   608 by (simp add: NSDeMoivre)
   609 
   610 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
   611 by (simp add: NSDeMoivre_ext)
   612 
   613 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
   614 by (simp add: NSDeMoivre_ext)
   615 
   616 lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
   617 by transfer (rule expi_add)
   618 
   619 
   620 subsection{*@{term hcomplex_of_complex}: the Injection from
   621   type @{typ complex} to to @{typ hcomplex}*}
   622 
   623 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
   624 (* TODO: delete *)
   625 by (rule inj_star_of)
   626 
   627 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
   628 by (rule iii_def)
   629 
   630 lemma hRe_hcomplex_of_complex:
   631    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
   632 by transfer (rule refl)
   633 
   634 lemma hIm_hcomplex_of_complex:
   635    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
   636 by transfer (rule refl)
   637 
   638 lemma hcmod_hcomplex_of_complex:
   639      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
   640 by transfer (rule refl)
   641 
   642 
   643 subsection{*Numerals and Arithmetic*}
   644 
   645 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
   646 by transfer (rule number_of_eq [THEN eq_reflection])
   647 
   648 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
   649      "hcomplex_of_hypreal (hypreal_of_real x) =  
   650       hcomplex_of_complex (complex_of_real x)"
   651 by transfer (rule refl)
   652 
   653 lemma hcomplex_hypreal_number_of: 
   654   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
   655 by transfer (rule of_real_number_of_eq [symmetric])
   656 
   657 lemma hcomplex_number_of_hcnj [simp]:
   658      "hcnj (number_of v :: hcomplex) = number_of v"
   659 by transfer (rule complex_cnj_number_of)
   660 
   661 lemma hcomplex_number_of_hcmod [simp]: 
   662       "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
   663 by transfer (rule norm_number_of)
   664 
   665 lemma hcomplex_number_of_hRe [simp]: 
   666       "hRe(number_of v :: hcomplex) = number_of v"
   667 by transfer (rule complex_Re_number_of)
   668 
   669 lemma hcomplex_number_of_hIm [simp]: 
   670       "hIm(number_of v :: hcomplex) = 0"
   671 by transfer (rule complex_Im_number_of)
   672 
   673 end