src/HOL/Complex/NSComplex.thy
author paulson
Thu Jul 29 16:14:42 2004 +0200 (2004-07-29)
changeset 15085 5693a977a767
parent 15013 34264f5e4691
child 15131 c69542757a4d
permissions -rw-r--r--
removed some [iff] declarations from RealDef.thy, concerning inequalities
     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 (*????move to RealDef????*)
   992 lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
   993 by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
   994 
   995 lemma hcomplex_inverse_complex_split:
   996      "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   997       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
   998       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
   999 apply (cases x, cases y)
  1000 apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
  1001          starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
  1002          hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
  1003 apply (simp add: diff_minus) 
  1004 done
  1005 
  1006 lemma HComplex_inverse:
  1007      "inverse (HComplex x y) =
  1008       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
  1009 by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
  1010 
  1011 
  1012 
  1013 lemma hRe_mult_i_eq[simp]:
  1014     "hRe (iii * hcomplex_of_hypreal y) = 0"
  1015 apply (simp add: iii_def, cases y)
  1016 apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
  1017 done
  1018 
  1019 lemma hIm_mult_i_eq [simp]:
  1020     "hIm (iii * hcomplex_of_hypreal y) = y"
  1021 apply (simp add: iii_def, cases y)
  1022 apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
  1023 done
  1024 
  1025 lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
  1026 apply (cases y)
  1027 apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
  1028 done
  1029 
  1030 lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
  1031 by (simp only: hcmod_mult_i hcomplex_mult_commute)
  1032 
  1033 (*---------------------------------------------------------------------------*)
  1034 (*  harg                                                                     *)
  1035 (*---------------------------------------------------------------------------*)
  1036 
  1037 lemma harg:
  1038   "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
  1039       Abs_hypreal(hyprel `` {%n. arg (X n)})"
  1040 apply (simp add: harg_def)
  1041 apply (rule_tac f = Abs_hypreal in arg_cong)
  1042 apply (auto iff: hcomplexrel_iff, ultra)
  1043 done
  1044 
  1045 lemma cos_harg_i_mult_zero_pos:
  1046      "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
  1047 apply (cases y)
  1048 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
  1049                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
  1050 done
  1051 
  1052 lemma cos_harg_i_mult_zero_neg:
  1053      "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
  1054 apply (cases y)
  1055 apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
  1056                  hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
  1057 done
  1058 
  1059 lemma cos_harg_i_mult_zero [simp]:
  1060      "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
  1061 by (auto simp add: linorder_neq_iff
  1062                    cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
  1063 
  1064 lemma hcomplex_of_hypreal_zero_iff [simp]:
  1065      "(hcomplex_of_hypreal y = 0) = (y = 0)"
  1066 apply (cases y)
  1067 apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
  1068 done
  1069 
  1070 
  1071 subsection{*Polar Form for Nonstandard Complex Numbers*}
  1072 
  1073 lemma complex_split_polar2:
  1074      "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
  1075 by (blast intro: complex_split_polar)
  1076 
  1077 lemma lemma_hypreal_P_EX2:
  1078      "(\<exists>(x::hypreal) y. P x y) =
  1079       (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
  1080 apply auto
  1081 apply (rule_tac z = x in eq_Abs_hypreal)
  1082 apply (rule_tac z = y in eq_Abs_hypreal, auto)
  1083 done
  1084 
  1085 lemma hcomplex_split_polar:
  1086   "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
  1087 apply (cases z)
  1088 apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
  1089 apply (cut_tac z = x in complex_split_polar2)
  1090 apply (drule choice, safe)+
  1091 apply (rule_tac x = f in exI)
  1092 apply (rule_tac x = fa in exI, auto)
  1093 done
  1094 
  1095 lemma hcis:
  1096   "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
  1097       Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
  1098 apply (simp add: hcis_def)
  1099 apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
  1100 done
  1101 
  1102 lemma hcis_eq:
  1103    "hcis a =
  1104     (hcomplex_of_hypreal(( *f* cos) a) +
  1105     iii * hcomplex_of_hypreal(( *f* sin) a))"
  1106 apply (cases a)
  1107 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
  1108 done
  1109 
  1110 lemma hrcis:
  1111   "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
  1112       Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
  1113 by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
  1114 
  1115 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
  1116 apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
  1117 apply (rule hcomplex_split_polar)
  1118 done
  1119 
  1120 lemma hRe_hcomplex_polar [simp]:
  1121      "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
  1122       r * ( *f* cos) a"
  1123 by (simp add: hcomplex_of_hypreal_mult_HComplex)
  1124 
  1125 lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
  1126 by (simp add: hrcis_def hcis_eq)
  1127 
  1128 lemma hIm_hcomplex_polar [simp]:
  1129      "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
  1130       r * ( *f* sin) a"
  1131 by (simp add: hcomplex_of_hypreal_mult_HComplex)
  1132 
  1133 lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
  1134 by (simp add: hrcis_def hcis_eq)
  1135 
  1136 
  1137 lemma hcmod_unit_one [simp]:
  1138      "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
  1139 apply (cases a) 
  1140 apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
  1141                  hcomplex_mult hcmod hcomplex_add hypreal_one_def)
  1142 done
  1143 
  1144 lemma hcmod_complex_polar [simp]:
  1145      "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
  1146       abs r"
  1147 apply (simp only: hcmod_mult hcmod_unit_one, simp)  
  1148 done
  1149 
  1150 lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
  1151 by (simp add: hrcis_def hcis_eq)
  1152 
  1153 (*---------------------------------------------------------------------------*)
  1154 (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
  1155 (*---------------------------------------------------------------------------*)
  1156 
  1157 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
  1158 by (simp add: hrcis_def)
  1159 declare hcis_hrcis_eq [symmetric, simp]
  1160 
  1161 lemma hrcis_mult:
  1162   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
  1163 apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
  1164 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  1165                       hcomplex_mult cis_mult [symmetric])
  1166 done
  1167 
  1168 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
  1169 apply (cases a, cases b)
  1170 apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
  1171 done
  1172 
  1173 lemma hcis_zero [simp]: "hcis 0 = 1"
  1174 by (simp add: hcomplex_one_def hcis hypreal_zero_num)
  1175 
  1176 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
  1177 apply (simp add: hcomplex_zero_def, cases a)
  1178 apply (simp add: hrcis hypreal_zero_num)
  1179 done
  1180 
  1181 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
  1182 apply (cases r)
  1183 apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
  1184 done
  1185 
  1186 lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
  1187 by (simp add: hcomplex_mult_assoc [symmetric])
  1188 
  1189 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
  1190 by simp
  1191 
  1192 lemma hcis_hypreal_of_nat_Suc_mult:
  1193    "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
  1194 apply (cases a)
  1195 apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1196 done
  1197 
  1198 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
  1199 apply (induct_tac "n")
  1200 apply (simp_all add: hcis_hypreal_of_nat_Suc_mult)
  1201 done
  1202 
  1203 lemma hcis_hypreal_of_hypnat_Suc_mult:
  1204      "hcis (hypreal_of_hypnat (n + 1) * a) =
  1205       hcis a * hcis (hypreal_of_hypnat n * a)"
  1206 apply (cases a, cases n)
  1207 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  1208 done
  1209 
  1210 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
  1211 apply (cases a, cases n)
  1212 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
  1213 done
  1214 
  1215 lemma DeMoivre2:
  1216   "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
  1217 apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
  1218 done
  1219 
  1220 lemma DeMoivre2_ext:
  1221   "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
  1222 apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
  1223 done
  1224 
  1225 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
  1226 apply (cases a)
  1227 apply (simp add: hcomplex_inverse hcis hypreal_minus)
  1228 done
  1229 
  1230 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
  1231 apply (cases a, cases r)
  1232 apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
  1233 apply (simp add: real_divide_def)
  1234 done
  1235 
  1236 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
  1237 apply (cases a)
  1238 apply (simp add: hcis starfun hRe)
  1239 done
  1240 
  1241 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
  1242 apply (cases a)
  1243 apply (simp add: hcis starfun hIm)
  1244 done
  1245 
  1246 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
  1247 by (simp add: NSDeMoivre)
  1248 
  1249 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
  1250 by (simp add: NSDeMoivre)
  1251 
  1252 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
  1253 by (simp add: NSDeMoivre_ext)
  1254 
  1255 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
  1256 by (simp add: NSDeMoivre_ext)
  1257 
  1258 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
  1259 apply (simp add: hexpi_def, cases a, cases b)
  1260 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)
  1261 done
  1262 
  1263 
  1264 subsection{*@{term hcomplex_of_complex}: the Injection from
  1265   type @{typ complex} to to @{typ hcomplex}*}
  1266 
  1267 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
  1268 apply (rule inj_onI, rule ccontr)
  1269 apply (simp add: hcomplex_of_complex_def)
  1270 done
  1271 
  1272 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
  1273 by (simp add: iii_def hcomplex_of_complex_def)
  1274 
  1275 lemma hcomplex_of_complex_add [simp]:
  1276      "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
  1277 by (simp add: hcomplex_of_complex_def hcomplex_add)
  1278 
  1279 lemma hcomplex_of_complex_mult [simp]:
  1280      "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
  1281 by (simp add: hcomplex_of_complex_def hcomplex_mult)
  1282 
  1283 lemma hcomplex_of_complex_eq_iff [simp]:
  1284      "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
  1285 by (simp add: hcomplex_of_complex_def)
  1286 
  1287 
  1288 lemma hcomplex_of_complex_minus [simp]:
  1289      "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
  1290 by (simp add: hcomplex_of_complex_def hcomplex_minus)
  1291 
  1292 lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1"
  1293 by (simp add: hcomplex_of_complex_def hcomplex_one_def)
  1294 
  1295 lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
  1296 by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1297 
  1298 lemma hcomplex_of_complex_zero_iff [simp]:
  1299      "(hcomplex_of_complex r = 0) = (r = 0)"
  1300 by (auto intro: FreeUltrafilterNat_P 
  1301          simp add: hcomplex_of_complex_def hcomplex_zero_def)
  1302 
  1303 lemma hcomplex_of_complex_inverse [simp]:
  1304      "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
  1305 proof cases
  1306   assume "r=0" thus ?thesis by simp
  1307 next
  1308   assume nz: "r\<noteq>0" 
  1309   show ?thesis
  1310   proof (rule hcomplex_mult_left_cancel [THEN iffD1]) 
  1311     show "hcomplex_of_complex r \<noteq> 0"
  1312       by (simp add: nz) 
  1313   next
  1314     have "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
  1315           hcomplex_of_complex (r * inverse r)"
  1316       by simp
  1317     also have "... = hcomplex_of_complex r * inverse (hcomplex_of_complex r)" 
  1318       by (simp add: nz)
  1319     finally show "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
  1320                   hcomplex_of_complex r * inverse (hcomplex_of_complex r)" .
  1321   qed
  1322 qed
  1323 
  1324 lemma hcomplex_of_complex_divide [simp]:
  1325      "hcomplex_of_complex (z1 / z2) = 
  1326       hcomplex_of_complex z1 / hcomplex_of_complex z2"
  1327 by (simp add: hcomplex_divide_def complex_divide_def)
  1328 
  1329 lemma hRe_hcomplex_of_complex:
  1330    "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
  1331 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
  1332 
  1333 lemma hIm_hcomplex_of_complex:
  1334    "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
  1335 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
  1336 
  1337 lemma hcmod_hcomplex_of_complex:
  1338      "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
  1339 by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
  1340 
  1341 
  1342 subsection{*Numerals and Arithmetic*}
  1343 
  1344 instance hcomplex :: number ..
  1345 
  1346 defs (overloaded)
  1347   hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
  1348     --{*the type constraint is essential!*}
  1349 
  1350 instance hcomplex :: number_ring
  1351 by (intro_classes, simp add: hcomplex_number_of_def) 
  1352 
  1353 
  1354 lemma hcomplex_of_complex_of_nat [simp]:
  1355      "hcomplex_of_complex (of_nat n) = of_nat n"
  1356 by (induct n, simp_all) 
  1357 
  1358 lemma hcomplex_of_complex_of_int [simp]:
  1359      "hcomplex_of_complex (of_int z) = of_int z"
  1360 proof (cases z)
  1361   case (1 n)
  1362     thus ?thesis by simp
  1363 next
  1364   case (2 n)
  1365     thus ?thesis 
  1366       by (simp only: of_int_minus hcomplex_of_complex_minus, simp)
  1367 qed
  1368 
  1369 
  1370 text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
  1371 lemma hcomplex_number_of [simp]:
  1372      "hcomplex_of_complex (number_of w) = number_of w"
  1373 by (simp add: hcomplex_number_of_def complex_number_of_def) 
  1374 
  1375 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
  1376      "hcomplex_of_hypreal (hypreal_of_real x) =  
  1377       hcomplex_of_complex (complex_of_real x)"
  1378 by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def 
  1379               complex_of_real_def)
  1380 
  1381 lemma hcomplex_hypreal_number_of: 
  1382   "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
  1383 by (simp only: complex_number_of [symmetric] hypreal_number_of [symmetric] 
  1384                hcomplex_of_hypreal_eq_hcomplex_of_complex)
  1385 
  1386 text{*This theorem is necessary because theorems such as
  1387    @{text iszero_number_of_0} only hold for ordered rings. They cannot
  1388    be generalized to fields in general because they fail for finite fields.
  1389    They work for type complex because the reals can be embedded in them.*}
  1390 lemma iszero_hcomplex_number_of [simp]:
  1391      "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
  1392 apply (simp only: iszero_complex_number_of [symmetric])  
  1393 apply (simp only: hcomplex_of_complex_zero_iff hcomplex_number_of [symmetric] 
  1394                   iszero_def)  
  1395 done
  1396 
  1397 
  1398 (*
  1399 Goal "z + hcnj z =  
  1400       hcomplex_of_hypreal (2 * hRe(z))"
  1401 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
  1402 by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add,
  1403     hypreal_mult,hcomplex_of_hypreal,complex_add_cnj]));
  1404 qed "hcomplex_add_hcnj";
  1405 
  1406 Goal "z - hcnj z = \
  1407 \     hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii";
  1408 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
  1409 by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff,
  1410     hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal,
  1411     complex_diff_cnj,iii_def,hcomplex_mult]));
  1412 qed "hcomplex_diff_hcnj";
  1413 *)
  1414 
  1415 
  1416 lemma hcomplex_hcnj_num_zero_iff: "(hcnj z = 0) = (z = 0)"
  1417 apply (auto simp add: hcomplex_hcnj_zero_iff)
  1418 done
  1419 declare hcomplex_hcnj_num_zero_iff [simp]
  1420 
  1421 lemma hcomplex_zero_num: "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})"
  1422 apply (simp add: hcomplex_zero_def)
  1423 done
  1424 
  1425 lemma hcomplex_one_num: "1 =  Abs_hcomplex (hcomplexrel `` {%n. 1})"
  1426 apply (simp add: hcomplex_one_def)
  1427 done
  1428 
  1429 (*** Real and imaginary stuff ***)
  1430 
  1431 (*Convert???
  1432 Goalw [hcomplex_number_of_def] 
  1433   "((number_of xa :: hcomplex) + iii * number_of ya =  
  1434         number_of xb + iii * number_of yb) =  
  1435    (((number_of xa :: hcomplex) = number_of xb) &  
  1436     ((number_of ya :: hcomplex) = number_of yb))"
  1437 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff,
  1438      hcomplex_hypreal_number_of]));
  1439 qed "hcomplex_number_of_eq_cancel_iff";
  1440 Addsimps [hcomplex_number_of_eq_cancel_iff];
  1441 
  1442 Goalw [hcomplex_number_of_def] 
  1443   "((number_of xa :: hcomplex) + number_of ya * iii = \
  1444 \       number_of xb + number_of yb * iii) = \
  1445 \  (((number_of xa :: hcomplex) = number_of xb) & \
  1446 \   ((number_of ya :: hcomplex) = number_of yb))";
  1447 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA,
  1448     hcomplex_hypreal_number_of]));
  1449 qed "hcomplex_number_of_eq_cancel_iffA";
  1450 Addsimps [hcomplex_number_of_eq_cancel_iffA];
  1451 
  1452 Goalw [hcomplex_number_of_def] 
  1453   "((number_of xa :: hcomplex) + number_of ya * iii = \
  1454 \       number_of xb + iii * number_of yb) = \
  1455 \  (((number_of xa :: hcomplex) = number_of xb) & \
  1456 \   ((number_of ya :: hcomplex) = number_of yb))";
  1457 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB,
  1458     hcomplex_hypreal_number_of]));
  1459 qed "hcomplex_number_of_eq_cancel_iffB";
  1460 Addsimps [hcomplex_number_of_eq_cancel_iffB];
  1461 
  1462 Goalw [hcomplex_number_of_def] 
  1463   "((number_of xa :: hcomplex) + iii * number_of ya = \
  1464 \       number_of xb + number_of yb * iii) = \
  1465 \  (((number_of xa :: hcomplex) = number_of xb) & \
  1466 \   ((number_of ya :: hcomplex) = number_of yb))";
  1467 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC,
  1468      hcomplex_hypreal_number_of]));
  1469 qed "hcomplex_number_of_eq_cancel_iffC";
  1470 Addsimps [hcomplex_number_of_eq_cancel_iffC];
  1471 
  1472 Goalw [hcomplex_number_of_def] 
  1473   "((number_of xa :: hcomplex) + iii * number_of ya = \
  1474 \       number_of xb) = \
  1475 \  (((number_of xa :: hcomplex) = number_of xb) & \
  1476 \   ((number_of ya :: hcomplex) = 0))";
  1477 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2,
  1478     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
  1479 qed "hcomplex_number_of_eq_cancel_iff2";
  1480 Addsimps [hcomplex_number_of_eq_cancel_iff2];
  1481 
  1482 Goalw [hcomplex_number_of_def] 
  1483   "((number_of xa :: hcomplex) + number_of ya * iii = \
  1484 \       number_of xb) = \
  1485 \  (((number_of xa :: hcomplex) = number_of xb) & \
  1486 \   ((number_of ya :: hcomplex) = 0))";
  1487 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a,
  1488     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
  1489 qed "hcomplex_number_of_eq_cancel_iff2a";
  1490 Addsimps [hcomplex_number_of_eq_cancel_iff2a];
  1491 
  1492 Goalw [hcomplex_number_of_def] 
  1493   "((number_of xa :: hcomplex) + iii * number_of ya = \
  1494 \    iii * number_of yb) = \
  1495 \  (((number_of xa :: hcomplex) = 0) & \
  1496 \   ((number_of ya :: hcomplex) = number_of yb))";
  1497 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3,
  1498     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
  1499 qed "hcomplex_number_of_eq_cancel_iff3";
  1500 Addsimps [hcomplex_number_of_eq_cancel_iff3];
  1501 
  1502 Goalw [hcomplex_number_of_def] 
  1503   "((number_of xa :: hcomplex) + number_of ya * iii= \
  1504 \    iii * number_of yb) = \
  1505 \  (((number_of xa :: hcomplex) = 0) & \
  1506 \   ((number_of ya :: hcomplex) = number_of yb))";
  1507 by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a,
  1508     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
  1509 qed "hcomplex_number_of_eq_cancel_iff3a";
  1510 Addsimps [hcomplex_number_of_eq_cancel_iff3a];
  1511 *)
  1512 
  1513 lemma hcomplex_number_of_hcnj [simp]:
  1514      "hcnj (number_of v :: hcomplex) = number_of v"
  1515 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
  1516                hcomplex_hcnj_hcomplex_of_hypreal)
  1517 
  1518 lemma hcomplex_number_of_hcmod [simp]: 
  1519       "hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
  1520 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
  1521                hcmod_hcomplex_of_hypreal)
  1522 
  1523 lemma hcomplex_number_of_hRe [simp]: 
  1524       "hRe(number_of v :: hcomplex) = number_of v"
  1525 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
  1526                hRe_hcomplex_of_hypreal)
  1527 
  1528 lemma hcomplex_number_of_hIm [simp]: 
  1529       "hIm(number_of v :: hcomplex) = 0"
  1530 by (simp only: hcomplex_number_of [symmetric] hcomplex_hypreal_number_of
  1531                hIm_hcomplex_of_hypreal)
  1532 
  1533 
  1534 ML
  1535 {*
  1536 val hcomplex_zero_def = thm"hcomplex_zero_def";
  1537 val hcomplex_one_def = thm"hcomplex_one_def";
  1538 val hcomplex_minus_def = thm"hcomplex_minus_def";
  1539 val hcomplex_diff_def = thm"hcomplex_diff_def";
  1540 val hcomplex_divide_def = thm"hcomplex_divide_def";
  1541 val hcomplex_mult_def = thm"hcomplex_mult_def";
  1542 val hcomplex_add_def = thm"hcomplex_add_def";
  1543 val hcomplex_of_complex_def = thm"hcomplex_of_complex_def";
  1544 val iii_def = thm"iii_def";
  1545 
  1546 val hcomplexrel_iff = thm"hcomplexrel_iff";
  1547 val hcomplexrel_refl = thm"hcomplexrel_refl";
  1548 val hcomplexrel_sym = thm"hcomplexrel_sym";
  1549 val hcomplexrel_trans = thm"hcomplexrel_trans";
  1550 val equiv_hcomplexrel = thm"equiv_hcomplexrel";
  1551 val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff";
  1552 val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex";
  1553 val inj_on_Abs_hcomplex = thm"inj_on_Abs_hcomplex";
  1554 val inj_Rep_hcomplex = thm"inj_Rep_hcomplex";
  1555 val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl";
  1556 val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem";
  1557 val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty";
  1558 val eq_Abs_hcomplex = thm"eq_Abs_hcomplex";
  1559 val hRe = thm"hRe";
  1560 val hIm = thm"hIm";
  1561 val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
  1562 val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
  1563 val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
  1564 val hcomplex_hRe_one = thm"hcomplex_hRe_one";
  1565 val hcomplex_hIm_one = thm"hcomplex_hIm_one";
  1566 val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
  1567 val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
  1568 val hcomplex_add = thm"hcomplex_add";
  1569 val hcomplex_add_commute = thm"hcomplex_add_commute";
  1570 val hcomplex_add_assoc = thm"hcomplex_add_assoc";
  1571 val hcomplex_add_zero_left = thm"hcomplex_add_zero_left";
  1572 val hcomplex_add_zero_right = thm"hcomplex_add_zero_right";
  1573 val hRe_add = thm"hRe_add";
  1574 val hIm_add = thm"hIm_add";
  1575 val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
  1576 val hcomplex_minus = thm"hcomplex_minus";
  1577 val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
  1578 val hRe_minus = thm"hRe_minus";
  1579 val hIm_minus = thm"hIm_minus";
  1580 val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
  1581 val hcomplex_diff = thm"hcomplex_diff";
  1582 val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
  1583 val hcomplex_mult = thm"hcomplex_mult";
  1584 val hcomplex_mult_commute = thm"hcomplex_mult_commute";
  1585 val hcomplex_mult_assoc = thm"hcomplex_mult_assoc";
  1586 val hcomplex_mult_one_left = thm"hcomplex_mult_one_left";
  1587 val hcomplex_mult_one_right = thm"hcomplex_mult_one_right";
  1588 val hcomplex_mult_zero_left = thm"hcomplex_mult_zero_left";
  1589 val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
  1590 val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
  1591 val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
  1592 val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
  1593 val hcomplex_inverse = thm"hcomplex_inverse";
  1594 val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
  1595 val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
  1596 val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
  1597 val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
  1598 val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
  1599 val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
  1600 val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
  1601 val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
  1602 val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
  1603 val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
  1604 val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
  1605 val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
  1606 val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
  1607 val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
  1608 val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
  1609 val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
  1610 val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
  1611 val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
  1612 val hcmod = thm"hcmod";
  1613 val hcmod_zero = thm"hcmod_zero";
  1614 val hcmod_one = thm"hcmod_one";
  1615 val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
  1616 val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
  1617 val hcnj = thm"hcnj";
  1618 val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
  1619 val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
  1620 val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
  1621 val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
  1622 val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
  1623 val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
  1624 val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
  1625 val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
  1626 val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
  1627 val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
  1628 val hcnj_one = thm"hcnj_one";
  1629 val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
  1630 val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
  1631 val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
  1632 val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
  1633 val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
  1634 
  1635 val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
  1636 val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
  1637 val hcmod_minus = thm"hcmod_minus";
  1638 val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
  1639 val hcmod_ge_zero = thm"hcmod_ge_zero";
  1640 val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
  1641 val hcmod_mult = thm"hcmod_mult";
  1642 val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
  1643 val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
  1644 val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
  1645 val hcmod_triangle_squared = thm"hcmod_triangle_squared";
  1646 val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
  1647 val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
  1648 val hcmod_diff_commute = thm"hcmod_diff_commute";
  1649 val hcmod_add_less = thm"hcmod_add_less";
  1650 val hcmod_mult_less = thm"hcmod_mult_less";
  1651 val hcmod_diff_ineq = thm"hcmod_diff_ineq";
  1652 val hcpow = thm"hcpow";
  1653 val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
  1654 val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
  1655 val hcmod_hcpow = thm"hcmod_hcpow";
  1656 val hcpow_minus = thm"hcpow_minus";
  1657 val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
  1658 val hcmod_divide = thm"hcmod_divide";
  1659 val hcpow_mult = thm"hcpow_mult";
  1660 val hcpow_zero = thm"hcpow_zero";
  1661 val hcpow_zero2 = thm"hcpow_zero2";
  1662 val hcpow_not_zero = thm"hcpow_not_zero";
  1663 val hcpow_zero_zero = thm"hcpow_zero_zero";
  1664 val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
  1665 val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
  1666 val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
  1667 val hcomplex_divide = thm"hcomplex_divide";
  1668 val hsgn = thm"hsgn";
  1669 val hsgn_zero = thm"hsgn_zero";
  1670 val hsgn_one = thm"hsgn_one";
  1671 val hsgn_minus = thm"hsgn_minus";
  1672 val hsgn_eq = thm"hsgn_eq";
  1673 val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
  1674 val hcmod_i = thm"hcmod_i";
  1675 val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
  1676 val hRe_hsgn = thm"hRe_hsgn";
  1677 val hIm_hsgn = thm"hIm_hsgn";
  1678 val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
  1679 val hRe_mult_i_eq = thm"hRe_mult_i_eq";
  1680 val hIm_mult_i_eq = thm"hIm_mult_i_eq";
  1681 val hcmod_mult_i = thm"hcmod_mult_i";
  1682 val hcmod_mult_i2 = thm"hcmod_mult_i2";
  1683 val harg = thm"harg";
  1684 val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
  1685 val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
  1686 val complex_split_polar2 = thm"complex_split_polar2";
  1687 val hcomplex_split_polar = thm"hcomplex_split_polar";
  1688 val hcis = thm"hcis";
  1689 val hcis_eq = thm"hcis_eq";
  1690 val hrcis = thm"hrcis";
  1691 val hrcis_Ex = thm"hrcis_Ex";
  1692 val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
  1693 val hRe_hrcis = thm"hRe_hrcis";
  1694 val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
  1695 val hIm_hrcis = thm"hIm_hrcis";
  1696 val hcmod_complex_polar = thm"hcmod_complex_polar";
  1697 val hcmod_hrcis = thm"hcmod_hrcis";
  1698 val hcis_hrcis_eq = thm"hcis_hrcis_eq";
  1699 val hrcis_mult = thm"hrcis_mult";
  1700 val hcis_mult = thm"hcis_mult";
  1701 val hcis_zero = thm"hcis_zero";
  1702 val hrcis_zero_mod = thm"hrcis_zero_mod";
  1703 val hrcis_zero_arg = thm"hrcis_zero_arg";
  1704 val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
  1705 val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
  1706 val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
  1707 val NSDeMoivre = thm"NSDeMoivre";
  1708 val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
  1709 val NSDeMoivre_ext = thm"NSDeMoivre_ext";
  1710 val DeMoivre2 = thm"DeMoivre2";
  1711 val DeMoivre2_ext = thm"DeMoivre2_ext";
  1712 val hcis_inverse = thm"hcis_inverse";
  1713 val hrcis_inverse = thm"hrcis_inverse";
  1714 val hRe_hcis = thm"hRe_hcis";
  1715 val hIm_hcis = thm"hIm_hcis";
  1716 val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
  1717 val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
  1718 val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
  1719 val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
  1720 val hexpi_add = thm"hexpi_add";
  1721 val hcomplex_of_complex_add = thm"hcomplex_of_complex_add";
  1722 val hcomplex_of_complex_mult = thm"hcomplex_of_complex_mult";
  1723 val hcomplex_of_complex_eq_iff = thm"hcomplex_of_complex_eq_iff";
  1724 val hcomplex_of_complex_minus = thm"hcomplex_of_complex_minus";
  1725 val hcomplex_of_complex_one = thm"hcomplex_of_complex_one";
  1726 val hcomplex_of_complex_zero = thm"hcomplex_of_complex_zero";
  1727 val hcomplex_of_complex_zero_iff = thm"hcomplex_of_complex_zero_iff";
  1728 val hcomplex_of_complex_inverse = thm"hcomplex_of_complex_inverse";
  1729 val hcomplex_of_complex_divide = thm"hcomplex_of_complex_divide";
  1730 val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
  1731 val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
  1732 val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
  1733 *}
  1734 
  1735 end