src/HOL/Complex/NSComplex.thy
changeset 14377 f454b3004f8f
parent 14374 61de62096768
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -37,15 +37,15 @@
     1.4    hcomplex_diff_def:
     1.5    "w - z == w + -(z::hcomplex)"
     1.6  
     1.7 +  hcinv_def:
     1.8 +  "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
     1.9 +                    hcomplexrel `` {%n. inverse(X n)})"
    1.10 +
    1.11  constdefs
    1.12  
    1.13    hcomplex_of_complex :: "complex => hcomplex"
    1.14    "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
    1.15  
    1.16 -  hcinv  :: "hcomplex => hcomplex"
    1.17 -  "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P).
    1.18 -                    hcomplexrel `` {%n. inverse(X n)})"
    1.19 -
    1.20    (*--- real and Imaginary parts ---*)
    1.21  
    1.22    hRe :: "hcomplex => hypreal"
    1.23 @@ -99,6 +99,11 @@
    1.24    "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
    1.25  
    1.26  
    1.27 +constdefs
    1.28 +  HComplex :: "[hypreal,hypreal] => hcomplex"
    1.29 +   "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"
    1.30 +
    1.31 +
    1.32  defs (overloaded)
    1.33  
    1.34    (*----------- division ----------*)
    1.35 @@ -182,8 +187,7 @@
    1.36  apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
    1.37  done
    1.38  
    1.39 -(*??delete*)
    1.40 -lemma hcomplexrel_iff [iff]:
    1.41 +lemma hcomplexrel_iff [simp]:
    1.42     "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    1.43  by (simp add: hcomplexrel_def)
    1.44  
    1.45 @@ -195,7 +199,7 @@
    1.46        Abs_hypreal(hyprel `` {%n. Re(X n)})"
    1.47  apply (simp add: hRe_def)
    1.48  apply (rule_tac f = Abs_hypreal in arg_cong)
    1.49 -apply (auto, ultra)
    1.50 +apply (auto iff: hcomplexrel_iff, ultra)
    1.51  done
    1.52  
    1.53  lemma hIm:
    1.54 @@ -203,17 +207,20 @@
    1.55        Abs_hypreal(hyprel `` {%n. Im(X n)})"
    1.56  apply (simp add: hIm_def)
    1.57  apply (rule_tac f = Abs_hypreal in arg_cong)
    1.58 -apply (auto, ultra)
    1.59 +apply (auto iff: hcomplexrel_iff, ultra)
    1.60  done
    1.61  
    1.62  lemma hcomplex_hRe_hIm_cancel_iff:
    1.63       "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
    1.64  apply (rule eq_Abs_hcomplex [of z])
    1.65  apply (rule eq_Abs_hcomplex [of w])
    1.66 -apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
    1.67 +apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
    1.68  apply (ultra+)
    1.69  done
    1.70  
    1.71 +lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
    1.72 +by (simp add: hcomplex_hRe_hIm_cancel_iff) 
    1.73 +
    1.74  lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
    1.75  by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
    1.76  
    1.77 @@ -231,14 +238,15 @@
    1.78  
    1.79  lemma hcomplex_add_congruent2:
    1.80      "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
    1.81 -by (auto simp add: congruent2_def, ultra)
    1.82 +by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) 
    1.83  
    1.84  lemma hcomplex_add:
    1.85 -  "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
    1.86 -   Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
    1.87 +  "Abs_hcomplex(hcomplexrel``{%n. X n}) + 
    1.88 +   Abs_hcomplex(hcomplexrel``{%n. Y n}) =
    1.89 +     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
    1.90  apply (simp add: hcomplex_add_def)
    1.91  apply (rule_tac f = Abs_hcomplex in arg_cong)
    1.92 -apply (auto, ultra)
    1.93 +apply (auto simp add: iff: hcomplexrel_iff, ultra) 
    1.94  done
    1.95  
    1.96  lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
    1.97 @@ -286,7 +294,7 @@
    1.98        Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
    1.99  apply (simp add: hcomplex_minus_def)
   1.100  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.101 -apply (auto, ultra)
   1.102 +apply (auto iff: hcomplexrel_iff, ultra)
   1.103  done
   1.104  
   1.105  lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
   1.106 @@ -303,7 +311,7 @@
   1.107       Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
   1.108  apply (simp add: hcomplex_mult_def)
   1.109  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.110 -apply (auto, ultra)
   1.111 +apply (auto iff: hcomplexrel_iff, ultra)
   1.112  done
   1.113  
   1.114  lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
   1.115 @@ -350,7 +358,7 @@
   1.116        Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
   1.117  apply (simp add: hcinv_def)
   1.118  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.119 -apply (auto, ultra)
   1.120 +apply (auto iff: hcomplexrel_iff, ultra)
   1.121  done
   1.122  
   1.123  lemma hcomplex_mult_inv_left:
   1.124 @@ -428,6 +436,15 @@
   1.125  apply (simp add: minus_equation_iff [of x y])
   1.126  done
   1.127  
   1.128 +lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
   1.129 +by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
   1.130 +
   1.131 +lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
   1.132 +by (simp add: mult_assoc [symmetric])
   1.133 +
   1.134 +lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
   1.135 +by (simp add: iii_def hcomplex_zero_def)
   1.136 +
   1.137  
   1.138  subsection{*More Multiplication Laws*}
   1.139  
   1.140 @@ -469,7 +486,7 @@
   1.141    "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
   1.142        Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
   1.143  apply (simp add: hcomplex_of_hypreal_def)
   1.144 -apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
   1.145 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
   1.146  done
   1.147  
   1.148  lemma hcomplex_of_hypreal_cancel_iff [iff]:
   1.149 @@ -541,6 +558,34 @@
   1.150  by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
   1.151  
   1.152  
   1.153 +subsection{*HComplex theorems*}
   1.154 +
   1.155 +lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
   1.156 +apply (rule eq_Abs_hypreal [of x])
   1.157 +apply (rule eq_Abs_hypreal [of y])
   1.158 +apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   1.159 +done
   1.160 +
   1.161 +lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
   1.162 +apply (rule eq_Abs_hypreal [of x])
   1.163 +apply (rule eq_Abs_hypreal [of y])
   1.164 +apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   1.165 +done
   1.166 +
   1.167 +text{*Relates the two nonstandard constructions*}
   1.168 +lemma HComplex_eq_Abs_hcomplex_Complex:
   1.169 +     "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
   1.170 +      Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
   1.171 +by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) 
   1.172 +
   1.173 +lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
   1.174 +by (simp add: hcomplex_equality) 
   1.175 +
   1.176 +lemma hcomplex_induct [case_names rect, induct type: hcomplex]:
   1.177 +     "(\<And>x y. P (HComplex x y)) ==> P z"
   1.178 +by (rule hcomplex_surj [THEN subst], blast)
   1.179 +
   1.180 +
   1.181  subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   1.182  
   1.183  lemma hcmod:
   1.184 @@ -549,12 +594,11 @@
   1.185  
   1.186  apply (simp add: hcmod_def)
   1.187  apply (rule_tac f = Abs_hypreal in arg_cong)
   1.188 -apply (auto, ultra)
   1.189 +apply (auto iff: hcomplexrel_iff, ultra)
   1.190  done
   1.191  
   1.192  lemma hcmod_zero [simp]: "hcmod(0) = 0"
   1.193 -apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
   1.194 -done
   1.195 +by (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
   1.196  
   1.197  lemma hcmod_one [simp]: "hcmod(1) = 1"
   1.198  by (simp add: hcomplex_one_def hcmod hypreal_one_num)
   1.199 @@ -569,6 +613,64 @@
   1.200        hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
   1.201  by simp
   1.202  
   1.203 +lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')"
   1.204 +apply (rule iffI) 
   1.205 + prefer 2 apply simp 
   1.206 +apply (simp add: HComplex_def iii_def) 
   1.207 +apply (rule eq_Abs_hypreal [of x])
   1.208 +apply (rule eq_Abs_hypreal [of y])
   1.209 +apply (rule eq_Abs_hypreal [of x'])
   1.210 +apply (rule eq_Abs_hypreal [of y'])
   1.211 +apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
   1.212 +apply (ultra+) 
   1.213 +done
   1.214 +
   1.215 +lemma HComplex_add [simp]:
   1.216 +     "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
   1.217 +by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib) 
   1.218 +
   1.219 +lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
   1.220 +by (simp add: HComplex_def hcomplex_of_hypreal_minus) 
   1.221 +
   1.222 +lemma HComplex_diff [simp]:
   1.223 +     "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
   1.224 +by (simp add: diff_minus)
   1.225 +
   1.226 +lemma HComplex_mult [simp]:
   1.227 +  "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
   1.228 +by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus 
   1.229 +       hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
   1.230 +       add_ac mult_ac right_distrib)
   1.231 +
   1.232 +(*HComplex_inverse is proved below*)
   1.233 +
   1.234 +lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0"
   1.235 +by (simp add: HComplex_def)
   1.236 +
   1.237 +lemma HComplex_add_hcomplex_of_hypreal [simp]:
   1.238 +     "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
   1.239 +by (simp add: hcomplex_of_hypreal_eq)
   1.240 +
   1.241 +lemma hcomplex_of_hypreal_add_HComplex [simp]:
   1.242 +     "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
   1.243 +by (simp add: i_def hcomplex_of_hypreal_eq)
   1.244 +
   1.245 +lemma HComplex_mult_hcomplex_of_hypreal:
   1.246 +     "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
   1.247 +by (simp add: hcomplex_of_hypreal_eq)
   1.248 +
   1.249 +lemma hcomplex_of_hypreal_mult_HComplex:
   1.250 +     "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
   1.251 +by (simp add: i_def hcomplex_of_hypreal_eq)
   1.252 +
   1.253 +lemma i_hcomplex_of_hypreal [simp]:
   1.254 +     "iii * hcomplex_of_hypreal r = HComplex 0 r"
   1.255 +by (simp add: HComplex_def)
   1.256 +
   1.257 +lemma hcomplex_of_hypreal_i [simp]:
   1.258 +     "hcomplex_of_hypreal r * iii = HComplex 0 r"
   1.259 +by (simp add: mult_commute) 
   1.260 +
   1.261  
   1.262  subsection{*Conjugation*}
   1.263  
   1.264 @@ -577,7 +679,7 @@
   1.265     Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
   1.266  apply (simp add: hcnj_def)
   1.267  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.268 -apply (auto, ultra)
   1.269 +apply (auto iff: hcomplexrel_iff, ultra)
   1.270  done
   1.271  
   1.272  lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
   1.273 @@ -777,7 +879,7 @@
   1.274     Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
   1.275  apply (simp add: hcpow_def)
   1.276  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.277 -apply (auto, ultra)
   1.278 +apply (auto iff: hcomplexrel_iff, ultra)
   1.279  done
   1.280  
   1.281  lemma hcomplex_of_hypreal_hyperpow:
   1.282 @@ -817,6 +919,9 @@
   1.283    show "z^(Suc n) = z * (z^n)" by simp
   1.284  qed
   1.285  
   1.286 +lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
   1.287 +by (simp add: power2_eq_square)
   1.288 +
   1.289  
   1.290  lemma hcomplex_of_hypreal_pow:
   1.291       "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
   1.292 @@ -872,15 +977,6 @@
   1.293  lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
   1.294  by (blast intro: ccontr dest: hcpow_not_zero)
   1.295  
   1.296 -lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
   1.297 -by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
   1.298 -
   1.299 -lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
   1.300 -by (simp add: numeral_2_eq_2)
   1.301 -
   1.302 -lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
   1.303 -by (simp add: iii_def hcomplex_zero_def)
   1.304 -
   1.305  lemma hcomplex_divide:
   1.306    "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
   1.307     Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
   1.308 @@ -888,6 +984,7 @@
   1.309  
   1.310  
   1.311  
   1.312 +
   1.313  subsection{*The Function @{term hsgn}*}
   1.314  
   1.315  lemma hsgn:
   1.316 @@ -895,7 +992,7 @@
   1.317        Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
   1.318  apply (simp add: hsgn_def)
   1.319  apply (rule_tac f = Abs_hcomplex in arg_cong)
   1.320 -apply (auto, ultra)
   1.321 +apply (auto iff: hcomplexrel_iff, ultra)
   1.322  done
   1.323  
   1.324  lemma hsgn_zero [simp]: "hsgn 0 = 0"
   1.325 @@ -914,144 +1011,33 @@
   1.326  apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
   1.327  done
   1.328  
   1.329 -lemma lemma_hypreal_P_EX2:
   1.330 -     "(\<exists>(x::hypreal) y. P x y) =
   1.331 -      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
   1.332 -apply auto
   1.333 -apply (rule_tac z = x in eq_Abs_hypreal)
   1.334 -apply (rule_tac z = y in eq_Abs_hypreal, auto)
   1.335 -done
   1.336  
   1.337 -lemma complex_split2:
   1.338 -     "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
   1.339 -by (blast intro: complex_split)
   1.340 -
   1.341 -(* Interesting proof! *)
   1.342 -lemma hcomplex_split:
   1.343 -     "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
   1.344 -apply (rule eq_Abs_hcomplex [of z])
   1.345 -apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
   1.346 -apply (cut_tac z = x in complex_split2)
   1.347 -apply (drule choice, safe)+
   1.348 -apply (rule_tac x = f in exI)
   1.349 -apply (rule_tac x = fa in exI, auto)
   1.350 -done
   1.351 -
   1.352 -lemma hRe_hcomplex_i [simp]:
   1.353 -     "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
   1.354 -apply (rule eq_Abs_hypreal [of x])
   1.355 -apply (rule eq_Abs_hypreal [of y])
   1.356 -apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   1.357 -done
   1.358 -
   1.359 -lemma hIm_hcomplex_i [simp]:
   1.360 -     "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
   1.361 +lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
   1.362  apply (rule eq_Abs_hypreal [of x])
   1.363 -apply (rule eq_Abs_hypreal [of y])
   1.364 -apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
   1.365 -done
   1.366 -
   1.367 -lemma hcmod_i:
   1.368 -     "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
   1.369 -      ( *f* sqrt) (x ^ 2 + y ^ 2)"
   1.370 -apply (rule eq_Abs_hypreal [of x])
   1.371 -apply (rule eq_Abs_hypreal [of y])
   1.372 -apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
   1.373 -done
   1.374 -
   1.375 -lemma hcomplex_eq_hRe_eq:
   1.376 -     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
   1.377 -      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
   1.378 -       ==> xa = xb"
   1.379 -apply (simp add: iii_def)
   1.380 -apply (rule eq_Abs_hypreal [of xa])
   1.381 -apply (rule eq_Abs_hypreal [of ya])
   1.382 -apply (rule eq_Abs_hypreal [of xb])
   1.383 -apply (rule eq_Abs_hypreal [of yb])
   1.384 -apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
   1.385 -done
   1.386 -
   1.387 -lemma hcomplex_eq_hIm_eq:
   1.388 -     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
   1.389 -      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
   1.390 -       ==> ya = yb"
   1.391 -apply (simp add: iii_def)
   1.392 -apply (rule eq_Abs_hypreal [of xa])
   1.393 -apply (rule eq_Abs_hypreal [of ya])
   1.394 -apply (rule eq_Abs_hypreal [of xb])
   1.395 -apply (rule eq_Abs_hypreal [of yb])
   1.396 -apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
   1.397 +apply (rule eq_Abs_hypreal [of y]) 
   1.398 +apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
   1.399 +                 hypreal_mult hypreal_add hcmod numeral_2_eq_2)
   1.400  done
   1.401  
   1.402 -lemma hcomplex_eq_cancel_iff [simp]:
   1.403 -     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
   1.404 -       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
   1.405 -      ((xa = xb) & (ya = yb))"
   1.406 -by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
   1.407 -
   1.408 -lemma hcomplex_eq_cancel_iffA [iff]:
   1.409 -     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   1.410 -       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
   1.411 -apply (simp add: hcomplex_mult_commute)
   1.412 -done
   1.413 -
   1.414 -lemma hcomplex_eq_cancel_iffB [iff]:
   1.415 -     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
   1.416 -       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
   1.417 -apply (simp add: hcomplex_mult_commute)
   1.418 -done
   1.419 -
   1.420 -lemma hcomplex_eq_cancel_iffC [iff]:
   1.421 -     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
   1.422 -       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
   1.423 -apply (simp add: hcomplex_mult_commute)
   1.424 -done
   1.425 +lemma hcomplex_eq_cancel_iff1 [simp]:
   1.426 +     "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
   1.427 +by (simp add: hcomplex_of_hypreal_eq)
   1.428  
   1.429  lemma hcomplex_eq_cancel_iff2 [simp]:
   1.430 -     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   1.431 -      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   1.432 -apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff)
   1.433 -apply (simp del: hcomplex_eq_cancel_iff)
   1.434 -done
   1.435 +     "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   1.436 +by (simp add: hcomplex_of_hypreal_eq)
   1.437  
   1.438 -lemma hcomplex_eq_cancel_iff2a [simp]:
   1.439 -     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   1.440 -      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
   1.441 -apply (simp add: hcomplex_mult_commute)
   1.442 -done
   1.443 -
   1.444 -lemma hcomplex_eq_cancel_iff3 [simp]:
   1.445 -     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
   1.446 -      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
   1.447 -apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff)
   1.448 -apply (simp del: hcomplex_eq_cancel_iff)
   1.449 -done
   1.450 +lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
   1.451 +by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
   1.452  
   1.453 -lemma hcomplex_eq_cancel_iff3a [simp]:
   1.454 -     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
   1.455 -      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
   1.456 -apply (simp add: hcomplex_mult_commute)
   1.457 -done
   1.458 +lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
   1.459 +by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
   1.460  
   1.461 -lemma hcomplex_split_hRe_zero:
   1.462 -     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
   1.463 -      ==> x = 0"
   1.464 -apply (simp add: iii_def)
   1.465 -apply (rule eq_Abs_hypreal [of x])
   1.466 -apply (rule eq_Abs_hypreal [of y])
   1.467 -apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
   1.468 -apply (simp add: complex_split_Re_zero)
   1.469 -done
   1.470 +lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
   1.471 +by (insert hcomplex_of_hypreal_i [of 1], simp)
   1.472  
   1.473 -lemma hcomplex_split_hIm_zero:
   1.474 -     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
   1.475 -      ==> y = 0"
   1.476 -apply (simp add: iii_def)
   1.477 -apply (rule eq_Abs_hypreal [of x])
   1.478 -apply (rule eq_Abs_hypreal [of y])
   1.479 -apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
   1.480 -apply (simp add: complex_split_Im_zero)
   1.481 -done
   1.482 +lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
   1.483 +by (simp add: i_eq_HComplex_0_1) 
   1.484  
   1.485  lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
   1.486  apply (rule eq_Abs_hcomplex [of z])
   1.487 @@ -1064,8 +1050,7 @@
   1.488  done
   1.489  
   1.490  lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
   1.491 -apply (auto intro: real_sum_squares_cancel)
   1.492 -done
   1.493 +by (auto intro: real_sum_squares_cancel)
   1.494  
   1.495  lemma hcomplex_inverse_complex_split:
   1.496       "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
   1.497 @@ -1074,8 +1059,16 @@
   1.498  apply (rule eq_Abs_hypreal [of x])
   1.499  apply (rule eq_Abs_hypreal [of y])
   1.500  apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
   1.501 +apply (simp add: diff_minus) 
   1.502  done
   1.503  
   1.504 +lemma HComplex_inverse:
   1.505 +     "inverse (HComplex x y) =
   1.506 +      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
   1.507 +by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
   1.508 +
   1.509 +
   1.510 +
   1.511  lemma hRe_mult_i_eq[simp]:
   1.512      "hRe (iii * hcomplex_of_hypreal y) = 0"
   1.513  apply (simp add: iii_def)
   1.514 @@ -1096,7 +1089,7 @@
   1.515  done
   1.516  
   1.517  lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
   1.518 -by (simp add: hcomplex_mult_commute)
   1.519 +by (simp only: hcmod_mult_i hcomplex_mult_commute)
   1.520  
   1.521  (*---------------------------------------------------------------------------*)
   1.522  (*  harg                                                                     *)
   1.523 @@ -1105,31 +1098,29 @@
   1.524  lemma harg:
   1.525    "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
   1.526        Abs_hypreal(hyprel `` {%n. arg (X n)})"
   1.527 -
   1.528  apply (simp add: harg_def)
   1.529  apply (rule_tac f = Abs_hypreal in arg_cong)
   1.530 -apply (auto, ultra)
   1.531 +apply (auto iff: hcomplexrel_iff, ultra)
   1.532  done
   1.533  
   1.534  lemma cos_harg_i_mult_zero_pos:
   1.535 -     "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   1.536 +     "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   1.537  apply (rule eq_Abs_hypreal [of y])
   1.538 -apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
   1.539 -                hypreal_zero_num hypreal_less starfun harg, ultra)
   1.540 +apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
   1.541 +                hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
   1.542  done
   1.543  
   1.544  lemma cos_harg_i_mult_zero_neg:
   1.545 -     "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   1.546 +     "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   1.547  apply (rule eq_Abs_hypreal [of y])
   1.548 -apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
   1.549 -                      hypreal_zero_num hypreal_less starfun harg, ultra)
   1.550 +apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
   1.551 +                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
   1.552  done
   1.553  
   1.554  lemma cos_harg_i_mult_zero [simp]:
   1.555 -     "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
   1.556 -apply (cut_tac x = y and y = 0 in linorder_less_linear)
   1.557 -apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
   1.558 -done
   1.559 +     "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   1.560 +by (auto simp add: linorder_neq_iff
   1.561 +                   cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
   1.562  
   1.563  lemma hcomplex_of_hypreal_zero_iff [simp]:
   1.564       "(hcomplex_of_hypreal y = 0) = (y = 0)"
   1.565 @@ -1141,16 +1132,21 @@
   1.566  subsection{*Polar Form for Nonstandard Complex Numbers*}
   1.567  
   1.568  lemma complex_split_polar2:
   1.569 -     "\<forall>n. \<exists>r a. (z n) = complex_of_real r *
   1.570 -      (complex_of_real(cos a) + ii * complex_of_real(sin a))"
   1.571 -apply (blast intro: complex_split_polar)
   1.572 +     "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
   1.573 +by (blast intro: complex_split_polar)
   1.574 +
   1.575 +lemma lemma_hypreal_P_EX2:
   1.576 +     "(\<exists>(x::hypreal) y. P x y) =
   1.577 +      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
   1.578 +apply auto
   1.579 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.580 +apply (rule_tac z = y in eq_Abs_hypreal, auto)
   1.581  done
   1.582  
   1.583  lemma hcomplex_split_polar:
   1.584 -  "\<exists>r a. z = hcomplex_of_hypreal r *
   1.585 -   (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
   1.586 +  "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   1.587  apply (rule eq_Abs_hcomplex [of z])
   1.588 -apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
   1.589 +apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
   1.590  apply (cut_tac z = x in complex_split_polar2)
   1.591  apply (drule choice, safe)+
   1.592  apply (rule_tac x = f in exI)
   1.593 @@ -1161,7 +1157,7 @@
   1.594    "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
   1.595        Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
   1.596  apply (simp add: hcis_def)
   1.597 -apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
   1.598 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
   1.599  done
   1.600  
   1.601  lemma hcis_eq:
   1.602 @@ -1178,35 +1174,38 @@
   1.603  by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
   1.604  
   1.605  lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
   1.606 -apply (simp add: hrcis_def hcis_eq)
   1.607 +apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
   1.608  apply (rule hcomplex_split_polar)
   1.609  done
   1.610  
   1.611  lemma hRe_hcomplex_polar [simp]:
   1.612 -     "hRe(hcomplex_of_hypreal r *
   1.613 -      (hcomplex_of_hypreal(( *f* cos) a) +
   1.614 -       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
   1.615 -by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
   1.616 +     "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   1.617 +      r * ( *f* cos) a"
   1.618 +by (simp add: hcomplex_of_hypreal_mult_HComplex)
   1.619  
   1.620  lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
   1.621  by (simp add: hrcis_def hcis_eq)
   1.622  
   1.623  lemma hIm_hcomplex_polar [simp]:
   1.624 -     "hIm(hcomplex_of_hypreal r *
   1.625 -      (hcomplex_of_hypreal(( *f* cos) a) +
   1.626 -       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
   1.627 -by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
   1.628 +     "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   1.629 +      r * ( *f* sin) a"
   1.630 +by (simp add: hcomplex_of_hypreal_mult_HComplex)
   1.631  
   1.632  lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
   1.633  by (simp add: hrcis_def hcis_eq)
   1.634  
   1.635 +
   1.636 +lemma hcmod_unit_one [simp]:
   1.637 +     "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
   1.638 +apply (rule eq_Abs_hypreal [of a]) 
   1.639 +apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
   1.640 +                 hcomplex_mult hcmod hcomplex_add hypreal_one_def)
   1.641 +done
   1.642 +
   1.643  lemma hcmod_complex_polar [simp]:
   1.644 -     "hcmod (hcomplex_of_hypreal r *
   1.645 -      (hcomplex_of_hypreal(( *f* cos) a) +
   1.646 -       iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
   1.647 -apply (rule eq_Abs_hypreal [of r])
   1.648 -apply (rule eq_Abs_hypreal [of a])
   1.649 -apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
   1.650 +     "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   1.651 +      abs r"
   1.652 +apply (simp only: hcmod_mult hcmod_unit_one, simp)  
   1.653  done
   1.654  
   1.655  lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
   1.656 @@ -1316,20 +1315,16 @@
   1.657  done
   1.658  
   1.659  lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
   1.660 -apply (simp add: NSDeMoivre)
   1.661 -done
   1.662 +by (simp add: NSDeMoivre)
   1.663  
   1.664  lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
   1.665 -apply (simp add: NSDeMoivre)
   1.666 -done
   1.667 +by (simp add: NSDeMoivre)
   1.668  
   1.669  lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
   1.670 -apply (simp add: NSDeMoivre_ext)
   1.671 -done
   1.672 +by (simp add: NSDeMoivre_ext)
   1.673  
   1.674  lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
   1.675 -apply (simp add: NSDeMoivre_ext)
   1.676 -done
   1.677 +by (simp add: NSDeMoivre_ext)
   1.678  
   1.679  lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
   1.680  apply (simp add: hexpi_def)
   1.681 @@ -1545,27 +1540,11 @@
   1.682  val hsgn_minus = thm"hsgn_minus";
   1.683  val hsgn_eq = thm"hsgn_eq";
   1.684  val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
   1.685 -val complex_split2 = thm"complex_split2";
   1.686 -val hcomplex_split = thm"hcomplex_split";
   1.687 -val hRe_hcomplex_i = thm"hRe_hcomplex_i";
   1.688 -val hIm_hcomplex_i = thm"hIm_hcomplex_i";
   1.689  val hcmod_i = thm"hcmod_i";
   1.690 -val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq";
   1.691 -val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq";
   1.692 -val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff";
   1.693 -val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA";
   1.694 -val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB";
   1.695 -val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC";
   1.696  val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
   1.697 -val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a";
   1.698 -val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3";
   1.699 -val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a";
   1.700 -val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero";
   1.701 -val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero";
   1.702  val hRe_hsgn = thm"hRe_hsgn";
   1.703  val hIm_hsgn = thm"hIm_hsgn";
   1.704  val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
   1.705 -val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split";
   1.706  val hRe_mult_i_eq = thm"hRe_mult_i_eq";
   1.707  val hIm_mult_i_eq = thm"hIm_mult_i_eq";
   1.708  val hcmod_mult_i = thm"hcmod_mult_i";