src/HOL/Complex/NSComplex.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 15169 2b5da07a0b89 permissions -rw-r--r--
import -> imports
```     1 (*  Title:       NSComplex.thy
```
```     2     ID:      \$Id\$
```
```     3     Author:      Jacques D. Fleuriot
```
```     4     Copyright:   2001  University of Edinburgh
```
```     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
```
```     6 *)
```
```     7
```
```     8 header{*Nonstandard Complex Numbers*}
```
```     9
```
```    10 theory NSComplex
```
```    11 imports Complex
```
```    12 begin
```
```    13
```
```    14 constdefs
```
```    15     hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
```
```    16     "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
```
```    17                         {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
```
```    18
```
```    19 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
```
```    20   by (auto simp add: quotient_def)
```
```    21
```
```    22 instance hcomplex :: "{zero, one, plus, times, minus, inverse, power}" ..
```
```    23
```
```    24 defs (overloaded)
```
```    25   hcomplex_zero_def:
```
```    26   "0 == Abs_hcomplex(hcomplexrel `` {%n. (0::complex)})"
```
```    27
```
```    28   hcomplex_one_def:
```
```    29   "1 == Abs_hcomplex(hcomplexrel `` {%n. (1::complex)})"
```
```    30
```
```    31
```
```    32   hcomplex_minus_def:
```
```    33   "- z == Abs_hcomplex(UN X: Rep_hcomplex(z).
```
```    34                        hcomplexrel `` {%n::nat. - (X n)})"
```
```    35
```
```    36   hcomplex_diff_def:
```
```    37   "w - z == w + -(z::hcomplex)"
```
```    38
```
```    39   hcinv_def:
```
```    40   "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
```
```    41                     hcomplexrel `` {%n. inverse(X n)})"
```
```    42
```
```    43 constdefs
```
```    44
```
```    45   hcomplex_of_complex :: "complex => hcomplex"
```
```    46   "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
```
```    47
```
```    48   (*--- real and Imaginary parts ---*)
```
```    49
```
```    50   hRe :: "hcomplex => hypreal"
```
```    51   "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
```
```    52
```
```    53   hIm :: "hcomplex => hypreal"
```
```    54   "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
```
```    55
```
```    56
```
```    57   (*----------- modulus ------------*)
```
```    58
```
```    59   hcmod :: "hcomplex => hypreal"
```
```    60   "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
```
```    61 			  hyprel `` {%n. cmod (X n)})"
```
```    62
```
```    63   (*------ imaginary unit ----------*)
```
```    64
```
```    65   iii :: hcomplex
```
```    66   "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})"
```
```    67
```
```    68   (*------- complex conjugate ------*)
```
```    69
```
```    70   hcnj :: "hcomplex => hcomplex"
```
```    71   "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})"
```
```    72
```
```    73   (*------------ Argand -------------*)
```
```    74
```
```    75   hsgn :: "hcomplex => hcomplex"
```
```    76   "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
```
```    77
```
```    78   harg :: "hcomplex => hypreal"
```
```    79   "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
```
```    80
```
```    81   (* abbreviation for (cos a + i sin a) *)
```
```    82   hcis :: "hypreal => hcomplex"
```
```    83   "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
```
```    84
```
```    85   (*----- injection from hyperreals -----*)
```
```    86
```
```    87   hcomplex_of_hypreal :: "hypreal => hcomplex"
```
```    88   "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
```
```    89 			       hcomplexrel `` {%n. complex_of_real (X n)})"
```
```    90
```
```    91   (* abbreviation for r*(cos a + i sin a) *)
```
```    92   hrcis :: "[hypreal, hypreal] => hcomplex"
```
```    93   "hrcis r a == hcomplex_of_hypreal r * hcis a"
```
```    94
```
```    95   (*------------ e ^ (x + iy) ------------*)
```
```    96
```
```    97   hexpi :: "hcomplex => hcomplex"
```
```    98   "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
```
```    99
```
```   100
```
```   101 constdefs
```
```   102   HComplex :: "[hypreal,hypreal] => hcomplex"
```
```   103    "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"
```
```   104
```
```   105
```
```   106 defs (overloaded)
```
```   107
```
```   108   (*----------- division ----------*)
```
```   109
```
```   110   hcomplex_divide_def:
```
```   111   "w / (z::hcomplex) == w * inverse z"
```
```   112
```
```   113   hcomplex_add_def:
```
```   114   "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
```
```   115 		      hcomplexrel `` {%n. X n + Y n})"
```
```   116
```
```   117   hcomplex_mult_def:
```
```   118   "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z).
```
```   119 		      hcomplexrel `` {%n. X n * Y n})"
```
```   120
```
```   121
```
```   122
```
```   123 consts
```
```   124   "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr 80)
```
```   125
```
```   126 defs
```
```   127   (* hypernatural powers of nonstandard complex numbers *)
```
```   128   hcpow_def:
```
```   129   "(z::hcomplex) hcpow (n::hypnat)
```
```   130       == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
```
```   131              hcomplexrel `` {%n. (X n) ^ (Y n)})"
```
```   132
```
```   133
```
```   134 lemma hcomplexrel_refl: "(x,x): hcomplexrel"
```
```   135 by (simp add: hcomplexrel_def)
```
```   136
```
```   137 lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
```
```   138 by (auto simp add: hcomplexrel_def eq_commute)
```
```   139
```
```   140 lemma hcomplexrel_trans:
```
```   141       "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
```
```   142 by (simp add: hcomplexrel_def, ultra)
```
```   143
```
```   144 lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
```
```   145 apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl)
```
```   146 apply (blast intro: hcomplexrel_sym hcomplexrel_trans)
```
```   147 done
```
```   148
```
```   149 lemmas equiv_hcomplexrel_iff =
```
```   150     eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
```
```   151
```
```   152 lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
```
```   153 by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast)
```
```   154
```
```   155 lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
```
```   156 apply (rule inj_on_inverseI)
```
```   157 apply (erule Abs_hcomplex_inverse)
```
```   158 done
```
```   159
```
```   160 declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp]
```
```   161         Abs_hcomplex_inverse [simp]
```
```   162
```
```   163 declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
```
```   164
```
```   165
```
```   166 lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
```
```   167 apply (rule inj_on_inverseI)
```
```   168 apply (rule Rep_hcomplex_inverse)
```
```   169 done
```
```   170
```
```   171 lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}"
```
```   172 by (simp add: hcomplexrel_def)
```
```   173
```
```   174 lemma hcomplex_empty_not_mem [simp]: "{} \<notin> hcomplex"
```
```   175 apply (simp add: hcomplex_def hcomplexrel_def)
```
```   176 apply (auto elim!: quotientE)
```
```   177 done
```
```   178
```
```   179 lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \<noteq> {}"
```
```   180 by (cut_tac x = x in Rep_hcomplex, auto)
```
```   181
```
```   182 lemma eq_Abs_hcomplex:
```
```   183     "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
```
```   184 apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
```
```   185 apply (drule_tac f = Abs_hcomplex in arg_cong)
```
```   186 apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
```
```   187 done
```
```   188
```
```   189 theorem hcomplex_cases [case_names Abs_hcomplex, cases type: hcomplex]:
```
```   190     "(!!x. z = Abs_hcomplex(hcomplexrel``{x}) ==> P) ==> P"
```
```   191 by (rule eq_Abs_hcomplex [of z], blast)
```
```   192
```
```   193 lemma hcomplexrel_iff [simp]:
```
```   194    "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
```
```   195 by (simp add: hcomplexrel_def)
```
```   196
```
```   197
```
```   198 subsection{*Properties of Nonstandard Real and Imaginary Parts*}
```
```   199
```
```   200 lemma hRe:
```
```   201      "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
```
```   202       Abs_hypreal(hyprel `` {%n. Re(X n)})"
```
```   203 apply (simp add: hRe_def)
```
```   204 apply (rule_tac f = Abs_hypreal in arg_cong)
```
```   205 apply (auto iff: hcomplexrel_iff, ultra)
```
```   206 done
```
```   207
```
```   208 lemma hIm:
```
```   209      "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
```
```   210       Abs_hypreal(hyprel `` {%n. Im(X n)})"
```
```   211 apply (simp add: hIm_def)
```
```   212 apply (rule_tac f = Abs_hypreal in arg_cong)
```
```   213 apply (auto iff: hcomplexrel_iff, ultra)
```
```   214 done
```
```   215
```
```   216 lemma hcomplex_hRe_hIm_cancel_iff:
```
```   217      "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
```
```   218 apply (cases z, cases w)
```
```   219 apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
```
```   220 apply (ultra+)
```
```   221 done
```
```   222
```
```   223 lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
```
```   224 by (simp add: hcomplex_hRe_hIm_cancel_iff)
```
```   225
```
```   226 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
```
```   227 by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
```
```   228
```
```   229 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
```
```   230 by (simp add: hcomplex_zero_def hIm hypreal_zero_num)
```
```   231
```
```   232 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
```
```   233 by (simp add: hcomplex_one_def hRe hypreal_one_num)
```
```   234
```
```   235 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
```
```   236 by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num)
```
```   237
```
```   238
```
```   239 subsection{*Addition for Nonstandard Complex Numbers*}
```
```   240
```
```   241 lemma hcomplex_add_congruent2:
```
```   242     "congruent2 hcomplexrel hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
```
```   243 by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra)
```
```   244
```
```   245 lemma hcomplex_add:
```
```   246   "Abs_hcomplex(hcomplexrel``{%n. X n}) +
```
```   247    Abs_hcomplex(hcomplexrel``{%n. Y n}) =
```
```   248      Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
```
```   249 apply (simp add: hcomplex_add_def)
```
```   250 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   251 apply (auto simp add: iff: hcomplexrel_iff, ultra)
```
```   252 done
```
```   253
```
```   254 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
```
```   255 apply (cases z, cases w)
```
```   256 apply (simp add: complex_add_commute hcomplex_add)
```
```   257 done
```
```   258
```
```   259 lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
```
```   260 apply (cases z1, cases z2, cases z3)
```
```   261 apply (simp add: hcomplex_add complex_add_assoc)
```
```   262 done
```
```   263
```
```   264 lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
```
```   265 apply (cases z)
```
```   266 apply (simp add: hcomplex_zero_def hcomplex_add)
```
```   267 done
```
```   268
```
```   269 lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
```
```   270 by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
```
```   271
```
```   272 lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
```
```   273 apply (cases x, cases y)
```
```   274 apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
```
```   275 done
```
```   276
```
```   277 lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
```
```   278 apply (cases x, cases y)
```
```   279 apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
```
```   280 done
```
```   281
```
```   282
```
```   283 subsection{*Additive Inverse on Nonstandard Complex Numbers*}
```
```   284
```
```   285 lemma hcomplex_minus_congruent:
```
```   286      "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
```
```   287 by (simp add: congruent_def)
```
```   288
```
```   289 lemma hcomplex_minus:
```
```   290   "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```   291       Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
```
```   292 apply (simp add: hcomplex_minus_def)
```
```   293 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   294 apply (auto iff: hcomplexrel_iff, ultra)
```
```   295 done
```
```   296
```
```   297 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
```
```   298 apply (cases z)
```
```   299 apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
```
```   300 done
```
```   301
```
```   302
```
```   303 subsection{*Multiplication for Nonstandard Complex Numbers*}
```
```   304
```
```   305 lemma hcomplex_mult:
```
```   306   "Abs_hcomplex(hcomplexrel``{%n. X n}) *
```
```   307      Abs_hcomplex(hcomplexrel``{%n. Y n}) =
```
```   308      Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
```
```   309 apply (simp add: hcomplex_mult_def)
```
```   310 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   311 apply (auto iff: hcomplexrel_iff, ultra)
```
```   312 done
```
```   313
```
```   314 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
```
```   315 apply (cases w, cases z)
```
```   316 apply (simp add: hcomplex_mult complex_mult_commute)
```
```   317 done
```
```   318
```
```   319 lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
```
```   320 apply (cases u, cases v, cases w)
```
```   321 apply (simp add: hcomplex_mult complex_mult_assoc)
```
```   322 done
```
```   323
```
```   324 lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
```
```   325 apply (cases z)
```
```   326 apply (simp add: hcomplex_one_def hcomplex_mult)
```
```   327 done
```
```   328
```
```   329 lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
```
```   330 apply (cases z)
```
```   331 apply (simp add: hcomplex_zero_def hcomplex_mult)
```
```   332 done
```
```   333
```
```   334 lemma hcomplex_add_mult_distrib:
```
```   335      "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
```
```   336 apply (cases z1, cases z2, cases w)
```
```   337 apply (simp add: hcomplex_mult hcomplex_add left_distrib)
```
```   338 done
```
```   339
```
```   340 lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
```
```   341 by (simp add: hcomplex_zero_def hcomplex_one_def)
```
```   342
```
```   343 declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
```
```   344
```
```   345
```
```   346 subsection{*Inverse of Nonstandard Complex Number*}
```
```   347
```
```   348 lemma hcomplex_inverse:
```
```   349   "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```   350       Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
```
```   351 apply (simp add: hcinv_def)
```
```   352 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   353 apply (auto iff: hcomplexrel_iff, ultra)
```
```   354 done
```
```   355
```
```   356 lemma hcomplex_mult_inv_left:
```
```   357       "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
```
```   358 apply (cases z)
```
```   359 apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
```
```   360 apply (rule ccontr)
```
```   361 apply (drule left_inverse, auto)
```
```   362 done
```
```   363
```
```   364 subsection {* The Field of Nonstandard Complex Numbers *}
```
```   365
```
```   366 instance hcomplex :: field
```
```   367 proof
```
```   368   fix z u v w :: hcomplex
```
```   369   show "(u + v) + w = u + (v + w)"
```
```   370     by (simp add: hcomplex_add_assoc)
```
```   371   show "z + w = w + z"
```
```   372     by (simp add: hcomplex_add_commute)
```
```   373   show "0 + z = z"
```
```   374     by (simp add: hcomplex_add_zero_left)
```
```   375   show "-z + z = 0"
```
```   376     by (simp add: hcomplex_add_minus_left)
```
```   377   show "z - w = z + -w"
```
```   378     by (simp add: hcomplex_diff_def)
```
```   379   show "(u * v) * w = u * (v * w)"
```
```   380     by (simp add: hcomplex_mult_assoc)
```
```   381   show "z * w = w * z"
```
```   382     by (simp add: hcomplex_mult_commute)
```
```   383   show "1 * z = z"
```
```   384     by (simp add: hcomplex_mult_one_left)
```
```   385   show "0 \<noteq> (1::hcomplex)"
```
```   386     by (rule hcomplex_zero_not_eq_one)
```
```   387   show "(u + v) * w = u * w + v * w"
```
```   388     by (simp add: hcomplex_add_mult_distrib)
```
```   389   show "z / w = z * inverse w"
```
```   390     by (simp add: hcomplex_divide_def)
```
```   391   assume "w \<noteq> 0"
```
```   392   thus "inverse w * w = 1"
```
```   393     by (rule hcomplex_mult_inv_left)
```
```   394 qed
```
```   395
```
```   396 instance hcomplex :: division_by_zero
```
```   397 proof
```
```   398   show "inverse 0 = (0::hcomplex)"
```
```   399     by (simp add: hcomplex_inverse hcomplex_zero_def)
```
```   400 qed
```
```   401
```
```   402
```
```   403 subsection{*More Minus Laws*}
```
```   404
```
```   405 lemma hRe_minus: "hRe(-z) = - hRe(z)"
```
```   406 apply (cases z)
```
```   407 apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
```
```   408 done
```
```   409
```
```   410 lemma hIm_minus: "hIm(-z) = - hIm(z)"
```
```   411 apply (cases z)
```
```   412 apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
```
```   413 done
```
```   414
```
```   415 lemma hcomplex_add_minus_eq_minus:
```
```   416       "x + y = (0::hcomplex) ==> x = -y"
```
```   417 apply (drule OrderedGroup.equals_zero_I)
```
```   418 apply (simp add: minus_equation_iff [of x y])
```
```   419 done
```
```   420
```
```   421 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
```
```   422 by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
```
```   423
```
```   424 lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
```
```   425 by (simp add: mult_assoc [symmetric])
```
```   426
```
```   427 lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
```
```   428 by (simp add: iii_def hcomplex_zero_def)
```
```   429
```
```   430
```
```   431 subsection{*More Multiplication Laws*}
```
```   432
```
```   433 lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
```
```   434 by (rule OrderedGroup.mult_1_right)
```
```   435
```
```   436 lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
```
```   437 by simp
```
```   438
```
```   439 lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z"
```
```   440 by (subst hcomplex_mult_commute, simp)
```
```   441
```
```   442 lemma hcomplex_mult_left_cancel:
```
```   443      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
```
```   444 by (simp add: field_mult_cancel_left)
```
```   445
```
```   446 lemma hcomplex_mult_right_cancel:
```
```   447      "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
```
```   448 by (simp add: Ring_and_Field.field_mult_cancel_right)
```
```   449
```
```   450
```
```   451 subsection{*Subraction and Division*}
```
```   452
```
```   453 lemma hcomplex_diff:
```
```   454  "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
```
```   455   Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
```
```   456 by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def)
```
```   457
```
```   458 lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
```
```   459 by (rule OrderedGroup.diff_eq_eq)
```
```   460
```
```   461 lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
```
```   462 by (rule Ring_and_Field.add_divide_distrib)
```
```   463
```
```   464
```
```   465 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
```
```   466
```
```   467 lemma hcomplex_of_hypreal:
```
```   468   "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
```
```   469       Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
```
```   470 apply (simp add: hcomplex_of_hypreal_def)
```
```   471 apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
```
```   472 done
```
```   473
```
```   474 lemma hcomplex_of_hypreal_cancel_iff [iff]:
```
```   475      "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
```
```   476 apply (cases x, cases y)
```
```   477 apply (simp add: hcomplex_of_hypreal)
```
```   478 done
```
```   479
```
```   480 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
```
```   481 by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
```
```   482
```
```   483 lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
```
```   484 by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
```
```   485
```
```   486 lemma hcomplex_of_hypreal_minus [simp]:
```
```   487      "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
```
```   488 apply (cases x)
```
```   489 apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
```
```   490 done
```
```   491
```
```   492 lemma hcomplex_of_hypreal_inverse [simp]:
```
```   493      "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
```
```   494 apply (cases x)
```
```   495 apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
```
```   496 done
```
```   497
```
```   498 lemma hcomplex_of_hypreal_add [simp]:
```
```   499   "hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
```
```   500 apply (cases x, cases y)
```
```   501 apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
```
```   502 done
```
```   503
```
```   504 lemma hcomplex_of_hypreal_diff [simp]:
```
```   505      "hcomplex_of_hypreal (x - y) =
```
```   506       hcomplex_of_hypreal x - hcomplex_of_hypreal y "
```
```   507 by (simp add: hcomplex_diff_def hypreal_diff_def)
```
```   508
```
```   509 lemma hcomplex_of_hypreal_mult [simp]:
```
```   510   "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
```
```   511 apply (cases x, cases y)
```
```   512 apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
```
```   513 done
```
```   514
```
```   515 lemma hcomplex_of_hypreal_divide [simp]:
```
```   516   "hcomplex_of_hypreal(x/y) = hcomplex_of_hypreal x / hcomplex_of_hypreal y"
```
```   517 apply (simp add: hcomplex_divide_def)
```
```   518 apply (case_tac "y=0", simp)
```
```   519 apply (simp add: hypreal_divide_def)
```
```   520 done
```
```   521
```
```   522 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
```
```   523 apply (cases z)
```
```   524 apply (auto simp add: hcomplex_of_hypreal hRe)
```
```   525 done
```
```   526
```
```   527 lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
```
```   528 apply (cases z)
```
```   529 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
```
```   530 done
```
```   531
```
```   532 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
```
```   533      "hcomplex_of_hypreal epsilon \<noteq> 0"
```
```   534 by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
```
```   535
```
```   536
```
```   537 subsection{*HComplex theorems*}
```
```   538
```
```   539 lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
```
```   540 apply (cases x, cases y)
```
```   541 apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
```
```   542 done
```
```   543
```
```   544 lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
```
```   545 apply (cases x, cases y)
```
```   546 apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
```
```   547 done
```
```   548
```
```   549 text{*Relates the two nonstandard constructions*}
```
```   550 lemma HComplex_eq_Abs_hcomplex_Complex:
```
```   551      "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
```
```   552       Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
```
```   553 by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm)
```
```   554
```
```   555 lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
```
```   556 by (simp add: hcomplex_equality)
```
```   557
```
```   558 lemma hcomplex_induct [case_names rect, induct type: hcomplex]:
```
```   559      "(\<And>x y. P (HComplex x y)) ==> P z"
```
```   560 by (rule hcomplex_surj [THEN subst], blast)
```
```   561
```
```   562
```
```   563 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
```
```   564
```
```   565 lemma hcmod:
```
```   566   "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```   567       Abs_hypreal(hyprel `` {%n. cmod (X n)})"
```
```   568
```
```   569 apply (simp add: hcmod_def)
```
```   570 apply (rule_tac f = Abs_hypreal in arg_cong)
```
```   571 apply (auto iff: hcomplexrel_iff, ultra)
```
```   572 done
```
```   573
```
```   574 lemma hcmod_zero [simp]: "hcmod(0) = 0"
```
```   575 by (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
```
```   576
```
```   577 lemma hcmod_one [simp]: "hcmod(1) = 1"
```
```   578 by (simp add: hcomplex_one_def hcmod hypreal_one_num)
```
```   579
```
```   580 lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
```
```   581 apply (cases x)
```
```   582 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
```
```   583 done
```
```   584
```
```   585 lemma hcomplex_of_hypreal_abs:
```
```   586      "hcomplex_of_hypreal (abs x) =
```
```   587       hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
```
```   588 by simp
```
```   589
```
```   590 lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')"
```
```   591 apply (rule iffI)
```
```   592  prefer 2 apply simp
```
```   593 apply (simp add: HComplex_def iii_def)
```
```   594 apply (cases x, cases y, cases x', cases y')
```
```   595 apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
```
```   596 apply (ultra+)
```
```   597 done
```
```   598
```
```   599 lemma HComplex_add [simp]:
```
```   600      "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
```
```   601 by (simp add: HComplex_def add_ac right_distrib)
```
```   602
```
```   603 lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
```
```   604 by (simp add: HComplex_def hcomplex_of_hypreal_minus)
```
```   605
```
```   606 lemma HComplex_diff [simp]:
```
```   607      "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
```
```   608 by (simp add: diff_minus)
```
```   609
```
```   610 lemma HComplex_mult [simp]:
```
```   611   "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
```
```   612 by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus
```
```   613        add_ac mult_ac right_distrib)
```
```   614
```
```   615 (*HComplex_inverse is proved below*)
```
```   616
```
```   617 lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0"
```
```   618 by (simp add: HComplex_def)
```
```   619
```
```   620 lemma HComplex_add_hcomplex_of_hypreal [simp]:
```
```   621      "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
```
```   622 by (simp add: hcomplex_of_hypreal_eq)
```
```   623
```
```   624 lemma hcomplex_of_hypreal_add_HComplex [simp]:
```
```   625      "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
```
```   626 by (simp add: i_def hcomplex_of_hypreal_eq)
```
```   627
```
```   628 lemma HComplex_mult_hcomplex_of_hypreal:
```
```   629      "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
```
```   630 by (simp add: hcomplex_of_hypreal_eq)
```
```   631
```
```   632 lemma hcomplex_of_hypreal_mult_HComplex:
```
```   633      "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
```
```   634 by (simp add: i_def hcomplex_of_hypreal_eq)
```
```   635
```
```   636 lemma i_hcomplex_of_hypreal [simp]:
```
```   637      "iii * hcomplex_of_hypreal r = HComplex 0 r"
```
```   638 by (simp add: HComplex_def)
```
```   639
```
```   640 lemma hcomplex_of_hypreal_i [simp]:
```
```   641      "hcomplex_of_hypreal r * iii = HComplex 0 r"
```
```   642 by (simp add: mult_commute)
```
```   643
```
```   644
```
```   645 subsection{*Conjugation*}
```
```   646
```
```   647 lemma hcnj:
```
```   648   "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```   649    Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
```
```   650 apply (simp add: hcnj_def)
```
```   651 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   652 apply (auto iff: hcomplexrel_iff, ultra)
```
```   653 done
```
```   654
```
```   655 lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
```
```   656 apply (cases x, cases y)
```
```   657 apply (simp add: hcnj)
```
```   658 done
```
```   659
```
```   660 lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
```
```   661 apply (cases z)
```
```   662 apply (simp add: hcnj)
```
```   663 done
```
```   664
```
```   665 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
```
```   666      "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
```
```   667 apply (cases x)
```
```   668 apply (simp add: hcnj hcomplex_of_hypreal)
```
```   669 done
```
```   670
```
```   671 lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
```
```   672 apply (cases z)
```
```   673 apply (simp add: hcnj hcmod)
```
```   674 done
```
```   675
```
```   676 lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
```
```   677 apply (cases z)
```
```   678 apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
```
```   679 done
```
```   680
```
```   681 lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
```
```   682 apply (cases z)
```
```   683 apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
```
```   684 done
```
```   685
```
```   686 lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
```
```   687 apply (cases z, cases w)
```
```   688 apply (simp add: hcnj hcomplex_add complex_cnj_add)
```
```   689 done
```
```   690
```
```   691 lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
```
```   692 apply (cases z, cases w)
```
```   693 apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
```
```   694 done
```
```   695
```
```   696 lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
```
```   697 apply (cases z, cases w)
```
```   698 apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
```
```   699 done
```
```   700
```
```   701 lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
```
```   702 by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse)
```
```   703
```
```   704 lemma hcnj_one [simp]: "hcnj 1 = 1"
```
```   705 by (simp add: hcomplex_one_def hcnj)
```
```   706
```
```   707 lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
```
```   708 by (simp add: hcomplex_zero_def hcnj)
```
```   709
```
```   710 lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
```
```   711 apply (cases z)
```
```   712 apply (simp add: hcomplex_zero_def hcnj)
```
```   713 done
```
```   714
```
```   715 lemma hcomplex_mult_hcnj:
```
```   716      "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
```
```   717 apply (cases z)
```
```   718 apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
```
```   719                       hypreal_mult complex_mult_cnj numeral_2_eq_2)
```
```   720 done
```
```   721
```
```   722
```
```   723 subsection{*More Theorems about the Function @{term hcmod}*}
```
```   724
```
```   725 lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
```
```   726 apply (cases x)
```
```   727 apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
```
```   728 done
```
```   729
```
```   730 lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
```
```   731      "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
```
```   732 apply (simp add: abs_if linorder_not_less)
```
```   733 done
```
```   734
```
```   735 lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
```
```   736      "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
```
```   737 apply (simp add: abs_if linorder_not_less)
```
```   738 done
```
```   739
```
```   740 lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
```
```   741 apply (cases x)
```
```   742 apply (simp add: hcmod hcomplex_minus)
```
```   743 done
```
```   744
```
```   745 lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
```
```   746 apply (cases z)
```
```   747 apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
```
```   748 done
```
```   749
```
```   750 lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
```
```   751 apply (cases x)
```
```   752 apply (simp add: hcmod hypreal_zero_num hypreal_le)
```
```   753 done
```
```   754
```
```   755 lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
```
```   756 by (simp add: abs_if linorder_not_less)
```
```   757
```
```   758 lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
```
```   759 apply (cases x, cases y)
```
```   760 apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
```
```   761 done
```
```   762
```
```   763 lemma hcmod_add_squared_eq:
```
```   764      "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
```
```   765 apply (cases x, cases y)
```
```   766 apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
```
```   767                       numeral_2_eq_2 realpow_two [symmetric]
```
```   768                   del: realpow_Suc)
```
```   769 apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
```
```   770                  hypreal_add [symmetric] hypreal_mult [symmetric]
```
```   771                  hypreal_of_real_def [symmetric])
```
```   772 done
```
```   773
```
```   774 lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
```
```   775 apply (cases x, cases y)
```
```   776 apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
```
```   777 done
```
```   778
```
```   779 lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \<le> hcmod(x * y)"
```
```   780 apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod)
```
```   781 apply (simp add: hcmod_mult)
```
```   782 done
```
```   783
```
```   784 lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
```
```   785 apply (cases x, cases y)
```
```   786 apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
```
```   787                       hypreal_le realpow_two [symmetric] numeral_2_eq_2
```
```   788             del: realpow_Suc)
```
```   789 apply (simp add: numeral_2_eq_2 [symmetric])
```
```   790 done
```
```   791
```
```   792 lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
```
```   793 apply (cases x, cases y)
```
```   794 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
```
```   795 done
```
```   796
```
```   797 lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \<le> hcmod a"
```
```   798 apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
```
```   799 apply (simp add: add_ac)
```
```   800 done
```
```   801
```
```   802 lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
```
```   803 apply (cases x, cases y)
```
```   804 apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
```
```   805 done
```
```   806
```
```   807 lemma hcmod_add_less:
```
```   808      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
```
```   809 apply (cases x, cases y, cases r, cases s)
```
```   810 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
```
```   811 apply (auto intro: complex_mod_add_less)
```
```   812 done
```
```   813
```
```   814 lemma hcmod_mult_less:
```
```   815      "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
```
```   816 apply (cases x, cases y, cases r, cases s)
```
```   817 apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
```
```   818 apply (auto intro: complex_mod_mult_less)
```
```   819 done
```
```   820
```
```   821 lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
```
```   822 apply (cases a, cases b)
```
```   823 apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
```
```   824 done
```
```   825
```
```   826
```
```   827 subsection{*A Few Nonlinear Theorems*}
```
```   828
```
```   829 lemma hcpow:
```
```   830   "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
```
```   831    Abs_hypnat(hypnatrel``{%n. Y n}) =
```
```   832    Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
```
```   833 apply (simp add: hcpow_def)
```
```   834 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   835 apply (auto iff: hcomplexrel_iff, ultra)
```
```   836 done
```
```   837
```
```   838 lemma hcomplex_of_hypreal_hyperpow:
```
```   839      "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
```
```   840 apply (cases x, cases n)
```
```   841 apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
```
```   842 done
```
```   843
```
```   844 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
```
```   845 apply (cases x, cases n)
```
```   846 apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
```
```   847 done
```
```   848
```
```   849 lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
```
```   850 apply (case_tac "x = 0", simp)
```
```   851 apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
```
```   852 apply (auto simp add: hcmod_mult [symmetric])
```
```   853 done
```
```   854
```
```   855 lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
```
```   856 by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse)
```
```   857
```
```   858
```
```   859 subsection{*Exponentiation*}
```
```   860
```
```   861 primrec
```
```   862      hcomplexpow_0:   "z ^ 0       = 1"
```
```   863      hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
```
```   864
```
```   865 instance hcomplex :: recpower
```
```   866 proof
```
```   867   fix z :: hcomplex
```
```   868   fix n :: nat
```
```   869   show "z^0 = 1" by simp
```
```   870   show "z^(Suc n) = z * (z^n)" by simp
```
```   871 qed
```
```   872
```
```   873 lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
```
```   874 by (simp add: power2_eq_square)
```
```   875
```
```   876
```
```   877 lemma hcomplex_of_hypreal_pow:
```
```   878      "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
```
```   879 apply (induct_tac "n")
```
```   880 apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
```
```   881 done
```
```   882
```
```   883 lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
```
```   884 apply (induct_tac "n")
```
```   885 apply (auto simp add: hcomplex_hcnj_mult)
```
```   886 done
```
```   887
```
```   888 lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
```
```   889 apply (induct_tac "n")
```
```   890 apply (auto simp add: hcmod_mult)
```
```   891 done
```
```   892
```
```   893 lemma hcpow_minus:
```
```   894      "(-x::hcomplex) hcpow n =
```
```   895       (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
```
```   896 apply (cases x, cases n)
```
```   897 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
```
```   898 apply (auto simp add: neg_power_if, ultra)
```
```   899 done
```
```   900
```
```   901 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
```
```   902 apply (cases r, cases s, cases n)
```
```   903 apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
```
```   904 done
```
```   905
```
```   906 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
```
```   907 apply (simp add: hcomplex_zero_def hypnat_one_def, cases n)
```
```   908 apply (simp add: hcpow hypnat_add)
```
```   909 done
```
```   910
```
```   911 lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
```
```   912 by (simp add: hSuc_def)
```
```   913
```
```   914 lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
```
```   915 apply (cases r, cases n)
```
```   916 apply (auto simp add: hcpow hcomplex_zero_def, ultra)
```
```   917 done
```
```   918
```
```   919 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
```
```   920 by (blast intro: ccontr dest: hcpow_not_zero)
```
```   921
```
```   922 lemma hcomplex_divide:
```
```   923   "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
```
```   924    Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
```
```   925 by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult)
```
```   926
```
```   927
```
```   928
```
```   929
```
```   930 subsection{*The Function @{term hsgn}*}
```
```   931
```
```   932 lemma hsgn:
```
```   933   "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```   934       Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
```
```   935 apply (simp add: hsgn_def)
```
```   936 apply (rule_tac f = Abs_hcomplex in arg_cong)
```
```   937 apply (auto iff: hcomplexrel_iff, ultra)
```
```   938 done
```
```   939
```
```   940 lemma hsgn_zero [simp]: "hsgn 0 = 0"
```
```   941 by (simp add: hcomplex_zero_def hsgn)
```
```   942
```
```   943 lemma hsgn_one [simp]: "hsgn 1 = 1"
```
```   944 by (simp add: hcomplex_one_def hsgn)
```
```   945
```
```   946 lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
```
```   947 apply (cases z)
```
```   948 apply (simp add: hsgn hcomplex_minus sgn_minus)
```
```   949 done
```
```   950
```
```   951 lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
```
```   952 apply (cases z)
```
```   953 apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
```
```   954 done
```
```   955
```
```   956
```
```   957 lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
```
```   958 apply (cases x, cases y)
```
```   959 apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun
```
```   960                  hypreal_mult hypreal_add hcmod numeral_2_eq_2)
```
```   961 done
```
```   962
```
```   963 lemma hcomplex_eq_cancel_iff1 [simp]:
```
```   964      "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
```
```   965 by (simp add: hcomplex_of_hypreal_eq)
```
```   966
```
```   967 lemma hcomplex_eq_cancel_iff2 [simp]:
```
```   968      "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
```
```   969 by (simp add: hcomplex_of_hypreal_eq)
```
```   970
```
```   971 lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
```
```   972 by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
```
```   973
```
```   974 lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
```
```   975 by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
```
```   976
```
```   977 lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
```
```   978 by (insert hcomplex_of_hypreal_i [of 1], simp)
```
```   979
```
```   980 lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
```
```   981 by (simp add: i_eq_HComplex_0_1)
```
```   982
```
```   983 lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
```
```   984 apply (cases z)
```
```   985 apply (simp add: hsgn hcmod hRe hypreal_divide)
```
```   986 done
```
```   987
```
```   988 lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
```
```   989 apply (cases z)
```
```   990 apply (simp add: hsgn hcmod hIm hypreal_divide)
```
```   991 done
```
```   992
```
```   993 (*????move to RealDef????*)
```
```   994 lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
```
```   995 by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
```
```   996
```
```   997 lemma hcomplex_inverse_complex_split:
```
```   998      "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
```
```   999       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
```
```  1000       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
```
```  1001 apply (cases x, cases y)
```
```  1002 apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
```
```  1003          starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
```
```  1004          hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
```
```  1005 apply (simp add: diff_minus)
```
```  1006 done
```
```  1007
```
```  1008 lemma HComplex_inverse:
```
```  1009      "inverse (HComplex x y) =
```
```  1010       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
```
```  1011 by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
```
```  1012
```
```  1013
```
```  1014
```
```  1015 lemma hRe_mult_i_eq[simp]:
```
```  1016     "hRe (iii * hcomplex_of_hypreal y) = 0"
```
```  1017 apply (simp add: iii_def, cases y)
```
```  1018 apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
```
```  1019 done
```
```  1020
```
```  1021 lemma hIm_mult_i_eq [simp]:
```
```  1022     "hIm (iii * hcomplex_of_hypreal y) = y"
```
```  1023 apply (simp add: iii_def, cases y)
```
```  1024 apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
```
```  1025 done
```
```  1026
```
```  1027 lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
```
```  1028 apply (cases y)
```
```  1029 apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
```
```  1030 done
```
```  1031
```
```  1032 lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
```
```  1033 by (simp only: hcmod_mult_i hcomplex_mult_commute)
```
```  1034
```
```  1035 (*---------------------------------------------------------------------------*)
```
```  1036 (*  harg                                                                     *)
```
```  1037 (*---------------------------------------------------------------------------*)
```
```  1038
```
```  1039 lemma harg:
```
```  1040   "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
```
```  1041       Abs_hypreal(hyprel `` {%n. arg (X n)})"
```
```  1042 apply (simp add: harg_def)
```
```  1043 apply (rule_tac f = Abs_hypreal in arg_cong)
```
```  1044 apply (auto iff: hcomplexrel_iff, ultra)
```
```  1045 done
```
```  1046
```
```  1047 lemma cos_harg_i_mult_zero_pos:
```
```  1048      "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
```
```  1049 apply (cases y)
```
```  1050 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
```
```  1051                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
```
```  1052 done
```
```  1053
```
```  1054 lemma cos_harg_i_mult_zero_neg:
```
```  1055      "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
```
```  1056 apply (cases y)
```
```  1057 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
```
```  1058                  hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
```
```  1059 done
```
```  1060
```
```  1061 lemma cos_harg_i_mult_zero [simp]:
```
```  1062      "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
```
```  1063 by (auto simp add: linorder_neq_iff
```
```  1064                    cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
```
```  1065
```
```  1066 lemma hcomplex_of_hypreal_zero_iff [simp]:
```
```  1067      "(hcomplex_of_hypreal y = 0) = (y = 0)"
```
```  1068 apply (cases y)
```
```  1069 apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
```
```  1070 done
```
```  1071
```
```  1072
```
```  1073 subsection{*Polar Form for Nonstandard Complex Numbers*}
```
```  1074
```
```  1075 lemma complex_split_polar2:
```
```  1076      "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
```
```  1077 by (blast intro: complex_split_polar)
```
```  1078
```
```  1079 lemma lemma_hypreal_P_EX2:
```
```  1080      "(\<exists>(x::hypreal) y. P x y) =
```
```  1081       (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
```
```  1082 apply auto
```
```  1083 apply (rule_tac z = x in eq_Abs_hypreal)
```
```  1084 apply (rule_tac z = y in eq_Abs_hypreal, auto)
```
```  1085 done
```
```  1086
```
```  1087 lemma hcomplex_split_polar:
```
```  1088   "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
```
```  1089 apply (cases z)
```
```  1090 apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
```
```  1091 apply (cut_tac z = x in complex_split_polar2)
```
```  1092 apply (drule choice, safe)+
```
```  1093 apply (rule_tac x = f in exI)
```
```  1094 apply (rule_tac x = fa in exI, auto)
```
```  1095 done
```
```  1096
```
```  1097 lemma hcis:
```
```  1098   "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
```
```  1099       Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
```
```  1100 apply (simp add: hcis_def)
```
```  1101 apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
```
```  1102 done
```
```  1103
```
```  1104 lemma hcis_eq:
```
```  1105    "hcis a =
```
```  1106     (hcomplex_of_hypreal(( *f* cos) a) +
```
```  1107     iii * hcomplex_of_hypreal(( *f* sin) a))"
```
```  1108 apply (cases a)
```
```  1109 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
```
```  1110 done
```
```  1111
```
```  1112 lemma hrcis:
```
```  1113   "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
```
```  1114       Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
```
```  1115 by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
```
```  1116
```
```  1117 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
```
```  1118 apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
```
```  1119 apply (rule hcomplex_split_polar)
```
```  1120 done
```
```  1121
```
```  1122 lemma hRe_hcomplex_polar [simp]:
```
```  1123      "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
```
```  1124       r * ( *f* cos) a"
```
```  1125 by (simp add: hcomplex_of_hypreal_mult_HComplex)
```
```  1126
```
```  1127 lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
```
```  1128 by (simp add: hrcis_def hcis_eq)
```
```  1129
```
```  1130 lemma hIm_hcomplex_polar [simp]:
```
```  1131      "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
```
```  1132       r * ( *f* sin) a"
```
```  1133 by (simp add: hcomplex_of_hypreal_mult_HComplex)
```
```  1134
```
```  1135 lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
```
```  1136 by (simp add: hrcis_def hcis_eq)
```
```  1137
```
```  1138
```
```  1139 lemma hcmod_unit_one [simp]:
```
```  1140      "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
```
```  1141 apply (cases a)
```
```  1142 apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal
```
```  1143                  hcomplex_mult hcmod hcomplex_add hypreal_one_def)
```
```  1144 done
```
```  1145
```
```  1146 lemma hcmod_complex_polar [simp]:
```
```  1147      "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
```
```  1148       abs r"
```
```  1149 apply (simp only: hcmod_mult hcmod_unit_one, simp)
```
```  1150 done
```
```  1151
```
```  1152 lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
```
```  1153 by (simp add: hrcis_def hcis_eq)
```
```  1154
```
```  1155 (*---------------------------------------------------------------------------*)
```
```  1156 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
```
```  1157 (*---------------------------------------------------------------------------*)
```
```  1158
```
```  1159 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
```
```  1160 by (simp add: hrcis_def)
```
```  1161 declare hcis_hrcis_eq [symmetric, simp]
```
```  1162
```
```  1163 lemma hrcis_mult:
```
```  1164   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
```
```  1165 apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
```
```  1166 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
```
```  1167                       hcomplex_mult cis_mult [symmetric])
```
```  1168 done
```
```  1169
```
```  1170 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
```
```  1171 apply (cases a, cases b)
```
```  1172 apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
```
```  1173 done
```
```  1174
```
```  1175 lemma hcis_zero [simp]: "hcis 0 = 1"
```
```  1176 by (simp add: hcomplex_one_def hcis hypreal_zero_num)
```
```  1177
```
```  1178 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
```
```  1179 apply (simp add: hcomplex_zero_def, cases a)
```
```  1180 apply (simp add: hrcis hypreal_zero_num)
```
```  1181 done
```
```  1182
```
```  1183 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
```
```  1184 apply (cases r)
```
```  1185 apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
```
```  1186 done
```
```  1187
```
```  1188 lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
```
```  1189 by (simp add: hcomplex_mult_assoc [symmetric])
```
```  1190
```
```  1191 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
```
```  1192 by simp
```
```  1193
```
```  1194 lemma hcis_hypreal_of_nat_Suc_mult:
```
```  1195    "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
```
```  1196 apply (cases a)
```
```  1197 apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
```
```  1198 done
```
```  1199
```
```  1200 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
```
```  1201 apply (induct_tac "n")
```
```  1202 apply (simp_all add: hcis_hypreal_of_nat_Suc_mult)
```
```  1203 done
```
```  1204
```
```  1205 lemma hcis_hypreal_of_hypnat_Suc_mult:
```
```  1206      "hcis (hypreal_of_hypnat (n + 1) * a) =
```
```  1207       hcis a * hcis (hypreal_of_hypnat n * a)"
```
```  1208 apply (cases a, cases n)
```
```  1209 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
```
```  1210 done
```
```  1211
```
```  1212 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
```
```  1213 apply (cases a, cases n)
```
```  1214 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
```
```  1215 done
```
```  1216
```
```  1217 lemma DeMoivre2:
```
```  1218   "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
```
```  1219 apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
```
```  1220 done
```
```  1221
```
```  1222 lemma DeMoivre2_ext:
```
```  1223   "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
```
```  1224 apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
```
```  1225 done
```
```  1226
```
```  1227 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
```
```  1228 apply (cases a)
```
```  1229 apply (simp add: hcomplex_inverse hcis hypreal_minus)
```
```  1230 done
```
```  1231
```
```  1232 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
```
```  1233 apply (cases a, cases r)
```
```  1234 apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
```
```  1235 apply (simp add: real_divide_def)
```
```  1236 done
```
```  1237
```
```  1238 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
```
```  1239 apply (cases a)
```
```  1240 apply (simp add: hcis starfun hRe)
```
```  1241 done
```
```  1242
```
```  1243 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
```
```  1244 apply (cases a)
```
```  1245 apply (simp add: hcis starfun hIm)
```
```  1246 done
```
```  1247
```
```  1248 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
```
```  1249 by (simp add: NSDeMoivre)
```
```  1250
```
```  1251 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
```
```  1252 by (simp add: NSDeMoivre)
```
```  1253
```
```  1254 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
```
```  1255 by (simp add: NSDeMoivre_ext)
```
```  1256
```
```  1257 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
```
```  1258 by (simp add: NSDeMoivre_ext)
```
```  1259
```
```  1260 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
```
```  1261 apply (simp add: hexpi_def, cases a, cases b)
```
```  1262 apply (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)
```
```  1263 done
```
```  1264
```
```  1265
```
```  1266 subsection{*@{term hcomplex_of_complex}: the Injection from
```
```  1267   type @{typ complex} to to @{typ hcomplex}*}
```
```  1268
```
```  1269 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
```
```  1270 apply (rule inj_onI, rule ccontr)
```
```  1271 apply (simp add: hcomplex_of_complex_def)
```
```  1272 done
```
```  1273
```
```  1274 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
```
```  1275 by (simp add: iii_def hcomplex_of_complex_def)
```
```  1276
```
```  1277 lemma hcomplex_of_complex_add [simp]:
```
```  1278      "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
```
```  1279 by (simp add: hcomplex_of_complex_def hcomplex_add)
```
```  1280
```
```  1281 lemma hcomplex_of_complex_mult [simp]:
```
```  1282      "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
```
```  1283 by (simp add: hcomplex_of_complex_def hcomplex_mult)
```
```  1284
```
```  1285 lemma hcomplex_of_complex_eq_iff [simp]:
```
```  1286      "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
```
```  1287 by (simp add: hcomplex_of_complex_def)
```
```  1288
```
```  1289
```
```  1290 lemma hcomplex_of_complex_minus [simp]:
```
```  1291      "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
```
```  1292 by (simp add: hcomplex_of_complex_def hcomplex_minus)
```
```  1293
```
```  1294 lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1"
```
```  1295 by (simp add: hcomplex_of_complex_def hcomplex_one_def)
```
```  1296
```
```  1297 lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
```
```  1298 by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
```
```  1299
```
```  1300 lemma hcomplex_of_complex_zero_iff [simp]:
```
```  1301      "(hcomplex_of_complex r = 0) = (r = 0)"
```
```  1302 by (auto intro: FreeUltrafilterNat_P
```
```  1303          simp add: hcomplex_of_complex_def hcomplex_zero_def)
```
```  1304
```
```  1305 lemma hcomplex_of_complex_inverse [simp]:
```
```  1306      "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
```
```  1307 proof cases
```
```  1308   assume "r=0" thus ?thesis by simp
```
```  1309 next
```
```  1310   assume nz: "r\<noteq>0"
```
```  1311   show ?thesis
```
```  1312   proof (rule hcomplex_mult_left_cancel [THEN iffD1])
```
```  1313     show "hcomplex_of_complex r \<noteq> 0"
```
```  1314       by (simp add: nz)
```
```  1315   next
```
```  1316     have "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
```
```  1317           hcomplex_of_complex (r * inverse r)"
```
```  1318       by simp
```
```  1319     also have "... = hcomplex_of_complex r * inverse (hcomplex_of_complex r)"
```
```  1320       by (simp add: nz)
```
```  1321     finally show "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
```
```  1322                   hcomplex_of_complex r * inverse (hcomplex_of_complex r)" .
```
```  1323   qed
```
```  1324 qed
```
```  1325
```
```  1326 lemma hcomplex_of_complex_divide [simp]:
```
```  1327      "hcomplex_of_complex (z1 / z2) =
```
```  1328       hcomplex_of_complex z1 / hcomplex_of_complex z2"
```
```  1329 by (simp add: hcomplex_divide_def complex_divide_def)
```
```  1330
```
```  1331 lemma hRe_hcomplex_of_complex:
```
```  1332    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
```
```  1333 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
```
```  1334
```
```  1335 lemma hIm_hcomplex_of_complex:
```
```  1336    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
```
```  1337 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
```
```  1338
```
```  1339 lemma hcmod_hcomplex_of_complex:
```
```  1340      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
```
```  1341 by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
```
```  1342
```
```  1343
```
```  1344 subsection{*Numerals and Arithmetic*}
```
```  1345
```
```  1346 instance hcomplex :: number ..
```
```  1347
```
```  1348 defs (overloaded)
```
```  1349   hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
```
```  1350     --{*the type constraint is essential!*}
```
```  1351
```
```  1352 instance hcomplex :: number_ring
```
```  1353 by (intro_classes, simp add: hcomplex_number_of_def)
```
```  1354
```
```  1355
```
```  1356 lemma hcomplex_of_complex_of_nat [simp]:
```
```  1357      "hcomplex_of_complex (of_nat n) = of_nat n"
```
```  1358 by (induct n, simp_all)
```
```  1359
```
```  1360 lemma hcomplex_of_complex_of_int [simp]:
```
```  1361      "hcomplex_of_complex (of_int z) = of_int z"
```
```  1362 proof (cases z)
```
```  1363   case (1 n)
```
```  1364     thus ?thesis by simp
```
```  1365 next
```
```  1366   case (2 n)
```
```  1367     thus ?thesis
```
```  1368       by (simp only: of_int_minus hcomplex_of_complex_minus, simp)
```
```  1369 qed
```
```  1370
```
```  1371
```
```  1372 text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
```
```  1373 lemma hcomplex_number_of [simp]:
```
```  1374      "hcomplex_of_complex (number_of w) = number_of w"
```
```  1375 by (simp add: hcomplex_number_of_def complex_number_of_def)
```
```  1376
```
```  1377 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
```
```  1378      "hcomplex_of_hypreal (hypreal_of_real x) =
```
```  1379       hcomplex_of_complex (complex_of_real x)"
```
```  1380 by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def
```
```  1381               complex_of_real_def)
```
```  1382
```
```  1383 lemma hcomplex_hypreal_number_of:
```
```  1384   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
```
```  1385 by (simp only: complex_number_of [symmetric] hypreal_number_of [symmetric]
```
```  1386                hcomplex_of_hypreal_eq_hcomplex_of_complex)
```
```  1387
```
```  1388 text{*This theorem is necessary because theorems such as
```
```  1389    @{text iszero_number_of_0} only hold for ordered rings. They cannot
```
```  1390    be generalized to fields in general because they fail for finite fields.
```
```  1391    They work for type complex because the reals can be embedded in them.*}
```
```  1392 lemma iszero_hcomplex_number_of [simp]:
```
```  1393      "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
```
```  1394 apply (simp only: iszero_complex_number_of [symmetric])
```
```  1395 apply (simp only: hcomplex_of_complex_zero_iff hcomplex_number_of [symmetric]
```
```  1396                   iszero_def)
```
```  1397 done
```
```  1398
```
```  1399
```
```  1400 (*
```
```  1401 Goal "z + hcnj z =
```
```  1402       hcomplex_of_hypreal (2 * hRe(z))"
```
```  1403 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
```
```  1404 by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
```
```  1405     hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
```
```  1406 qed "hcomplex_add_hcnj";
```
```  1407
```
```  1408 Goal "z - hcnj z = \
```
```  1409 \     hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
```
```  1410 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
```
```  1411 by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
```
```  1412     hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
```
```  1413     complex_diff_cnj,iii_def,hcomplex_mult]));
```
```  1414 qed "hcomplex_diff_hcnj";
```
```  1415 *)
```
```  1416
```
```  1417
```
```  1418 lemma hcomplex_hcnj_num_zero_iff: "(hcnj z = 0) = (z = 0)"
```
```  1419 apply (auto simp add: hcomplex_hcnj_zero_iff)
```
```  1420 done
```
```  1421 declare hcomplex_hcnj_num_zero_iff [simp]
```
```  1422
```
```  1423 lemma hcomplex_zero_num: "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})"
```
```  1424 apply (simp add: hcomplex_zero_def)
```
```  1425 done
```
```  1426
```
```  1427 lemma hcomplex_one_num: "1 =  Abs_hcomplex (hcomplexrel `` {%n. 1})"
```
```  1428 apply (simp add: hcomplex_one_def)
```
```  1429 done
```
```  1430
```
```  1431 (*** Real and imaginary stuff ***)
```
```  1432
```
```  1433 (*Convert???
```
```  1434 Goalw [hcomplex_number_of_def]
```
```  1435   "((number_of xa :: hcomplex) + iii * number_of ya =
```
```  1436         number_of xb + iii * number_of yb) =
```
```  1437    (((number_of xa :: hcomplex) = number_of xb) &
```
```  1438     ((number_of ya :: hcomplex) = number_of yb))"
```
```  1439 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
```
```  1440      hcomplex_hypreal_number_of]));
```
```  1441 qed "hcomplex_number_of_eq_cancel_iff";
```
```  1442 Addsimps [hcomplex_number_of_eq_cancel_iff];
```
```  1443
```
```  1444 Goalw [hcomplex_number_of_def]
```
```  1445   "((number_of xa :: hcomplex) + number_of ya * iii = \
```
```  1446 \       number_of xb + number_of yb * iii) = \
```
```  1447 \  (((number_of xa :: hcomplex) = number_of xb) & \
```
```  1448 \   ((number_of ya :: hcomplex) = number_of yb))";
```
```  1449 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
```
```  1450     hcomplex_hypreal_number_of]));
```
```  1451 qed "hcomplex_number_of_eq_cancel_iffA";
```
```  1452 Addsimps [hcomplex_number_of_eq_cancel_iffA];
```
```  1453
```
```  1454 Goalw [hcomplex_number_of_def]
```
```  1455   "((number_of xa :: hcomplex) + number_of ya * iii = \
```
```  1456 \       number_of xb + iii * number_of yb) = \
```
```  1457 \  (((number_of xa :: hcomplex) = number_of xb) & \
```
```  1458 \   ((number_of ya :: hcomplex) = number_of yb))";
```
```  1459 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
```
```  1460     hcomplex_hypreal_number_of]));
```
```  1461 qed "hcomplex_number_of_eq_cancel_iffB";
```
```  1462 Addsimps [hcomplex_number_of_eq_cancel_iffB];
```
```  1463
```
```  1464 Goalw [hcomplex_number_of_def]
```
```  1465   "((number_of xa :: hcomplex) + iii * number_of ya = \
```
```  1466 \       number_of xb + number_of yb * iii) = \
```
```  1467 \  (((number_of xa :: hcomplex) = number_of xb) & \
```
```  1468 \   ((number_of ya :: hcomplex) = number_of yb))";
```
```  1469 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
```
```  1470      hcomplex_hypreal_number_of]));
```
```  1471 qed "hcomplex_number_of_eq_cancel_iffC";
```
```  1472 Addsimps [hcomplex_number_of_eq_cancel_iffC];
```
```  1473
```
```  1474 Goalw [hcomplex_number_of_def]
```
```  1475   "((number_of xa :: hcomplex) + iii * number_of ya = \
```
```  1476 \       number_of xb) = \
```
```  1477 \  (((number_of xa :: hcomplex) = number_of xb) & \
```
```  1478 \   ((number_of ya :: hcomplex) = 0))";
```
```  1479 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
```
```  1480     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
```
```  1481 qed "hcomplex_number_of_eq_cancel_iff2";
```
```  1482 Addsimps [hcomplex_number_of_eq_cancel_iff2];
```
```  1483
```
```  1484 Goalw [hcomplex_number_of_def]
```
```  1485   "((number_of xa :: hcomplex) + number_of ya * iii = \
```
```  1486 \       number_of xb) = \
```
```  1487 \  (((number_of xa :: hcomplex) = number_of xb) & \
```
```  1488 \   ((number_of ya :: hcomplex) = 0))";
```
```  1489 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
```
```  1490     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
```
```  1491 qed "hcomplex_number_of_eq_cancel_iff2a";
```
```  1492 Addsimps [hcomplex_number_of_eq_cancel_iff2a];
```
```  1493
```
```  1494 Goalw [hcomplex_number_of_def]
```
```  1495   "((number_of xa :: hcomplex) + iii * number_of ya = \
```
```  1496 \    iii * number_of yb) = \
```
```  1497 \  (((number_of xa :: hcomplex) = 0) & \
```
```  1498 \   ((number_of ya :: hcomplex) = number_of yb))";
```
```  1499 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
```
```  1500     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
```
```  1501 qed "hcomplex_number_of_eq_cancel_iff3";
```
```  1502 Addsimps [hcomplex_number_of_eq_cancel_iff3];
```
```  1503
```
```  1504 Goalw [hcomplex_number_of_def]
```
```  1505   "((number_of xa :: hcomplex) + number_of ya * iii= \
```
```  1506 \    iii * number_of yb) = \
```
```  1507 \  (((number_of xa :: hcomplex) = 0) & \
```
```  1508 \   ((number_of ya :: hcomplex) = number_of yb))";
```
```  1509 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
```
```  1510     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
```
```  1511 qed "hcomplex_number_of_eq_cancel_iff3a";
```
```  1512 Addsimps [hcomplex_number_of_eq_cancel_iff3a];
```
```  1513 *)
```
```  1514
```
```  1515 lemma hcomplex_number_of_hcnj [simp]:
```
```  1516      "hcnj (number_of v :: hcomplex) = number_of v"
```
```  1517 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
```
```  1518                hcomplex_hcnj_hcomplex_of_hypreal)
```
```  1519
```
```  1520 lemma hcomplex_number_of_hcmod [simp]:
```
```  1521       "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
```
```  1522 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
```
```  1523                hcmod_hcomplex_of_hypreal)
```
```  1524
```
```  1525 lemma hcomplex_number_of_hRe [simp]:
```
```  1526       "hRe(number_of v :: hcomplex) = number_of v"
```
```  1527 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
```
```  1528                hRe_hcomplex_of_hypreal)
```
```  1529
```
```  1530 lemma hcomplex_number_of_hIm [simp]:
```
```  1531       "hIm(number_of v :: hcomplex) = 0"
```
```  1532 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
```
```  1533                hIm_hcomplex_of_hypreal)
```
```  1534
```
```  1535
```
```  1536 ML
```
```  1537 {*
```
```  1538 val hcomplex_zero_def = thm"hcomplex_zero_def";
```
```  1539 val hcomplex_one_def = thm"hcomplex_one_def";
```
```  1540 val hcomplex_minus_def = thm"hcomplex_minus_def";
```
```  1541 val hcomplex_diff_def = thm"hcomplex_diff_def";
```
```  1542 val hcomplex_divide_def = thm"hcomplex_divide_def";
```
```  1543 val hcomplex_mult_def = thm"hcomplex_mult_def";
```
```  1544 val hcomplex_add_def = thm"hcomplex_add_def";
```
```  1545 val hcomplex_of_complex_def = thm"hcomplex_of_complex_def";
```
```  1546 val iii_def = thm"iii_def";
```
```  1547
```
```  1548 val hcomplexrel_iff = thm"hcomplexrel_iff";
```
```  1549 val hcomplexrel_refl = thm"hcomplexrel_refl";
```
```  1550 val hcomplexrel_sym = thm"hcomplexrel_sym";
```
```  1551 val hcomplexrel_trans = thm"hcomplexrel_trans";
```
```  1552 val equiv_hcomplexrel = thm"equiv_hcomplexrel";
```
```  1553 val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff";
```
```  1554 val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex";
```
```  1555 val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex";
```
```  1556 val inj_Rep_hcomplex = thm"inj_Rep_hcomplex";
```
```  1557 val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl";
```
```  1558 val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem";
```
```  1559 val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty";
```
```  1560 val eq_Abs_hcomplex = thm"eq_Abs_hcomplex";
```
```  1561 val hRe = thm"hRe";
```
```  1562 val hIm = thm"hIm";
```
```  1563 val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
```
```  1564 val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
```
```  1565 val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
```
```  1566 val hcomplex_hRe_one = thm"hcomplex_hRe_one";
```
```  1567 val hcomplex_hIm_one = thm"hcomplex_hIm_one";
```
```  1568 val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
```
```  1569 val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
```
```  1570 val hcomplex_add = thm"hcomplex_add";
```
```  1571 val hcomplex_add_commute = thm"hcomplex_add_commute";
```
```  1572 val hcomplex_add_assoc = thm"hcomplex_add_assoc";
```
```  1573 val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
```
```  1574 val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
```
```  1575 val hRe_add = thm"hRe_add";
```
```  1576 val hIm_add = thm"hIm_add";
```
```  1577 val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
```
```  1578 val hcomplex_minus = thm"hcomplex_minus";
```
```  1579 val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
```
```  1580 val hRe_minus = thm"hRe_minus";
```
```  1581 val hIm_minus = thm"hIm_minus";
```
```  1582 val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
```
```  1583 val hcomplex_diff = thm"hcomplex_diff";
```
```  1584 val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
```
```  1585 val hcomplex_mult = thm"hcomplex_mult";
```
```  1586 val hcomplex_mult_commute = thm"hcomplex_mult_commute";
```
```  1587 val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
```
```  1588 val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
```
```  1589 val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
```
```  1590 val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
```
```  1591 val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
```
```  1592 val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
```
```  1593 val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
```
```  1594 val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
```
```  1595 val hcomplex_inverse = thm"hcomplex_inverse";
```
```  1596 val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
```
```  1597 val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
```
```  1598 val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
```
```  1599 val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
```
```  1600 val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
```
```  1601 val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
```
```  1602 val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
```
```  1603 val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
```
```  1604 val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
```
```  1605 val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
```
```  1606 val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
```
```  1607 val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
```
```  1608 val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
```
```  1609 val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
```
```  1610 val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
```
```  1611 val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
```
```  1612 val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
```
```  1613 val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
```
```  1614 val hcmod = thm"hcmod";
```
```  1615 val hcmod_zero = thm"hcmod_zero";
```
```  1616 val hcmod_one = thm"hcmod_one";
```
```  1617 val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
```
```  1618 val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
```
```  1619 val hcnj = thm"hcnj";
```
```  1620 val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
```
```  1621 val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
```
```  1622 val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
```
```  1623 val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
```
```  1624 val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
```
```  1625 val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
```
```  1626 val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
```
```  1627 val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
```
```  1628 val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
```
```  1629 val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
```
```  1630 val hcnj_one = thm"hcnj_one";
```
```  1631 val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
```
```  1632 val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
```
```  1633 val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
```
```  1634 val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
```
```  1635 val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
```
```  1636
```
```  1637 val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
```
```  1638 val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
```
```  1639 val hcmod_minus = thm"hcmod_minus";
```
```  1640 val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
```
```  1641 val hcmod_ge_zero = thm"hcmod_ge_zero";
```
```  1642 val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
```
```  1643 val hcmod_mult = thm"hcmod_mult";
```
```  1644 val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
```
```  1645 val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
```
```  1646 val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
```
```  1647 val hcmod_triangle_squared = thm"hcmod_triangle_squared";
```
```  1648 val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
```
```  1649 val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
```
```  1650 val hcmod_diff_commute = thm"hcmod_diff_commute";
```
```  1651 val hcmod_add_less = thm"hcmod_add_less";
```
```  1652 val hcmod_mult_less = thm"hcmod_mult_less";
```
```  1653 val hcmod_diff_ineq = thm"hcmod_diff_ineq";
```
```  1654 val hcpow = thm"hcpow";
```
```  1655 val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
```
```  1656 val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
```
```  1657 val hcmod_hcpow = thm"hcmod_hcpow";
```
```  1658 val hcpow_minus = thm"hcpow_minus";
```
```  1659 val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
```
```  1660 val hcmod_divide = thm"hcmod_divide";
```
```  1661 val hcpow_mult = thm"hcpow_mult";
```
```  1662 val hcpow_zero = thm"hcpow_zero";
```
```  1663 val hcpow_zero2 = thm"hcpow_zero2";
```
```  1664 val hcpow_not_zero = thm"hcpow_not_zero";
```
```  1665 val hcpow_zero_zero = thm"hcpow_zero_zero";
```
```  1666 val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
```
```  1667 val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
```
```  1668 val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
```
```  1669 val hcomplex_divide = thm"hcomplex_divide";
```
```  1670 val hsgn = thm"hsgn";
```
```  1671 val hsgn_zero = thm"hsgn_zero";
```
```  1672 val hsgn_one = thm"hsgn_one";
```
```  1673 val hsgn_minus = thm"hsgn_minus";
```
```  1674 val hsgn_eq = thm"hsgn_eq";
```
```  1675 val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
```
```  1676 val hcmod_i = thm"hcmod_i";
```
```  1677 val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
```
```  1678 val hRe_hsgn = thm"hRe_hsgn";
```
```  1679 val hIm_hsgn = thm"hIm_hsgn";
```
```  1680 val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
```
```  1681 val hRe_mult_i_eq = thm"hRe_mult_i_eq";
```
```  1682 val hIm_mult_i_eq = thm"hIm_mult_i_eq";
```
```  1683 val hcmod_mult_i = thm"hcmod_mult_i";
```
```  1684 val hcmod_mult_i2 = thm"hcmod_mult_i2";
```
```  1685 val harg = thm"harg";
```
```  1686 val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
```
```  1687 val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
```
```  1688 val complex_split_polar2 = thm"complex_split_polar2";
```
```  1689 val hcomplex_split_polar = thm"hcomplex_split_polar";
```
```  1690 val hcis = thm"hcis";
```
```  1691 val hcis_eq = thm"hcis_eq";
```
```  1692 val hrcis = thm"hrcis";
```
```  1693 val hrcis_Ex = thm"hrcis_Ex";
```
```  1694 val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
```
```  1695 val hRe_hrcis = thm"hRe_hrcis";
```
```  1696 val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
```
```  1697 val hIm_hrcis = thm"hIm_hrcis";
```
```  1698 val hcmod_complex_polar = thm"hcmod_complex_polar";
```
```  1699 val hcmod_hrcis = thm"hcmod_hrcis";
```
```  1700 val hcis_hrcis_eq = thm"hcis_hrcis_eq";
```
```  1701 val hrcis_mult = thm"hrcis_mult";
```
```  1702 val hcis_mult = thm"hcis_mult";
```
```  1703 val hcis_zero = thm"hcis_zero";
```
```  1704 val hrcis_zero_mod = thm"hrcis_zero_mod";
```
```  1705 val hrcis_zero_arg = thm"hrcis_zero_arg";
```
```  1706 val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
```
```  1707 val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
```
```  1708 val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
```
```  1709 val NSDeMoivre = thm"NSDeMoivre";
```
```  1710 val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
```
```  1711 val NSDeMoivre_ext = thm"NSDeMoivre_ext";
```
```  1712 val DeMoivre2 = thm"DeMoivre2";
```
```  1713 val DeMoivre2_ext = thm"DeMoivre2_ext";
```
```  1714 val hcis_inverse = thm"hcis_inverse";
```
```  1715 val hrcis_inverse = thm"hrcis_inverse";
```
```  1716 val hRe_hcis = thm"hRe_hcis";
```
```  1717 val hIm_hcis = thm"hIm_hcis";
```
```  1718 val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
```
```  1719 val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
```
```  1720 val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
```
```  1721 val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
```
```  1722 val hexpi_add = thm"hexpi_add";
```
```  1723 val hcomplex_of_complex_add = thm"hcomplex_of_complex_add";
```
```  1724 val hcomplex_of_complex_mult = thm"hcomplex_of_complex_mult";
```
```  1725 val hcomplex_of_complex_eq_iff = thm"hcomplex_of_complex_eq_iff";
```
```  1726 val hcomplex_of_complex_minus = thm"hcomplex_of_complex_minus";
```
```  1727 val hcomplex_of_complex_one = thm"hcomplex_of_complex_one";
```
```  1728 val hcomplex_of_complex_zero = thm"hcomplex_of_complex_zero";
```
```  1729 val hcomplex_of_complex_zero_iff = thm"hcomplex_of_complex_zero_iff";
```
```  1730 val hcomplex_of_complex_inverse = thm"hcomplex_of_complex_inverse";
```
```  1731 val hcomplex_of_complex_divide = thm"hcomplex_of_complex_divide";
```
```  1732 val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
```
```  1733 val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
```
```  1734 val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
```
```  1735 *}
```
```  1736
```
```  1737 end
```