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