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