src/HOL/Complex/NSComplex.thy
author paulson
Tue Dec 23 14:45:47 2003 +0100 (2003-12-23)
changeset 14320 fb7a114826be
parent 14318 7dbd3988b15b
child 14323 27724f528f82
permissions -rw-r--r--
tidying up hcomplex arithmetic
     1 (*  Title:       NSComplex.thy
     2     Author:      Jacques D. Fleuriot
     3     Copyright:   2001  University of Edinburgh
     4     Description: Nonstandard Complex numbers
     5 *)
     6 
     7 theory NSComplex = NSInduct:
     8 
     9 (* Move to one of the hyperreal theories *)
    10 lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
    11 apply (induct_tac "m")
    12 apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
    13 done
    14 
    15 constdefs
    16     hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
    17     "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) &
    18                         {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    19 
    20 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
    21   by (auto simp add: quotient_def)
    22 
    23 instance hcomplex :: zero ..
    24 instance hcomplex :: one ..
    25 instance hcomplex :: plus ..
    26 instance hcomplex :: times ..
    27 instance hcomplex :: minus ..
    28 instance hcomplex :: inverse ..
    29 instance hcomplex :: power ..
    30 
    31 defs (overloaded)
    32   hcomplex_zero_def:
    33   "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
    34 
    35   hcomplex_one_def:
    36   "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"
    37 
    38 
    39   hcomplex_minus_def:
    40   "- z == Abs_hcomplex(UN X: Rep_hcomplex(z).
    41                        hcomplexrel `` {%n::nat. - (X n)})"
    42 
    43   hcomplex_diff_def:
    44   "w - z == w + -(z::hcomplex)"
    45 
    46 constdefs
    47 
    48   hcomplex_of_complex :: "complex => hcomplex"
    49   "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
    50 
    51   hcinv  :: "hcomplex => hcomplex"
    52   "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P).
    53                     hcomplexrel `` {%n. inverse(X n)})"
    54 
    55   (*--- real and Imaginary parts ---*)
    56 
    57   hRe :: "hcomplex => hypreal"
    58   "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
    59 
    60   hIm :: "hcomplex => hypreal"
    61   "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
    62 
    63 
    64   (*----------- modulus ------------*)
    65 
    66   hcmod :: "hcomplex => hypreal"
    67   "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
    68 			  hyprel `` {%n. cmod (X n)})"
    69 
    70   (*------ imaginary unit ----------*)
    71 
    72   iii :: hcomplex
    73   "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"
    74 
    75   (*------- complex conjugate ------*)
    76 
    77   hcnj :: "hcomplex => hcomplex"
    78   "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"
    79 
    80   (*------------ Argand -------------*)
    81 
    82   hsgn :: "hcomplex => hcomplex"
    83   "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
    84 
    85   harg :: "hcomplex => hypreal"
    86   "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
    87 
    88   (* abbreviation for (cos a + i sin a) *)
    89   hcis :: "hypreal => hcomplex"
    90   "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
    91 
    92   (* abbreviation for r*(cos a + i sin a) *)
    93   hrcis :: "[hypreal, hypreal] => hcomplex"
    94   "hrcis r a == hcomplex_of_hypreal r * hcis a"
    95 
    96   (*----- injection from hyperreals -----*)
    97 
    98   hcomplex_of_hypreal :: "hypreal => hcomplex"
    99   "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
   100 			       hcomplexrel `` {%n. complex_of_real (X n)})"
   101 
   102   (*------------ e ^ (x + iy) ------------*)
   103 
   104   hexpi :: "hcomplex => hcomplex"
   105   "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
   106 
   107 
   108 defs (overloaded)
   109 
   110   (*----------- division ----------*)
   111 
   112   hcomplex_divide_def:
   113   "w / (z::hcomplex) == w * inverse z"
   114 
   115   hcomplex_add_def:
   116   "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
   117 		      hcomplexrel `` {%n. X n + Y n})"
   118 
   119   hcomplex_mult_def:
   120   "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
   121 		      hcomplexrel `` {%n. X n * Y n})"
   122 
   123 
   124 primrec
   125      hcomplexpow_0:   "z ^ 0       = 1"
   126      hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
   127 
   128 
   129 consts
   130   "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr 80)
   131 
   132 defs
   133   (* hypernatural powers of nonstandard complex numbers *)
   134   hcpow_def:
   135   "(z::hcomplex) hcpow (n::hypnat)
   136       == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
   137              hcomplexrel `` {%n. (X n) ^ (Y n)})"
   138 
   139 
   140 lemma hcomplexrel_iff:
   141    "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
   142 apply (unfold hcomplexrel_def)
   143 apply fast
   144 done
   145 
   146 lemma hcomplexrel_refl: "(x,x): hcomplexrel"
   147 apply (simp add: hcomplexrel_iff) 
   148 done
   149 
   150 lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
   151 apply (auto simp add: hcomplexrel_iff eq_commute)
   152 done
   153 
   154 lemma hcomplexrel_trans:
   155       "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
   156 apply (simp add: hcomplexrel_iff) 
   157 apply ultra
   158 done
   159 
   160 lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
   161 apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) 
   162 apply (blast intro: hcomplexrel_sym hcomplexrel_trans) 
   163 done
   164 
   165 lemmas equiv_hcomplexrel_iff =
   166     eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
   167 
   168 lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
   169 apply (unfold hcomplex_def hcomplexrel_def quotient_def)
   170 apply blast
   171 done
   172 
   173 lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
   174 apply (rule inj_on_inverseI)
   175 apply (erule Abs_hcomplex_inverse)
   176 done
   177 
   178 declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp]
   179         Abs_hcomplex_inverse [simp]
   180 
   181 declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
   182 
   183 declare hcomplexrel_iff [iff]
   184 
   185 lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
   186 apply (rule inj_on_inverseI)
   187 apply (rule Rep_hcomplex_inverse)
   188 done
   189 
   190 lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}"
   191 apply (unfold hcomplexrel_def)
   192 apply (safe)
   193 apply auto
   194 done
   195 declare lemma_hcomplexrel_refl [simp]
   196 
   197 lemma hcomplex_empty_not_mem: "{} ~: hcomplex"
   198 apply (unfold hcomplex_def)
   199 apply (auto elim!: quotientE)
   200 done
   201 declare hcomplex_empty_not_mem [simp]
   202 
   203 lemma Rep_hcomplex_nonempty: "Rep_hcomplex x ~= {}"
   204 apply (cut_tac x = "x" in Rep_hcomplex)
   205 apply auto
   206 done
   207 declare Rep_hcomplex_nonempty [simp]
   208 
   209 lemma eq_Abs_hcomplex:
   210     "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
   211 apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
   212 apply (drule_tac f = Abs_hcomplex in arg_cong)
   213 apply (force simp add: Rep_hcomplex_inverse)
   214 done
   215 
   216 
   217 subsection{*Properties of Nonstandard Real and Imaginary Parts*}
   218 
   219 lemma hRe:
   220      "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
   221       Abs_hypreal(hyprel `` {%n. Re(X n)})"
   222 apply (unfold hRe_def)
   223 apply (rule_tac f = "Abs_hypreal" in arg_cong)
   224 apply (auto , ultra)
   225 done
   226 
   227 lemma hIm:
   228      "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
   229       Abs_hypreal(hyprel `` {%n. Im(X n)})"
   230 apply (unfold hIm_def)
   231 apply (rule_tac f = "Abs_hypreal" in arg_cong)
   232 apply (auto , ultra)
   233 done
   234 
   235 lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
   236 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   237 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   238 apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
   239 apply (ultra+)
   240 done
   241 
   242 lemma hcomplex_hRe_zero: "hRe 0 = 0"
   243 apply (unfold hcomplex_zero_def)
   244 apply (simp (no_asm) add: hRe hypreal_zero_num)
   245 done
   246 declare hcomplex_hRe_zero [simp]
   247 
   248 lemma hcomplex_hIm_zero: "hIm 0 = 0"
   249 apply (unfold hcomplex_zero_def)
   250 apply (simp (no_asm) add: hIm hypreal_zero_num)
   251 done
   252 declare hcomplex_hIm_zero [simp]
   253 
   254 lemma hcomplex_hRe_one: "hRe 1 = 1"
   255 apply (unfold hcomplex_one_def)
   256 apply (simp (no_asm) add: hRe hypreal_one_num)
   257 done
   258 declare hcomplex_hRe_one [simp]
   259 
   260 lemma hcomplex_hIm_one: "hIm 1 = 0"
   261 apply (unfold hcomplex_one_def)
   262 apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num)
   263 done
   264 declare hcomplex_hIm_one [simp]
   265 
   266 (*-----------------------------------------------------------------------*)
   267 (*   hcomplex_of_complex: the injection from complex to hcomplex         *)
   268 (* ----------------------------------------------------------------------*)
   269 
   270 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
   271 apply (rule inj_onI , rule ccontr)
   272 apply (auto simp add: hcomplex_of_complex_def)
   273 done
   274 
   275 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
   276 apply (unfold iii_def hcomplex_of_complex_def)
   277 apply (simp (no_asm))
   278 done
   279 
   280 (*-----------------------------------------------------------------------*)
   281 (*   Addition for nonstandard complex numbers: hcomplex_add              *)
   282 (* ----------------------------------------------------------------------*)
   283 
   284 lemma hcomplex_add_congruent2:
   285     "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
   286 apply (unfold congruent2_def)
   287 apply safe
   288 apply (ultra+)
   289 done
   290 
   291 lemma hcomplex_add:
   292   "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   293    Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
   294 apply (unfold hcomplex_add_def)
   295 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   296 apply auto
   297 apply (ultra)
   298 done
   299 
   300 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
   301 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   302 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   303 apply (simp (no_asm_simp) add: complex_add_commute hcomplex_add)
   304 done
   305 
   306 lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
   307 apply (rule_tac z = "z1" in eq_Abs_hcomplex)
   308 apply (rule_tac z = "z2" in eq_Abs_hcomplex)
   309 apply (rule_tac z = "z3" in eq_Abs_hcomplex)
   310 apply (simp (no_asm_simp) add: hcomplex_add complex_add_assoc)
   311 done
   312 
   313 (*For AC rewriting*)
   314 lemma hcomplex_add_left_commute: "(x::hcomplex)+(y+z)=y+(x+z)"
   315 apply (rule hcomplex_add_commute [THEN trans])
   316 apply (rule hcomplex_add_assoc [THEN trans])
   317 apply (rule hcomplex_add_commute [THEN arg_cong])
   318 done
   319 
   320 (* hcomplex addition is an AC operator *)
   321 lemmas hcomplex_add_ac = hcomplex_add_assoc hcomplex_add_commute
   322                       hcomplex_add_left_commute 
   323 
   324 lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
   325 apply (unfold hcomplex_zero_def)
   326 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   327 apply (simp add: hcomplex_add)
   328 done
   329 
   330 lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
   331 apply (simp (no_asm) add: hcomplex_add_zero_left hcomplex_add_commute)
   332 done
   333 declare hcomplex_add_zero_left [simp] hcomplex_add_zero_right [simp]
   334 
   335 lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
   336 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   337 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   338 apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add)
   339 done
   340 
   341 lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
   342 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   343 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   344 apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
   345 done
   346 
   347 (*-----------------------------------------------------------------------*)
   348 (* hypreal_minus: additive inverse on nonstandard complex                *)
   349 (* ----------------------------------------------------------------------*)
   350 
   351 lemma hcomplex_minus_congruent:
   352   "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
   353 
   354 apply (unfold congruent_def)
   355 apply safe
   356 apply (ultra+)
   357 done
   358 
   359 lemma hcomplex_minus:
   360   "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   361       Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
   362 apply (unfold hcomplex_minus_def)
   363 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   364 apply (auto , ultra)
   365 done
   366 
   367 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
   368 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   369 apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   370 done
   371 declare hcomplex_add_minus_left [simp]
   372 
   373 subsection{*Multiplication for Nonstandard Complex Numbers*}
   374 
   375 lemma hcomplex_mult:
   376   "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   377    Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
   378 
   379 apply (unfold hcomplex_mult_def)
   380 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   381 apply (auto , ultra)
   382 done
   383 
   384 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
   385 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   386 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   387 apply (auto simp add: hcomplex_mult complex_mult_commute)
   388 done
   389 
   390 lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
   391 apply (rule_tac z = "u" in eq_Abs_hcomplex)
   392 apply (rule_tac z = "v" in eq_Abs_hcomplex)
   393 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   394 apply (auto simp add: hcomplex_mult complex_mult_assoc)
   395 done
   396 
   397 lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
   398 apply (unfold hcomplex_one_def)
   399 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   400 apply (auto simp add: hcomplex_mult)
   401 done
   402 declare hcomplex_mult_one_left [simp]
   403 
   404 lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
   405 apply (unfold hcomplex_zero_def)
   406 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   407 apply (auto simp add: hcomplex_mult)
   408 done
   409 declare hcomplex_mult_zero_left [simp]
   410 
   411 lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
   412 apply (rule_tac z = "z1" in eq_Abs_hcomplex)
   413 apply (rule_tac z = "z2" in eq_Abs_hcomplex)
   414 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   415 apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
   416 done
   417 
   418 lemma hcomplex_zero_not_eq_one: "(0::hcomplex) ~= (1::hcomplex)"
   419 apply (unfold hcomplex_zero_def hcomplex_one_def)
   420 apply auto
   421 done
   422 declare hcomplex_zero_not_eq_one [simp]
   423 declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
   424 
   425 
   426 subsection{*Inverse of Nonstandard Complex Number*}
   427 
   428 lemma hcomplex_inverse:
   429   "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   430       Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
   431 apply (unfold hcinv_def)
   432 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   433 apply (auto , ultra)
   434 done
   435 
   436 lemma hcomplex_mult_inv_left:
   437       "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
   438 apply (unfold hcomplex_zero_def hcomplex_one_def)
   439 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   440 apply (auto simp add: hcomplex_inverse hcomplex_mult)
   441 apply (ultra)
   442 apply (rule ccontr)
   443 apply (drule complex_mult_inv_left)
   444 apply auto
   445 done
   446 declare hcomplex_mult_inv_left [simp]
   447 
   448 subsection {* The Field of Nonstandard Complex Numbers *}
   449 
   450 instance hcomplex :: field
   451 proof
   452   fix z u v w :: hcomplex
   453   show "(u + v) + w = u + (v + w)"
   454     by (simp add: hcomplex_add_assoc)
   455   show "z + w = w + z"
   456     by (simp add: hcomplex_add_commute)
   457   show "0 + z = z"
   458     by (simp)
   459   show "-z + z = 0"
   460     by (simp)
   461   show "z - w = z + -w"
   462     by (simp add: hcomplex_diff_def)
   463   show "(u * v) * w = u * (v * w)"
   464     by (simp add: hcomplex_mult_assoc)
   465   show "z * w = w * z"
   466     by (simp add: hcomplex_mult_commute)
   467   show "1 * z = z"
   468     by (simp)
   469   show "0 \<noteq> (1::hcomplex)"
   470     by (rule hcomplex_zero_not_eq_one)
   471   show "(u + v) * w = u * w + v * w"
   472     by (simp add: hcomplex_add_mult_distrib)
   473   assume neq: "w \<noteq> 0"
   474   thus "z / w = z * inverse w"
   475     by (simp add: hcomplex_divide_def)
   476   show "inverse w * w = 1"
   477     by (rule hcomplex_mult_inv_left)
   478 qed
   479 
   480 lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0"
   481 apply (unfold hcomplex_zero_def)
   482 apply (auto simp add: hcomplex_inverse)
   483 done
   484 
   485 lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0"
   486 apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
   487 done
   488 
   489 instance hcomplex :: division_by_zero
   490 proof
   491   fix x :: hcomplex
   492   show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO)
   493   show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) 
   494 qed
   495 
   496 lemma hcomplex_mult_left_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
   497 by (simp add: field_mult_cancel_left) 
   498 
   499 subsection{*More Minus Laws*}
   500 
   501 lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)"
   502 apply (rule inj_onI)
   503 apply (drule_tac f = "uminus" in arg_cong)
   504 apply simp
   505 done
   506 
   507 lemma hRe_minus: "hRe(-z) = - hRe(z)"
   508 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   509 apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
   510 done
   511 
   512 lemma hIm_minus: "hIm(-z) = - hIm(z)"
   513 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   514 apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
   515 done
   516 
   517 lemma hcomplex_add_minus_eq_minus:
   518       "x + y = (0::hcomplex) ==> x = -y"
   519 apply (drule Ring_and_Field.equals_zero_I) 
   520 apply (simp add: minus_equation_iff [of x y]) 
   521 done
   522 
   523 lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)"
   524 apply (rule Ring_and_Field.minus_add_distrib) 
   525 done
   526 
   527 lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)"
   528 apply (rule Ring_and_Field.add_left_cancel) 
   529 done
   530 declare hcomplex_add_left_cancel [iff]
   531 
   532 lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)"
   533 apply (rule Ring_and_Field.add_right_cancel)
   534 done
   535 declare hcomplex_add_right_cancel [iff]
   536 
   537 subsection{*More Multiplication Laws*}
   538 
   539 lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)"
   540 apply (rule Ring_and_Field.mult_left_commute)
   541 done
   542 
   543 lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute
   544                           hcomplex_mult_left_commute
   545 
   546 lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
   547 apply (rule Ring_and_Field.mult_1_right)
   548 done
   549 
   550 lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0"
   551 apply (rule Ring_and_Field.mult_right_zero)
   552 done
   553 
   554 lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)"
   555 apply (rule Ring_and_Field.minus_mult_left)
   556 done
   557 
   558 declare hcomplex_minus_mult_eq1 [symmetric, simp] 
   559 
   560 lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)"
   561 apply (rule Ring_and_Field.minus_mult_right)
   562 done
   563 
   564 declare hcomplex_minus_mult_eq2 [symmetric, simp]
   565 
   566 lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
   567 apply (simp (no_asm))
   568 done
   569 declare hcomplex_mult_minus_one [simp]
   570 
   571 lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
   572 apply (subst hcomplex_mult_commute)
   573 apply (simp (no_asm))
   574 done
   575 declare hcomplex_mult_minus_one_right [simp]
   576 
   577 lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)"
   578 apply (rule Ring_and_Field.right_distrib)
   579 done
   580 
   581 lemma hcomplex_mult_right_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   582 apply (simp add: Ring_and_Field.field_mult_cancel_right); 
   583 done
   584 
   585 lemma hcomplex_inverse_not_zero: "z ~= (0::hcomplex) ==> inverse(z) ~= 0"
   586 apply (simp add: ); 
   587 done
   588 
   589 lemma hcomplex_mult_not_zero: "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0"
   590 apply (simp add: Ring_and_Field.field_mult_eq_0_iff); 
   591 done
   592 
   593 lemmas hcomplex_mult_not_zeroE = hcomplex_mult_not_zero [THEN notE, standard]
   594 
   595 lemma hcomplex_minus_inverse: "inverse(-x) = -inverse(x::hcomplex)"
   596 apply (rule Ring_and_Field.inverse_minus_eq) 
   597 done
   598 
   599 
   600 subsection{*Subraction and Division*}
   601 
   602 lemma hcomplex_diff:
   603  "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   604   Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
   605 apply (unfold hcomplex_diff_def)
   606 apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def)
   607 done
   608 
   609 lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)"
   610 apply (rule Ring_and_Field.diff_eq_eq) 
   611 done
   612 
   613 lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
   614 apply (rule Ring_and_Field.add_divide_distrib) 
   615 done
   616 
   617 
   618 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
   619 
   620 lemma hcomplex_of_hypreal:
   621   "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
   622       Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
   623 apply (unfold hcomplex_of_hypreal_def)
   624 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   625 apply auto
   626 apply (ultra)
   627 done
   628 
   629 lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal"
   630 apply (rule inj_onI)
   631 apply (rule_tac z = "x" in eq_Abs_hypreal)
   632 apply (rule_tac z = "y" in eq_Abs_hypreal)
   633 apply (auto simp add: hcomplex_of_hypreal)
   634 done
   635 
   636 lemma hcomplex_of_hypreal_cancel_iff: "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
   637 apply (auto dest: inj_hcomplex_of_hypreal [THEN injD])
   638 done
   639 declare hcomplex_of_hypreal_cancel_iff [iff]
   640 
   641 lemma hcomplex_of_hypreal_minus: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
   642 apply (rule_tac z = "x" in eq_Abs_hypreal)
   643 apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
   644 done
   645 
   646 lemma hcomplex_of_hypreal_inverse: "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
   647 apply (rule_tac z = "x" in eq_Abs_hypreal)
   648 apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
   649 done
   650 
   651 lemma hcomplex_of_hypreal_add: "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
   652       hcomplex_of_hypreal (x + y)"
   653 apply (rule_tac z = "x" in eq_Abs_hypreal)
   654 apply (rule_tac z = "y" in eq_Abs_hypreal)
   655 apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   656 done
   657 
   658 lemma hcomplex_of_hypreal_diff:
   659      "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
   660       hcomplex_of_hypreal (x - y)"
   661 apply (unfold hcomplex_diff_def)
   662 apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   663 done
   664 
   665 lemma hcomplex_of_hypreal_mult: "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
   666       hcomplex_of_hypreal (x * y)"
   667 apply (rule_tac z = "x" in eq_Abs_hypreal)
   668 apply (rule_tac z = "y" in eq_Abs_hypreal)
   669 apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
   670 done
   671 
   672 lemma hcomplex_of_hypreal_divide:
   673   "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
   674 apply (unfold hcomplex_divide_def)
   675 apply (case_tac "y=0")
   676 apply (simp (no_asm_simp) add: HYPREAL_DIVISION_BY_ZERO HYPREAL_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO)
   677 apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
   678 apply (simp (no_asm) add: hypreal_divide_def)
   679 done
   680 
   681 lemma hcomplex_of_hypreal_one [simp]:
   682       "hcomplex_of_hypreal 1 = 1"
   683 apply (unfold hcomplex_one_def)
   684 apply (auto simp add: hcomplex_of_hypreal hypreal_one_num)
   685 done
   686 
   687 lemma hcomplex_of_hypreal_zero [simp]:
   688       "hcomplex_of_hypreal 0 = 0"
   689 apply (unfold hcomplex_zero_def hypreal_zero_def)
   690 apply (auto simp add: hcomplex_of_hypreal)
   691 done
   692 
   693 lemma hcomplex_of_hypreal_pow:
   694      "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
   695 apply (induct_tac "n")
   696 apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
   697 done
   698 
   699 lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
   700 apply (rule_tac z = "z" in eq_Abs_hypreal)
   701 apply (auto simp add: hcomplex_of_hypreal hRe)
   702 done
   703 declare hRe_hcomplex_of_hypreal [simp]
   704 
   705 lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0"
   706 apply (rule_tac z = "z" in eq_Abs_hypreal)
   707 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
   708 done
   709 declare hIm_hcomplex_of_hypreal [simp]
   710 
   711 lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon ~= 0"
   712 apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
   713 done
   714 declare hcomplex_of_hypreal_epsilon_not_zero [simp]
   715 
   716 
   717 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   718 
   719 lemma hcmod:
   720   "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   721       Abs_hypreal(hyprel `` {%n. cmod (X n)})"
   722 
   723 apply (unfold hcmod_def)
   724 apply (rule_tac f = "Abs_hypreal" in arg_cong)
   725 apply (auto , ultra)
   726 done
   727 
   728 lemma hcmod_zero [simp]:
   729       "hcmod(0) = 0"
   730 apply (unfold hcomplex_zero_def hypreal_zero_def)
   731 apply (auto simp add: hcmod)
   732 done
   733 
   734 lemma hcmod_one:
   735       "hcmod(1) = 1"
   736 apply (unfold hcomplex_one_def)
   737 apply (auto simp add: hcmod hypreal_one_num)
   738 done
   739 declare hcmod_one [simp]
   740 
   741 lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x"
   742 apply (rule_tac z = "x" in eq_Abs_hypreal)
   743 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
   744 done
   745 declare hcmod_hcomplex_of_hypreal [simp]
   746 
   747 lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) =
   748       hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   749 apply (simp (no_asm))
   750 done
   751 
   752 
   753 subsection{*Conjugation*}
   754 
   755 lemma hcnj:
   756   "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   757    Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
   758 apply (unfold hcnj_def)
   759 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   760 apply (auto , ultra)
   761 done
   762 
   763 lemma inj_hcnj: "inj hcnj"
   764 apply (rule inj_onI)
   765 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   766 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   767 apply (auto simp add: hcnj)
   768 done
   769 
   770 lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)"
   771 apply (auto dest: inj_hcnj [THEN injD])
   772 done
   773 declare hcomplex_hcnj_cancel_iff [simp]
   774 
   775 lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z"
   776 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   777 apply (auto simp add: hcnj)
   778 done
   779 declare hcomplex_hcnj_hcnj [simp]
   780 
   781 lemma hcomplex_hcnj_hcomplex_of_hypreal: "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
   782 apply (rule_tac z = "x" in eq_Abs_hypreal)
   783 apply (auto simp add: hcnj hcomplex_of_hypreal)
   784 done
   785 declare hcomplex_hcnj_hcomplex_of_hypreal [simp]
   786 
   787 lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z"
   788 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   789 apply (auto simp add: hcnj hcmod)
   790 done
   791 declare hcomplex_hmod_hcnj [simp]
   792 
   793 lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
   794 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   795 apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus)
   796 done
   797 
   798 lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
   799 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   800 apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse)
   801 done
   802 
   803 lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
   804 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   805 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   806 apply (auto simp add: hcnj hcomplex_add complex_cnj_add)
   807 done
   808 
   809 lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
   810 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   811 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   812 apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff)
   813 done
   814 
   815 lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
   816 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   817 apply (rule_tac z = "w" in eq_Abs_hcomplex)
   818 apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult)
   819 done
   820 
   821 lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
   822 apply (unfold hcomplex_divide_def)
   823 apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse)
   824 done
   825 
   826 lemma hcnj_one: "hcnj 1 = 1"
   827 apply (unfold hcomplex_one_def)
   828 apply (simp (no_asm) add: hcnj)
   829 done
   830 declare hcnj_one [simp]
   831 
   832 lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
   833 apply (induct_tac "n")
   834 apply (auto simp add: hcomplex_hcnj_mult)
   835 done
   836 
   837 (* MOVE to NSComplexBin
   838 Goal "z + hcnj z =
   839       hcomplex_of_hypreal (2 * hRe(z))"
   840 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   841 by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
   842     hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
   843 qed "hcomplex_add_hcnj";
   844 
   845 Goal "z - hcnj z = \
   846 \     hcomplex_of_hypreal (hypreal_of_real 2 * hIm(z)) * iii";
   847 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
   848 by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
   849     hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
   850     complex_diff_cnj,iii_def,hcomplex_mult]));
   851 qed "hcomplex_diff_hcnj";
   852 *)
   853 
   854 lemma hcomplex_hcnj_zero:
   855       "hcnj 0 = 0"
   856 apply (unfold hcomplex_zero_def)
   857 apply (auto simp add: hcnj)
   858 done
   859 declare hcomplex_hcnj_zero [simp]
   860 
   861 lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)"
   862 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   863 apply (auto simp add: hcomplex_zero_def hcnj)
   864 done
   865 declare hcomplex_hcnj_zero_iff [iff]
   866 
   867 lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
   868 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   869 apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj two_eq_Suc_Suc)
   870 done
   871 
   872 
   873 (*---------------------------------------------------------------------------*)
   874 (*  some algebra etc.                                                        *)
   875 (*---------------------------------------------------------------------------*)
   876 
   877 lemma hcomplex_mult_zero_iff: "(x*y = (0::hcomplex)) = (x = 0 | y = 0)"
   878 apply auto
   879 apply (auto intro: ccontr dest: hcomplex_mult_not_zero)
   880 done
   881 declare hcomplex_mult_zero_iff [simp]
   882 
   883 lemma hcomplex_add_left_cancel_zero: "(x + y = x) = (y = (0::hcomplex))"
   884 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   885 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   886 apply (auto simp add: hcomplex_add hcomplex_zero_def)
   887 done
   888 declare hcomplex_add_left_cancel_zero [simp]
   889 
   890 lemma hcomplex_diff_mult_distrib:
   891       "((z1::hcomplex) - z2) * w = (z1 * w) - (z2 * w)"
   892 apply (unfold hcomplex_diff_def)
   893 apply (simp (no_asm) add: hcomplex_add_mult_distrib)
   894 done
   895 
   896 lemma hcomplex_diff_mult_distrib2:
   897       "(w::hcomplex) * (z1 - z2) = (w * z1) - (w * z2)"
   898 apply (unfold hcomplex_diff_def)
   899 apply (simp (no_asm) add: hcomplex_add_mult_distrib2)
   900 done
   901 
   902 (*---------------------------------------------------------------------------*)
   903 (*  More theorems about hcmod                                                *)
   904 (*---------------------------------------------------------------------------*)
   905 
   906 lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
   907 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   908 apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num)
   909 done
   910 declare hcomplex_hcmod_eq_zero_cancel [simp]
   911 
   912 (* not proved already? strange! *)
   913 lemma hypreal_of_nat_le_iff:
   914       "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
   915 apply (unfold hypreal_le_def)
   916 apply auto
   917 done
   918 declare hypreal_of_nat_le_iff [simp]
   919 
   920 lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
   921 apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
   922          del: hypreal_of_nat_zero)
   923 done
   924 declare hypreal_of_nat_ge_zero [simp]
   925 
   926 declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
   927 
   928 lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
   929 apply (rule_tac z = "n" in eq_Abs_hypnat)
   930 apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
   931 done
   932 declare hypreal_of_hypnat_ge_zero [simp]
   933 
   934 declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
   935 
   936 lemma hcmod_hcomplex_of_hypreal_of_nat: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
   937 apply auto
   938 done
   939 declare hcmod_hcomplex_of_hypreal_of_nat [simp]
   940 
   941 lemma hcmod_hcomplex_of_hypreal_of_hypnat: "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
   942 apply auto
   943 done
   944 declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
   945 
   946 lemma hcmod_minus: "hcmod (-x) = hcmod(x)"
   947 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   948 apply (auto simp add: hcmod hcomplex_minus)
   949 done
   950 declare hcmod_minus [simp]
   951 
   952 lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
   953 apply (rule_tac z = "z" in eq_Abs_hcomplex)
   954 apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj two_eq_Suc_Suc)
   955 done
   956 
   957 lemma hcmod_ge_zero: "(0::hypreal) <= hcmod x"
   958 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   959 apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
   960 done
   961 declare hcmod_ge_zero [simp]
   962 
   963 lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x"
   964 apply (auto intro: hrabs_eqI1)
   965 done
   966 declare hrabs_hcmod_cancel [simp]
   967 
   968 lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
   969 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   970 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   971 apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
   972 done
   973 
   974 lemma hcmod_add_squared_eq:
   975      "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
   976 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   977 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   978 apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   979                       two_eq_Suc_Suc realpow_two [symmetric] 
   980                  simp del: realpow_Suc)
   981 apply (auto simp add: two_eq_Suc_Suc [symmetric] complex_mod_add_squared_eq
   982                  hypreal_add [symmetric] hypreal_mult [symmetric] 
   983                  hypreal_of_real_def [symmetric])
   984 done
   985 
   986 lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) <= hcmod(x * hcnj y)"
   987 apply (rule_tac z = "x" in eq_Abs_hcomplex)
   988 apply (rule_tac z = "y" in eq_Abs_hcomplex)
   989 apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
   990 done
   991 declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
   992 
   993 lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) <= hcmod(x * y)"
   994 apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
   995 apply (simp add: hcmod_mult)
   996 done
   997 declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
   998 
   999 lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 <= (hcmod(x) + hcmod(y)) ^ 2"
  1000 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1001 apply (rule_tac z = "y" in eq_Abs_hcomplex)
  1002 apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
  1003                       hypreal_le realpow_two [symmetric] two_eq_Suc_Suc
  1004             simp del: realpow_Suc)
  1005 apply (simp (no_asm) add: two_eq_Suc_Suc [symmetric])
  1006 done
  1007 declare hcmod_triangle_squared [simp]
  1008 
  1009 lemma hcmod_triangle_ineq: "hcmod (x + y) <= hcmod(x) + hcmod(y)"
  1010 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1011 apply (rule_tac z = "y" in eq_Abs_hcomplex)
  1012 apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
  1013 done
  1014 declare hcmod_triangle_ineq [simp]
  1015 
  1016 lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a"
  1017 apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
  1018 apply (simp add: hypreal_add_ac)
  1019 done
  1020 declare hcmod_triangle_ineq2 [simp]
  1021 
  1022 lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
  1023 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1024 apply (rule_tac z = "y" in eq_Abs_hcomplex)
  1025 apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute)
  1026 done
  1027 
  1028 lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
  1029 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1030 apply (rule_tac z = "y" in eq_Abs_hcomplex)
  1031 apply (rule_tac z = "r" in eq_Abs_hypreal)
  1032 apply (rule_tac z = "s" in eq_Abs_hypreal)
  1033 apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less)
  1034 apply ultra
  1035 apply (auto intro: complex_mod_add_less)
  1036 done
  1037 
  1038 lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
  1039 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1040 apply (rule_tac z = "y" in eq_Abs_hcomplex)
  1041 apply (rule_tac z = "r" in eq_Abs_hypreal)
  1042 apply (rule_tac z = "s" in eq_Abs_hypreal)
  1043 apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult)
  1044 apply ultra
  1045 apply (auto intro: complex_mod_mult_less)
  1046 done
  1047 
  1048 lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) <= hcmod(a + b)"
  1049 apply (rule_tac z = "a" in eq_Abs_hcomplex)
  1050 apply (rule_tac z = "b" in eq_Abs_hcomplex)
  1051 apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
  1052 done
  1053 declare hcmod_diff_ineq [simp]
  1054 
  1055 
  1056 
  1057 subsection{*A Few Nonlinear Theorems*}
  1058 
  1059 lemma hcpow:
  1060   "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
  1061    Abs_hypnat(hypnatrel``{%n. Y n}) =
  1062    Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
  1063 apply (unfold hcpow_def)
  1064 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1065 apply (auto , ultra)
  1066 done
  1067 
  1068 lemma hcomplex_of_hypreal_hyperpow: "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
  1069 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1070 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1071 apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
  1072 done
  1073 
  1074 lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
  1075 apply (induct_tac "n")
  1076 apply (auto simp add: hcmod_mult)
  1077 done
  1078 
  1079 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
  1080 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1081 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1082 apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
  1083 done
  1084 
  1085 lemma hcomplexpow_minus: "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
  1086 apply (induct_tac "n")
  1087 apply auto
  1088 done
  1089 
  1090 lemma hcpow_minus: "(-x::hcomplex) hcpow n =
  1091       (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
  1092 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1093 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1094 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
  1095 apply ultra
  1096 apply (auto simp add: complexpow_minus) 
  1097 apply ultra
  1098 done
  1099 
  1100 lemma hccomplex_inverse_minus: "inverse(-x) = - inverse (x::hcomplex)"
  1101 apply (rule_tac z = "x" in eq_Abs_hcomplex)
  1102 apply (auto simp add: hcomplex_inverse hcomplex_minus complex_inverse_minus)
  1103 done
  1104 
  1105 lemma hcomplex_div_one: "x / (1::hcomplex) = x"
  1106 apply (unfold hcomplex_divide_def)
  1107 apply (simp (no_asm))
  1108 done
  1109 declare hcomplex_div_one [simp]
  1110 
  1111 lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
  1112 apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
  1113 apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
  1114 apply (auto simp add: hcmod_mult [symmetric])
  1115 done
  1116 
  1117 lemma hcmod_divide:
  1118       "hcmod(x/y) = hcmod(x)/(hcmod y)"
  1119 apply (unfold hcomplex_divide_def hypreal_divide_def)
  1120 apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse)
  1121 done
  1122 
  1123 lemma hcomplex_inverse_divide:
  1124       "inverse(x/y) = y/(x::hcomplex)"
  1125 apply (unfold hcomplex_divide_def)
  1126 apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute)
  1127 done
  1128 declare hcomplex_inverse_divide [simp]
  1129 
  1130 lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"
  1131 apply (induct_tac "n")
  1132 apply (auto simp add: hcomplex_mult_ac)
  1133 done
  1134 
  1135 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
  1136 apply (rule_tac z = "r" in eq_Abs_hcomplex)
  1137 apply (rule_tac z = "s" in eq_Abs_hcomplex)
  1138 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1139 apply (auto simp add: hcpow hypreal_mult hcomplex_mult complexpow_mult)
  1140 done
  1141 
  1142 lemma hcomplexpow_zero: "(0::hcomplex) ^ (Suc n) = 0"
  1143 apply auto
  1144 done
  1145 declare hcomplexpow_zero [simp]
  1146 
  1147 lemma hcpow_zero:
  1148    "0 hcpow (n + 1) = 0"
  1149 apply (unfold hcomplex_zero_def hypnat_one_def)
  1150 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1151 apply (auto simp add: hcpow hypnat_add)
  1152 done
  1153 declare hcpow_zero [simp]
  1154 
  1155 lemma hcpow_zero2:
  1156    "0 hcpow (hSuc n) = 0"
  1157 apply (unfold hSuc_def)
  1158 apply (simp (no_asm))
  1159 done
  1160 declare hcpow_zero2 [simp]
  1161 
  1162 lemma hcomplexpow_not_zero [rule_format (no_asm)]: "r ~= (0::hcomplex) --> r ^ n ~= 0"
  1163 apply (induct_tac "n")
  1164 apply (auto simp add: hcomplex_mult_not_zero)
  1165 done
  1166 declare hcomplexpow_not_zero [simp]
  1167 declare hcomplexpow_not_zero [intro]
  1168 
  1169 lemma hcpow_not_zero: "r ~= 0 ==> r hcpow n ~= (0::hcomplex)"
  1170 apply (rule_tac z = "r" in eq_Abs_hcomplex)
  1171 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1172 apply (auto simp add: hcpow hcomplex_zero_def)
  1173 apply ultra
  1174 apply (auto dest: complexpow_zero_zero)
  1175 done
  1176 declare hcpow_not_zero [simp]
  1177 declare hcpow_not_zero [intro]
  1178 
  1179 lemma hcomplexpow_zero_zero: "r ^ n = (0::hcomplex) ==> r = 0"
  1180 apply (blast intro: ccontr dest: hcomplexpow_not_zero)
  1181 done
  1182 
  1183 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
  1184 apply (blast intro: ccontr dest: hcpow_not_zero)
  1185 done
  1186 
  1187 lemma hcomplex_i_mult_eq: "iii * iii = - 1"
  1188 apply (unfold iii_def)
  1189 apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus)
  1190 done
  1191 declare hcomplex_i_mult_eq [simp]
  1192 
  1193 lemma hcomplexpow_i_squared: "iii ^ 2 = - 1"
  1194 apply (simp (no_asm) add: two_eq_Suc_Suc)
  1195 done
  1196 declare hcomplexpow_i_squared [simp]
  1197 
  1198 lemma hcomplex_i_not_zero: "iii ~= 0"
  1199 apply (unfold iii_def hcomplex_zero_def)
  1200 apply auto
  1201 done
  1202 declare hcomplex_i_not_zero [simp]
  1203 
  1204 lemma hcomplex_mult_eq_zero_cancel1: "x * y ~= (0::hcomplex) ==> x ~= 0"
  1205 apply auto
  1206 done
  1207 
  1208 lemma hcomplex_mult_eq_zero_cancel2: "x * y ~= (0::hcomplex) ==> y ~= 0"
  1209 apply auto
  1210 done
  1211 
  1212 lemma hcomplex_mult_not_eq_zero_iff: "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
  1213 apply auto
  1214 done
  1215 declare hcomplex_mult_not_eq_zero_iff [iff]
  1216 
  1217 lemma hcomplex_divide:
  1218   "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
  1219    Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
  1220 apply (unfold hcomplex_divide_def complex_divide_def)
  1221 apply (auto simp add: hcomplex_inverse hcomplex_mult)
  1222 done
  1223 
  1224 
  1225 subsection{*The Function @{term hsgn}*}
  1226 
  1227 lemma hsgn:
  1228   "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
  1229       Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
  1230 apply (unfold hsgn_def)
  1231 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1232 apply (auto , ultra)
  1233 done
  1234 
  1235 lemma hsgn_zero: "hsgn 0 = 0"
  1236 apply (unfold hcomplex_zero_def)
  1237 apply (simp (no_asm) add: hsgn)
  1238 done
  1239 declare hsgn_zero [simp]
  1240 
  1241 
  1242 lemma hsgn_one: "hsgn 1 = 1"
  1243 apply (unfold hcomplex_one_def)
  1244 apply (simp (no_asm) add: hsgn)
  1245 done
  1246 declare hsgn_one [simp]
  1247 
  1248 lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
  1249 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1250 apply (auto simp add: hsgn hcomplex_minus sgn_minus)
  1251 done
  1252 
  1253 lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
  1254 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1255 apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
  1256 done
  1257 
  1258 lemma lemma_hypreal_P_EX2: "(EX (x::hypreal) y. P x y) =
  1259       (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
  1260 apply auto
  1261 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1262 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1263 apply auto
  1264 done
  1265 
  1266 lemma complex_split2: "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
  1267 apply (blast intro: complex_split)
  1268 done
  1269 
  1270 (* Interesting proof! *)
  1271 lemma hcomplex_split: "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
  1272 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1273 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
  1274 apply (cut_tac z = "x" in complex_split2)
  1275 apply (drule choice , safe)+
  1276 apply (rule_tac x = "f" in exI)
  1277 apply (rule_tac x = "fa" in exI)
  1278 apply auto
  1279 done
  1280 
  1281 lemma hRe_hcomplex_i: "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
  1282 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1283 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1284 apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  1285 done
  1286 declare hRe_hcomplex_i [simp]
  1287 
  1288 lemma hIm_hcomplex_i: "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
  1289 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1290 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1291 apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  1292 done
  1293 declare hIm_hcomplex_i [simp]
  1294 
  1295 lemma hcmod_i: "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
  1296       ( *f* sqrt) (x ^ 2 + y ^ 2)"
  1297 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1298 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1299 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i two_eq_Suc_Suc)
  1300 done
  1301 
  1302 lemma hcomplex_eq_hRe_eq:
  1303      "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1304       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
  1305        ==> xa = xb"
  1306 apply (unfold iii_def)
  1307 apply (rule_tac z = "xa" in eq_Abs_hypreal)
  1308 apply (rule_tac z = "ya" in eq_Abs_hypreal)
  1309 apply (rule_tac z = "xb" in eq_Abs_hypreal)
  1310 apply (rule_tac z = "yb" in eq_Abs_hypreal)
  1311 apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  1312 apply (ultra)
  1313 done
  1314 
  1315 lemma hcomplex_eq_hIm_eq:
  1316      "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1317       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
  1318        ==> ya = yb"
  1319 apply (unfold iii_def)
  1320 apply (rule_tac z = "xa" in eq_Abs_hypreal)
  1321 apply (rule_tac z = "ya" in eq_Abs_hypreal)
  1322 apply (rule_tac z = "xb" in eq_Abs_hypreal)
  1323 apply (rule_tac z = "yb" in eq_Abs_hypreal)
  1324 apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  1325 apply (ultra)
  1326 done
  1327 
  1328 lemma hcomplex_eq_cancel_iff: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
  1329        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
  1330       ((xa = xb) & (ya = yb))"
  1331 apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
  1332 done
  1333 declare hcomplex_eq_cancel_iff [simp]
  1334 
  1335 lemma hcomplex_eq_cancel_iffA: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
  1336        hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"
  1337 apply (auto simp add: hcomplex_mult_commute)
  1338 done
  1339 declare hcomplex_eq_cancel_iffA [iff]
  1340 
  1341 lemma hcomplex_eq_cancel_iffB: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
  1342        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
  1343 apply (auto simp add: hcomplex_mult_commute)
  1344 done
  1345 declare hcomplex_eq_cancel_iffB [iff]
  1346 
  1347 lemma hcomplex_eq_cancel_iffC: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
  1348        hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
  1349 apply (auto simp add: hcomplex_mult_commute)
  1350 done
  1351 declare hcomplex_eq_cancel_iffC [iff]
  1352 
  1353 lemma hcomplex_eq_cancel_iff2: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
  1354       hcomplex_of_hypreal xa) = (x = xa & y = 0)"
  1355 apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff)
  1356 apply (simp del: hcomplex_eq_cancel_iff)
  1357 done
  1358 declare hcomplex_eq_cancel_iff2 [simp]
  1359 
  1360 lemma hcomplex_eq_cancel_iff2a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
  1361       hcomplex_of_hypreal xa) = (x = xa & y = 0)"
  1362 apply (auto simp add: hcomplex_mult_commute)
  1363 done
  1364 declare hcomplex_eq_cancel_iff2a [simp]
  1365 
  1366 lemma hcomplex_eq_cancel_iff3: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
  1367       iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
  1368 apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff)
  1369 apply (simp del: hcomplex_eq_cancel_iff)
  1370 done
  1371 declare hcomplex_eq_cancel_iff3 [simp]
  1372 
  1373 lemma hcomplex_eq_cancel_iff3a: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
  1374       iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
  1375 apply (auto simp add: hcomplex_mult_commute)
  1376 done
  1377 declare hcomplex_eq_cancel_iff3a [simp]
  1378 
  1379 lemma hcomplex_split_hRe_zero:
  1380      "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
  1381       ==> x = 0"
  1382 apply (unfold iii_def)
  1383 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1384 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1385 apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  1386 apply ultra
  1387 apply (auto simp add: complex_split_Re_zero)
  1388 done
  1389 
  1390 lemma hcomplex_split_hIm_zero:
  1391      "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
  1392       ==> y = 0"
  1393 apply (unfold iii_def)
  1394 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1395 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1396 apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  1397 apply ultra
  1398 apply (auto simp add: complex_split_Im_zero)
  1399 done
  1400 
  1401 lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z"
  1402 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1403 apply (auto simp add: hsgn hcmod hRe hypreal_divide)
  1404 done
  1405 declare hRe_hsgn [simp]
  1406 
  1407 lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z"
  1408 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1409 apply (auto simp add: hsgn hcmod hIm hypreal_divide)
  1410 done
  1411 declare hIm_hsgn [simp]
  1412 
  1413 lemma real_two_squares_add_zero_iff: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
  1414 apply (auto intro: real_sum_squares_cancel)
  1415 done
  1416 declare real_two_squares_add_zero_iff [simp]
  1417 
  1418 lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
  1419       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
  1420       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
  1421 apply (rule_tac z = "x" in eq_Abs_hypreal)
  1422 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1423 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split two_eq_Suc_Suc)
  1424 done
  1425 
  1426 lemma hRe_mult_i_eq:
  1427     "hRe (iii * hcomplex_of_hypreal y) = 0"
  1428 apply (unfold iii_def)
  1429 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1430 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
  1431 done
  1432 declare hRe_mult_i_eq [simp]
  1433 
  1434 lemma hIm_mult_i_eq:
  1435     "hIm (iii * hcomplex_of_hypreal y) = y"
  1436 apply (unfold iii_def)
  1437 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1438 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
  1439 done
  1440 declare hIm_mult_i_eq [simp]
  1441 
  1442 lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
  1443 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1444 apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
  1445 done
  1446 declare hcmod_mult_i [simp]
  1447 
  1448 lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
  1449 apply (auto simp add: hcomplex_mult_commute)
  1450 done
  1451 declare hcmod_mult_i2 [simp]
  1452 
  1453 (*---------------------------------------------------------------------------*)
  1454 (*  harg                                                                     *)
  1455 (*---------------------------------------------------------------------------*)
  1456 
  1457 lemma harg:
  1458   "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
  1459       Abs_hypreal(hyprel `` {%n. arg (X n)})"
  1460 
  1461 apply (unfold harg_def)
  1462 apply (rule_tac f = "Abs_hypreal" in arg_cong)
  1463 apply (auto , ultra)
  1464 done
  1465 
  1466 lemma cos_harg_i_mult_zero: "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1467 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1468 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
  1469 apply (ultra)
  1470 done
  1471 declare cos_harg_i_mult_zero [simp]
  1472 
  1473 lemma cos_harg_i_mult_zero2: "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1474 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1475 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
  1476 apply (ultra)
  1477 done
  1478 declare cos_harg_i_mult_zero2 [simp]
  1479 
  1480 lemma hcomplex_of_hypreal_not_zero_iff: "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
  1481 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1482 apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
  1483 done
  1484 declare hcomplex_of_hypreal_not_zero_iff [simp]
  1485 
  1486 lemma hcomplex_of_hypreal_zero_iff: "(hcomplex_of_hypreal y = 0) = (y = 0)"
  1487 apply (rule_tac z = "y" in eq_Abs_hypreal)
  1488 apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
  1489 done
  1490 declare hcomplex_of_hypreal_zero_iff [simp]
  1491 
  1492 lemma cos_harg_i_mult_zero3: "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
  1493 apply (cut_tac x = "y" and y = "0" in hypreal_linear)
  1494 apply auto
  1495 done
  1496 declare cos_harg_i_mult_zero3 [simp]
  1497 
  1498 (*---------------------------------------------------------------------------*)
  1499 (* Polar form for nonstandard complex numbers                                 *)
  1500 (*---------------------------------------------------------------------------*)
  1501 
  1502 lemma complex_split_polar2: "ALL n. EX r a. (z n) = complex_of_real r *
  1503       (complex_of_real(cos a) + ii * complex_of_real(sin a))"
  1504 apply (blast intro: complex_split_polar)
  1505 done
  1506 
  1507 lemma hcomplex_split_polar:
  1508   "EX r a. z = hcomplex_of_hypreal r *
  1509    (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
  1510 apply (rule_tac z = "z" in eq_Abs_hcomplex)
  1511 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
  1512 apply (cut_tac z = "x" in complex_split_polar2)
  1513 apply (drule choice , safe)+
  1514 apply (rule_tac x = "f" in exI)
  1515 apply (rule_tac x = "fa" in exI)
  1516 apply auto
  1517 done
  1518 
  1519 lemma hcis:
  1520   "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
  1521       Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
  1522 apply (unfold hcis_def)
  1523 apply (rule_tac f = "Abs_hcomplex" in arg_cong)
  1524 apply auto
  1525 apply (ultra)
  1526 done
  1527 
  1528 lemma hcis_eq:
  1529    "hcis a =
  1530     (hcomplex_of_hypreal(( *f* cos) a) +
  1531     iii * hcomplex_of_hypreal(( *f* sin) a))"
  1532 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1533 apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
  1534 done
  1535 
  1536 lemma hrcis:
  1537   "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
  1538       Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
  1539 apply (unfold hrcis_def)
  1540 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
  1541 done
  1542 
  1543 lemma hrcis_Ex: "EX r a. z = hrcis r a"
  1544 apply (simp (no_asm) add: hrcis_def hcis_eq)
  1545 apply (rule hcomplex_split_polar)
  1546 done
  1547 
  1548 lemma hRe_hcomplex_polar: "hRe(hcomplex_of_hypreal r *
  1549       (hcomplex_of_hypreal(( *f* cos) a) +
  1550        iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
  1551 apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
  1552 done
  1553 declare hRe_hcomplex_polar [simp]
  1554 
  1555 lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a"
  1556 apply (unfold hrcis_def)
  1557 apply (auto simp add: hcis_eq)
  1558 done
  1559 declare hRe_hrcis [simp]
  1560 
  1561 lemma hIm_hcomplex_polar: "hIm(hcomplex_of_hypreal r *
  1562       (hcomplex_of_hypreal(( *f* cos) a) +
  1563        iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
  1564 apply (auto simp add: hcomplex_add_mult_distrib2 hcomplex_of_hypreal_mult hcomplex_mult_ac)
  1565 done
  1566 declare hIm_hcomplex_polar [simp]
  1567 
  1568 lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a"
  1569 apply (unfold hrcis_def)
  1570 apply (auto simp add: hcis_eq)
  1571 done
  1572 declare hIm_hrcis [simp]
  1573 
  1574 lemma hcmod_complex_polar: "hcmod (hcomplex_of_hypreal r *
  1575       (hcomplex_of_hypreal(( *f* cos) a) +
  1576        iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
  1577 apply (rule_tac z = "r" in eq_Abs_hypreal)
  1578 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1579 apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
  1580 done
  1581 declare hcmod_complex_polar [simp]
  1582 
  1583 lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r"
  1584 apply (unfold hrcis_def)
  1585 apply (auto simp add: hcis_eq)
  1586 done
  1587 declare hcmod_hrcis [simp]
  1588 
  1589 (*---------------------------------------------------------------------------*)
  1590 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
  1591 (*---------------------------------------------------------------------------*)
  1592 
  1593 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
  1594 apply (unfold hrcis_def)
  1595 apply (simp (no_asm))
  1596 done
  1597 declare hcis_hrcis_eq [symmetric, simp]
  1598 
  1599 lemma hrcis_mult:
  1600   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
  1601 apply (unfold hrcis_def)
  1602 apply (rule_tac z = "r1" in eq_Abs_hypreal)
  1603 apply (rule_tac z = "r2" in eq_Abs_hypreal)
  1604 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1605 apply (rule_tac z = "b" in eq_Abs_hypreal)
  1606 apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  1607                       hcomplex_mult cis_mult [symmetric] 
  1608                       complex_of_real_mult [symmetric])
  1609 done
  1610 
  1611 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
  1612 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1613 apply (rule_tac z = "b" in eq_Abs_hypreal)
  1614 apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult)
  1615 done
  1616 
  1617 lemma hcis_zero:
  1618   "hcis 0 = 1"
  1619 apply (unfold hcomplex_one_def)
  1620 apply (auto simp add: hcis hypreal_zero_num)
  1621 done
  1622 declare hcis_zero [simp]
  1623 
  1624 lemma hrcis_zero_mod:
  1625   "hrcis 0 a = 0"
  1626 apply (unfold hcomplex_zero_def)
  1627 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1628 apply (auto simp add: hrcis hypreal_zero_num)
  1629 done
  1630 declare hrcis_zero_mod [simp]
  1631 
  1632 lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r"
  1633 apply (rule_tac z = "r" in eq_Abs_hypreal)
  1634 apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
  1635 done
  1636 declare hrcis_zero_arg [simp]
  1637 
  1638 lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x"
  1639 apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric])
  1640 done
  1641 declare hcomplex_i_mult_minus [simp]
  1642 
  1643 lemma hcomplex_i_mult_minus2: "iii * iii * x = - x"
  1644 apply (simp (no_asm))
  1645 done
  1646 declare hcomplex_i_mult_minus2 [simp]
  1647 
  1648 lemma hcis_hypreal_of_nat_Suc_mult:
  1649    "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
  1650 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1651 apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1652 done
  1653 
  1654 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
  1655 apply (induct_tac "n")
  1656 apply (auto simp add: hcis_hypreal_of_nat_Suc_mult)
  1657 done
  1658 
  1659 lemma hcis_hypreal_of_hypnat_Suc_mult: "hcis (hypreal_of_hypnat (n + 1) * a) =
  1660       hcis a * hcis (hypreal_of_hypnat n * a)"
  1661 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1662 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1663 apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1664 done
  1665 
  1666 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
  1667 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1668 apply (rule_tac z = "n" in eq_Abs_hypnat)
  1669 apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
  1670 done
  1671 
  1672 lemma DeMoivre2:
  1673   "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
  1674 apply (unfold hrcis_def)
  1675 apply (auto simp add: hcomplexpow_mult NSDeMoivre hcomplex_of_hypreal_pow)
  1676 done
  1677 
  1678 lemma DeMoivre2_ext:
  1679   "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
  1680 apply (unfold hrcis_def)
  1681 apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
  1682 done
  1683 
  1684 lemma hcis_inverse: "inverse(hcis a) = hcis (-a)"
  1685 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1686 apply (auto simp add: hcomplex_inverse hcis hypreal_minus)
  1687 done
  1688 declare hcis_inverse [simp]
  1689 
  1690 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
  1691 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1692 apply (rule_tac z = "r" in eq_Abs_hypreal)
  1693 apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse)
  1694 apply (ultra)
  1695 apply (unfold real_divide_def)
  1696 apply (auto simp add: INVERSE_ZERO)
  1697 done
  1698 
  1699 lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a"
  1700 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1701 apply (auto simp add: hcis starfun hRe)
  1702 done
  1703 declare hRe_hcis [simp]
  1704 
  1705 lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a"
  1706 apply (rule_tac z = "a" in eq_Abs_hypreal)
  1707 apply (auto simp add: hcis starfun hIm)
  1708 done
  1709 declare hIm_hcis [simp]
  1710 
  1711 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
  1712 apply (auto simp add: NSDeMoivre)
  1713 done
  1714 
  1715 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
  1716 apply (auto simp add: NSDeMoivre)
  1717 done
  1718 
  1719 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
  1720 apply (auto simp add: NSDeMoivre_ext)
  1721 done
  1722 
  1723 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
  1724 apply (auto simp add: NSDeMoivre_ext)
  1725 done
  1726 
  1727 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
  1728 apply (unfold hexpi_def)
  1729 apply (rule_tac z = "a" in eq_Abs_hcomplex)
  1730 apply (rule_tac z = "b" in eq_Abs_hcomplex)
  1731 apply (auto simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
  1732 done
  1733 
  1734 
  1735 subsection{*@{term hcomplex_of_complex} Preserves Field Properties*}
  1736 
  1737 lemma hcomplex_of_complex_add:
  1738      "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
  1739 apply (unfold hcomplex_of_complex_def)
  1740 apply (simp (no_asm) add: hcomplex_add)
  1741 done
  1742 declare hcomplex_of_complex_add [simp]
  1743 
  1744 lemma hcomplex_of_complex_mult:
  1745      "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
  1746 apply (unfold hcomplex_of_complex_def)
  1747 apply (simp (no_asm) add: hcomplex_mult)
  1748 done
  1749 declare hcomplex_of_complex_mult [simp]
  1750 
  1751 lemma hcomplex_of_complex_eq_iff:
  1752  "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
  1753 apply (unfold hcomplex_of_complex_def)
  1754 apply auto
  1755 done
  1756 declare hcomplex_of_complex_eq_iff [simp]
  1757 
  1758 lemma hcomplex_of_complex_minus: "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
  1759 apply (unfold hcomplex_of_complex_def)
  1760 apply (auto simp add: hcomplex_minus)
  1761 done
  1762 declare hcomplex_of_complex_minus [simp]
  1763 
  1764 lemma hcomplex_of_complex_one [simp]:
  1765       "hcomplex_of_complex 1 = 1"
  1766 apply (unfold hcomplex_of_complex_def hcomplex_one_def)
  1767 apply auto
  1768 done
  1769 
  1770 lemma hcomplex_of_complex_zero [simp]:
  1771       "hcomplex_of_complex 0 = 0"
  1772 apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
  1773 apply (simp (no_asm))
  1774 done
  1775 
  1776 lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)"
  1777 apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1778 done
  1779 
  1780 lemma hcomplex_of_complex_inverse: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
  1781 apply (case_tac "r=0")
  1782 apply (simp (no_asm_simp) add: COMPLEX_INVERSE_ZERO HCOMPLEX_INVERSE_ZERO hcomplex_of_complex_zero COMPLEX_DIVIDE_ZERO)
  1783 apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1])
  1784 apply (force simp add: hcomplex_of_complex_zero_iff)
  1785 apply (subst hcomplex_of_complex_mult [symmetric])
  1786 apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff); 
  1787 done
  1788 declare hcomplex_of_complex_inverse [simp]
  1789 
  1790 lemma hcomplex_of_complex_divide: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
  1791 apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def)
  1792 done
  1793 declare hcomplex_of_complex_divide [simp]
  1794 
  1795 lemma hRe_hcomplex_of_complex:
  1796    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
  1797 apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
  1798 apply (auto simp add: hRe)
  1799 done
  1800 
  1801 lemma hIm_hcomplex_of_complex:
  1802    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
  1803 apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
  1804 apply (auto simp add: hIm)
  1805 done
  1806 
  1807 lemma hcmod_hcomplex_of_complex:
  1808      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
  1809 apply (unfold hypreal_of_real_def hcomplex_of_complex_def)
  1810 apply (auto simp add: hcmod)
  1811 done
  1812 
  1813 ML
  1814 {*
  1815 val hcomplex_zero_def = thm"hcomplex_zero_def";
  1816 val hcomplex_one_def = thm"hcomplex_one_def";
  1817 val hcomplex_minus_def = thm"hcomplex_minus_def";
  1818 val hcomplex_diff_def = thm"hcomplex_diff_def";
  1819 val hcomplex_divide_def = thm"hcomplex_divide_def";
  1820 val hcomplex_mult_def = thm"hcomplex_mult_def";
  1821 val hcomplex_add_def = thm"hcomplex_add_def";
  1822 val hcomplex_of_complex_def = thm"hcomplex_of_complex_def";
  1823 val iii_def = thm"iii_def";
  1824 
  1825 val hcomplexrel_iff = thm"hcomplexrel_iff";
  1826 val hcomplexrel_refl = thm"hcomplexrel_refl";
  1827 val hcomplexrel_sym = thm"hcomplexrel_sym";
  1828 val hcomplexrel_trans = thm"hcomplexrel_trans";
  1829 val equiv_hcomplexrel = thm"equiv_hcomplexrel";
  1830 val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff";
  1831 val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex";
  1832 val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex";
  1833 val inj_Rep_hcomplex = thm"inj_Rep_hcomplex";
  1834 val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl";
  1835 val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem";
  1836 val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty";
  1837 val eq_Abs_hcomplex = thm"eq_Abs_hcomplex";
  1838 val hRe = thm"hRe";
  1839 val hIm = thm"hIm";
  1840 val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
  1841 val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
  1842 val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
  1843 val hcomplex_hRe_one = thm"hcomplex_hRe_one";
  1844 val hcomplex_hIm_one = thm"hcomplex_hIm_one";
  1845 val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
  1846 val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
  1847 val hcomplex_add_congruent2 = thm"hcomplex_add_congruent2";
  1848 val hcomplex_add = thm"hcomplex_add";
  1849 val hcomplex_add_commute = thm"hcomplex_add_commute";
  1850 val hcomplex_add_assoc = thm"hcomplex_add_assoc";
  1851 val hcomplex_add_left_commute = thm"hcomplex_add_left_commute";
  1852 val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
  1853 val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
  1854 val hRe_add = thm"hRe_add";
  1855 val hIm_add = thm"hIm_add";
  1856 val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
  1857 val hcomplex_minus = thm"hcomplex_minus";
  1858 val inj_hcomplex_minus = thm"inj_hcomplex_minus";
  1859 val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
  1860 val hRe_minus = thm"hRe_minus";
  1861 val hIm_minus = thm"hIm_minus";
  1862 val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
  1863 val hcomplex_minus_add_distrib = thm"hcomplex_minus_add_distrib";
  1864 val hcomplex_add_left_cancel = thm"hcomplex_add_left_cancel";
  1865 val hcomplex_add_right_cancel = thm"hcomplex_add_right_cancel";
  1866 val hcomplex_diff = thm"hcomplex_diff";
  1867 val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
  1868 val hcomplex_mult = thm"hcomplex_mult";
  1869 val hcomplex_mult_commute = thm"hcomplex_mult_commute";
  1870 val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
  1871 val hcomplex_mult_left_commute = thm"hcomplex_mult_left_commute";
  1872 val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
  1873 val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
  1874 val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
  1875 val hcomplex_mult_zero_right = thm"hcomplex_mult_zero_right";
  1876 val hcomplex_minus_mult_eq1 = thm"hcomplex_minus_mult_eq1";
  1877 val hcomplex_minus_mult_eq2 = thm"hcomplex_minus_mult_eq2";
  1878 val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
  1879 val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
  1880 val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
  1881 val hcomplex_add_mult_distrib2 = thm"hcomplex_add_mult_distrib2";
  1882 val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
  1883 val hcomplex_inverse = thm"hcomplex_inverse";
  1884 val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO";
  1885 val HCOMPLEX_DIVISION_BY_ZERO = thm"HCOMPLEX_DIVISION_BY_ZERO";
  1886 val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
  1887 val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
  1888 val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
  1889 val hcomplex_inverse_not_zero = thm"hcomplex_inverse_not_zero";
  1890 val hcomplex_mult_not_zero = thm"hcomplex_mult_not_zero";
  1891 val hcomplex_mult_not_zeroE = thm"hcomplex_mult_not_zeroE";
  1892 val hcomplex_minus_inverse = thm"hcomplex_minus_inverse";
  1893 val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
  1894 val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
  1895 val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal";
  1896 val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
  1897 val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
  1898 val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
  1899 val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
  1900 val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
  1901 val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
  1902 val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
  1903 val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
  1904 val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
  1905 val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
  1906 val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
  1907 val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
  1908 val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
  1909 val hcmod = thm"hcmod";
  1910 val hcmod_zero = thm"hcmod_zero";
  1911 val hcmod_one = thm"hcmod_one";
  1912 val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
  1913 val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
  1914 val hcnj = thm"hcnj";
  1915 val inj_hcnj = thm"inj_hcnj";
  1916 val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
  1917 val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
  1918 val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
  1919 val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
  1920 val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
  1921 val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
  1922 val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
  1923 val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
  1924 val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
  1925 val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
  1926 val hcnj_one = thm"hcnj_one";
  1927 val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
  1928 val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
  1929 val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
  1930 val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
  1931 val hcomplex_mult_zero_iff = thm"hcomplex_mult_zero_iff";
  1932 val hcomplex_add_left_cancel_zero = thm"hcomplex_add_left_cancel_zero";
  1933 val hcomplex_diff_mult_distrib = thm"hcomplex_diff_mult_distrib";
  1934 val hcomplex_diff_mult_distrib2 = thm"hcomplex_diff_mult_distrib2";
  1935 val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
  1936 val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
  1937 val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
  1938 val hypreal_of_hypnat_ge_zero = thm"hypreal_of_hypnat_ge_zero";
  1939 val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
  1940 val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
  1941 val hcmod_minus = thm"hcmod_minus";
  1942 val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
  1943 val hcmod_ge_zero = thm"hcmod_ge_zero";
  1944 val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
  1945 val hcmod_mult = thm"hcmod_mult";
  1946 val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
  1947 val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
  1948 val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
  1949 val hcmod_triangle_squared = thm"hcmod_triangle_squared";
  1950 val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
  1951 val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
  1952 val hcmod_diff_commute = thm"hcmod_diff_commute";
  1953 val hcmod_add_less = thm"hcmod_add_less";
  1954 val hcmod_mult_less = thm"hcmod_mult_less";
  1955 val hcmod_diff_ineq = thm"hcmod_diff_ineq";
  1956 val hcpow = thm"hcpow";
  1957 val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
  1958 val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
  1959 val hcmod_hcpow = thm"hcmod_hcpow";
  1960 val hcomplexpow_minus = thm"hcomplexpow_minus";
  1961 val hcpow_minus = thm"hcpow_minus";
  1962 val hccomplex_inverse_minus = thm"hccomplex_inverse_minus";
  1963 val hcomplex_div_one = thm"hcomplex_div_one";
  1964 val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
  1965 val hcmod_divide = thm"hcmod_divide";
  1966 val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
  1967 val hcomplexpow_mult = thm"hcomplexpow_mult";
  1968 val hcpow_mult = thm"hcpow_mult";
  1969 val hcomplexpow_zero = thm"hcomplexpow_zero";
  1970 val hcpow_zero = thm"hcpow_zero";
  1971 val hcpow_zero2 = thm"hcpow_zero2";
  1972 val hcomplexpow_not_zero = thm"hcomplexpow_not_zero";
  1973 val hcpow_not_zero = thm"hcpow_not_zero";
  1974 val hcomplexpow_zero_zero = thm"hcomplexpow_zero_zero";
  1975 val hcpow_zero_zero = thm"hcpow_zero_zero";
  1976 val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
  1977 val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
  1978 val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
  1979 val hcomplex_mult_eq_zero_cancel1 = thm"hcomplex_mult_eq_zero_cancel1";
  1980 val hcomplex_mult_eq_zero_cancel2 = thm"hcomplex_mult_eq_zero_cancel2";
  1981 val hcomplex_mult_not_eq_zero_iff = thm"hcomplex_mult_not_eq_zero_iff";
  1982 val hcomplex_divide = thm"hcomplex_divide";
  1983 val hsgn = thm"hsgn";
  1984 val hsgn_zero = thm"hsgn_zero";
  1985 val hsgn_one = thm"hsgn_one";
  1986 val hsgn_minus = thm"hsgn_minus";
  1987 val hsgn_eq = thm"hsgn_eq";
  1988 val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
  1989 val complex_split2 = thm"complex_split2";
  1990 val hcomplex_split = thm"hcomplex_split";
  1991 val hRe_hcomplex_i = thm"hRe_hcomplex_i";
  1992 val hIm_hcomplex_i = thm"hIm_hcomplex_i";
  1993 val hcmod_i = thm"hcmod_i";
  1994 val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq";
  1995 val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq";
  1996 val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff";
  1997 val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA";
  1998 val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB";
  1999 val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC";
  2000 val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
  2001 val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a";
  2002 val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3";
  2003 val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a";
  2004 val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero";
  2005 val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero";
  2006 val hRe_hsgn = thm"hRe_hsgn";
  2007 val hIm_hsgn = thm"hIm_hsgn";
  2008 val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
  2009 val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split";
  2010 val hRe_mult_i_eq = thm"hRe_mult_i_eq";
  2011 val hIm_mult_i_eq = thm"hIm_mult_i_eq";
  2012 val hcmod_mult_i = thm"hcmod_mult_i";
  2013 val hcmod_mult_i2 = thm"hcmod_mult_i2";
  2014 val harg = thm"harg";
  2015 val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
  2016 val cos_harg_i_mult_zero2 = thm"cos_harg_i_mult_zero2";
  2017 val hcomplex_of_hypreal_not_zero_iff = thm"hcomplex_of_hypreal_not_zero_iff";
  2018 val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
  2019 val cos_harg_i_mult_zero3 = thm"cos_harg_i_mult_zero3";
  2020 val complex_split_polar2 = thm"complex_split_polar2";
  2021 val hcomplex_split_polar = thm"hcomplex_split_polar";
  2022 val hcis = thm"hcis";
  2023 val hcis_eq = thm"hcis_eq";
  2024 val hrcis = thm"hrcis";
  2025 val hrcis_Ex = thm"hrcis_Ex";
  2026 val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
  2027 val hRe_hrcis = thm"hRe_hrcis";
  2028 val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
  2029 val hIm_hrcis = thm"hIm_hrcis";
  2030 val hcmod_complex_polar = thm"hcmod_complex_polar";
  2031 val hcmod_hrcis = thm"hcmod_hrcis";
  2032 val hcis_hrcis_eq = thm"hcis_hrcis_eq";
  2033 val hrcis_mult = thm"hrcis_mult";
  2034 val hcis_mult = thm"hcis_mult";
  2035 val hcis_zero = thm"hcis_zero";
  2036 val hrcis_zero_mod = thm"hrcis_zero_mod";
  2037 val hrcis_zero_arg = thm"hrcis_zero_arg";
  2038 val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
  2039 val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
  2040 val hypreal_of_nat = thm"hypreal_of_nat";
  2041 val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
  2042 val NSDeMoivre = thm"NSDeMoivre";
  2043 val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
  2044 val NSDeMoivre_ext = thm"NSDeMoivre_ext";
  2045 val DeMoivre2 = thm"DeMoivre2";
  2046 val DeMoivre2_ext = thm"DeMoivre2_ext";
  2047 val hcis_inverse = thm"hcis_inverse";
  2048 val hrcis_inverse = thm"hrcis_inverse";
  2049 val hRe_hcis = thm"hRe_hcis";
  2050 val hIm_hcis = thm"hIm_hcis";
  2051 val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
  2052 val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
  2053 val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
  2054 val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
  2055 val hexpi_add = thm"hexpi_add";
  2056 val hcomplex_of_complex_add = thm"hcomplex_of_complex_add";
  2057 val hcomplex_of_complex_mult = thm"hcomplex_of_complex_mult";
  2058 val hcomplex_of_complex_eq_iff = thm"hcomplex_of_complex_eq_iff";
  2059 val hcomplex_of_complex_minus = thm"hcomplex_of_complex_minus";
  2060 val hcomplex_of_complex_one = thm"hcomplex_of_complex_one";
  2061 val hcomplex_of_complex_zero = thm"hcomplex_of_complex_zero";
  2062 val hcomplex_of_complex_zero_iff = thm"hcomplex_of_complex_zero_iff";
  2063 val hcomplex_of_complex_inverse = thm"hcomplex_of_complex_inverse";
  2064 val hcomplex_of_complex_divide = thm"hcomplex_of_complex_divide";
  2065 val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
  2066 val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
  2067 val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
  2068 
  2069 val hcomplex_add_ac = thms"hcomplex_add_ac";
  2070 val hcomplex_mult_ac = thms"hcomplex_mult_ac";
  2071 *}
  2072 
  2073 end