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