# HG changeset patch
# User paulson
# Date 1075974328 -3600
# Node ID f454b3004f8f574d0f91dc16f21c735cb1d0c0e0
# Parent  9fe787a90a48bd88b58c3dae19b9c415294cc529
tidying up, especially the Complex numbers

diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/CStar.ML
--- a/src/HOL/Complex/CStar.ML	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/CStar.ML	Thu Feb 05 10:45:28 2004 +0100
@@ -194,7 +194,7 @@
 
 Goalw [congruent_def] 
       "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (ALLGOALS(Ultra_tac));
 qed "starfunC_congruent";
 
@@ -203,7 +203,7 @@
       "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \      Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunC";
 
@@ -219,7 +219,7 @@
       "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \      Abs_hypreal(hyprel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunCR";
 
@@ -523,7 +523,7 @@
 
 Goalw [congruent_def] 
       "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})";
-by (safe_tac (claset()));
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (ALLGOALS(Fuf_tac));
 qed "starfunC_n_congruent";
 
@@ -531,7 +531,7 @@
      "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
 \     Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})";
 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
-by Auto_tac;
+by (auto_tac (clasimpset() addIffs [hcomplexrel_iff]));
 by (Ultra_tac 1);
 qed "starfunC_n";
 
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Thu Feb 05 10:45:28 2004 +0100
@@ -3,12 +3,10 @@
     Copyright:   2001 University of Edinburgh
 *)
 
-header {* Complex numbers *}
+header {* Complex Numbers: Rectangular and Polar Representations *}
 
 theory Complex = HLog:
 
-subsection {* Representation of complex numbers *}
-
 datatype complex = Complex real real
 
 instance complex :: zero ..
@@ -89,7 +87,7 @@
 
   (* abbreviation for (cos a + i sin a) *)
   cis :: "real => complex"
-  "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"
+  "cis a == Complex (cos a) (sin a)"
 
   (* abbreviation for r*(cos a + i sin a) *)
   rcis :: "[real, real] => complex"
@@ -139,7 +137,7 @@
 
 subsection{*Unary Minus*}
 
-lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)"
+lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)"
 by (simp add: complex_minus_def)
 
 lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
@@ -151,7 +149,8 @@
 
 subsection{*Addition*}
 
-lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
+lemma complex_add [simp]:
+     "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
 by (simp add: complex_add_def)
 
 lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
@@ -188,7 +187,7 @@
 
 subsection{*Multiplication*}
 
-lemma complex_mult:
+lemma complex_mult [simp]:
      "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
 by (simp add: complex_mult_def)
 
@@ -208,7 +207,7 @@
 
 subsection{*Inverse*}
 
-lemma complex_inverse:
+lemma complex_inverse [simp]:
      "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
 by (simp add: complex_inverse_def)
 
@@ -272,6 +271,28 @@
 
 subsection{*Embedding Properties for @{term complex_of_real} Map*}
 
+lemma Complex_add_complex_of_real [simp]:
+     "Complex x y + complex_of_real r = Complex (x+r) y"
+by (simp add: complex_of_real_def)
+
+lemma complex_of_real_add_Complex [simp]:
+     "complex_of_real r + Complex x y = Complex (r+x) y"
+by (simp add: i_def complex_of_real_def)
+
+lemma Complex_mult_complex_of_real:
+     "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
+by (simp add: complex_of_real_def)
+
+lemma complex_of_real_mult_Complex:
+     "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
+by (simp add: i_def complex_of_real_def)
+
+lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
+by (simp add: i_def complex_of_real_def)
+
+lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
+by (simp add: i_def complex_of_real_def)
+
 lemma complex_of_real_one [simp]: "complex_of_real 1 = 1"
 by (simp add: complex_one_def complex_of_real_def)
 
@@ -313,7 +334,7 @@
                  real_divide_def)
 done
 
-lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
+lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
 by (simp add: cmod_def)
 
 lemma complex_mod_zero [simp]: "cmod(0) = 0"
@@ -330,6 +351,46 @@
 by simp
 
 
+subsection{*The Functions @{term Re} and @{term Im}*}
+
+lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
+by (induct z, induct w, simp add: complex_mult)
+
+lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z"
+by (induct z, induct w, simp add: complex_mult)
+
+lemma Re_i_times [simp]: "Re(ii * z) = - Im z"
+by (simp add: complex_Re_mult_eq) 
+
+lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
+by (simp add: complex_Re_mult_eq) 
+
+lemma Im_i_times [simp]: "Im(ii * z) = Re z"
+by (simp add: complex_Im_mult_eq) 
+
+lemma Im_times_i [simp]: "Im(z * ii) = Re z"
+by (simp add: complex_Im_mult_eq) 
+
+lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Re_mult_complex_of_real [simp]:
+     "Re (z * complex_of_real c) = Re(z) * c"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Im_mult_complex_of_real [simp]:
+     "Im (z * complex_of_real c) = Im(z) * c"
+by (simp add: complex_Im_mult_eq)
+
+lemma complex_Re_mult_complex_of_real2 [simp]:
+     "Re (complex_of_real c * z) = c * Re(z)"
+by (simp add: complex_Re_mult_eq)
+
+lemma complex_Im_mult_complex_of_real2 [simp]:
+     "Im (complex_of_real c * z) = c * Im(z)"
+by (simp add: complex_Im_mult_eq)
+ 
+
 subsection{*Conjugation is an Automorphism*}
 
 lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
@@ -420,14 +481,20 @@
 
 lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
 apply (induct x, induct y)
-apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric]
-         simp del: realpow_Suc)
+apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric])
 apply (rule_tac n = 1 in power_inject_base)
 apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
 apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
                       add_ac mult_ac)
 done
 
+lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
+by (simp add: cmod_def) 
+
+lemma cmod_complex_polar [simp]:
+     "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
+by (simp only: cmod_unit_one complex_mod_mult, simp) 
+
 lemma complex_mod_add_squared_eq:
      "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
 apply (induct x, induct y)
@@ -506,10 +573,7 @@
 done
 
 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
-by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse)
-
-lemma complex_inverse_divide [simp]: "inverse(x/y) = y/(x::complex)"
-by (simp add: complex_divide_def inverse_mult_distrib mult_commute)
+by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
 
 
 subsection{*Exponentiation*}
@@ -566,20 +630,7 @@
 by (simp add: sgn_def)
 
 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
-apply (simp add: sgn_def)
-done
-
-lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
-apply (induct z)
-apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
-done
-
-(*????delete????*)
-lemma Re_complex_i [simp]: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
-by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
-
-lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
-by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
+by (simp add: sgn_def)
 
 lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
 by (simp add: i_def complex_of_real_def complex_mult complex_add)
@@ -587,78 +638,22 @@
 lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
 by (simp add: i_def complex_one_def complex_mult complex_minus)
 
-lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
-      sqrt (x ^ 2 + y ^ 2)"
-by (simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
-
-lemma complex_eq_Re_eq:
-     "complex_of_real xa + ii * complex_of_real ya =
-      complex_of_real xb + ii * complex_of_real yb
-       ==> xa = xb"
-by (simp add: complex_of_real_def i_def complex_mult complex_add)
-
-lemma complex_eq_Im_eq:
-     "complex_of_real xa + ii * complex_of_real ya =
-      complex_of_real xb + ii * complex_of_real yb
-       ==> ya = yb"
-by (simp add: complex_of_real_def i_def complex_mult complex_add)
-
-(*FIXME: tidy up this mess by fixing a canonical form for complex expressions,
-e.g. x + y*ii*)
-
-lemma complex_eq_cancel_iff [iff]:
-     "(complex_of_real xa + ii * complex_of_real ya =
-       complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
-by (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
-
-lemma complex_eq_cancel_iffA [iff]:
-     "(complex_of_real xa + complex_of_real ya * ii =
-       complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
-by (simp add: mult_commute)
-
-lemma complex_eq_cancel_iffB [iff]:
-     "(complex_of_real xa + complex_of_real ya * ii =
-       complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
-by (auto simp add: mult_commute)
-
-lemma complex_eq_cancel_iffC [iff]:
-     "(complex_of_real xa + ii * complex_of_real ya  =
-       complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
-by (auto simp add: mult_commute)
-
 lemma complex_eq_cancel_iff2 [simp]:
-     "(complex_of_real x + ii * complex_of_real y =
-      complex_of_real xa) = (x = xa & y = 0)"
-apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff)
-apply (simp del: complex_eq_cancel_iff)
-done
+     "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
+by (simp add: complex_of_real_def) 
 
 lemma complex_eq_cancel_iff2a [simp]:
-     "(complex_of_real x + complex_of_real y * ii =
-      complex_of_real xa) = (x = xa & y = 0)"
-by (auto simp add: mult_commute)
+     "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
+by (simp add: complex_of_real_def)
 
-lemma complex_eq_cancel_iff3 [simp]:
-     "(complex_of_real x + ii * complex_of_real y =
-      ii * complex_of_real ya) = (x = 0 & y = ya)"
-apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff)
-apply (simp del: complex_eq_cancel_iff)
-done
+lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
+by (simp add: complex_zero_def)
 
-lemma complex_eq_cancel_iff3a [simp]:
-     "(complex_of_real x + complex_of_real y * ii =
-      ii * complex_of_real ya) = (x = 0 & y = ya)"
-by (auto simp add: mult_commute)
+lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
+by (simp add: complex_one_def)
 
-lemma complex_split_Re_zero:
-     "complex_of_real x + ii * complex_of_real y = 0
-      ==> x = 0"
-by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
-
-lemma complex_split_Im_zero:
-     "complex_of_real x + ii * complex_of_real y = 0
-      ==> y = 0"
-by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
+lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
+by (simp add: i_def)
 
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
 apply (induct z)
@@ -687,77 +682,53 @@
 lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
 by (auto simp add: complex_zero_def complex_of_real_def)
 
-lemma Re_mult_i_eq [simp]: "Re (ii * complex_of_real y) = 0"
-by (simp add: i_def complex_of_real_def complex_mult)
-
-lemma Im_mult_i_eq [simp]: "Im (ii * complex_of_real y) = y"
-by (simp add: i_def complex_of_real_def complex_mult)
-
-lemma complex_mod_mult_i [simp]: "cmod (ii * complex_of_real y) = abs y"
-by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square)
-
 lemma cos_arg_i_mult_zero_pos:
-   "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
+   "0 < y ==> cos (arg(Complex 0 y)) = 0"
 apply (simp add: arg_def abs_if)
 apply (rule_tac a = "pi/2" in someI2, auto)
 apply (rule order_less_trans [of _ 0], auto)
 done
 
 lemma cos_arg_i_mult_zero_neg:
-   "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
+   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
 apply (simp add: arg_def abs_if)
 apply (rule_tac a = "- pi/2" in someI2, auto)
 apply (rule order_trans [of _ 0], auto)
 done
 
 lemma cos_arg_i_mult_zero [simp]:
-     "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
-apply (insert linorder_less_linear [of y 0])
-apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
-done
+     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
+by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
 
 
 subsection{*Finally! Polar Form for Complex Numbers*}
 
 lemma complex_split_polar:
-     "\<exists>r a. z = complex_of_real r *
-      (complex_of_real(cos a) + ii * complex_of_real(sin a))"
-apply (cut_tac z = z in complex_split)
-apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
+     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
+apply (induct z) 
+apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
 done
 
 lemma rcis_Ex: "\<exists>r a. z = rcis r a"
-apply (simp add: rcis_def cis_def)
-apply (rule complex_split_polar)
+apply (induct z) 
+apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
 done
 
-lemma Re_complex_polar [simp]:
-     "Re(complex_of_real r *
-      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
-by (auto simp add: right_distrib complex_of_real_mult mult_ac)
-
 lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
 by (simp add: rcis_def cis_def)
 
-lemma Im_complex_polar [simp]:
-     "Im(complex_of_real r *
-         (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
-      r * sin a"
-by (auto simp add: right_distrib complex_of_real_mult mult_ac)
-
 lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
 by (simp add: rcis_def cis_def)
 
-lemma complex_mod_complex_polar [simp]:
-     "cmod (complex_of_real r *
-            (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
-      abs r"
-by (auto simp add: right_distrib cmod_i complex_of_real_mult
-                      right_distrib [symmetric] power_mult_distrib mult_ac
-         simp del: realpow_Suc)
+lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
+proof -
+  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
+    by (simp only: power_mult_distrib right_distrib) 
+  thus ?thesis by simp
+qed
 
 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
-by (simp add: rcis_def cis_def)
+by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
 
 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
 apply (simp add: cmod_def)
@@ -774,24 +745,6 @@
 lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
 by (induct z, simp add: complex_cnj complex_mult)
 
-lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
-by (induct z, induct w, simp add: complex_mult)
-
-lemma complex_Re_mult_complex_of_real [simp]:
-     "Re (z * complex_of_real c) = Re(z) * c"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Im_mult_complex_of_real [simp]:
-     "Im (z * complex_of_real c) = Im(z) * c"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Re_mult_complex_of_real2 [simp]:
-     "Re (complex_of_real c * z) = c * Re(z)"
-by (induct z, simp add: complex_of_real_def complex_mult)
-
-lemma complex_Im_mult_complex_of_real2 [simp]:
-     "Im (complex_of_real c * z) = c * Im(z)"
-by (induct z, simp add: complex_of_real_def complex_mult)
 
 (*---------------------------------------------------------------------------*)
 (*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
@@ -801,21 +754,13 @@
 by (simp add: rcis_def)
 
 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib
-                 mult_ac add_ac)
-apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2)
-apply (auto simp add: add_ac)
-apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac)
-done
+by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
 
 lemma cis_mult: "cis a * cis b = cis (a + b)"
 by (simp add: cis_rcis_eq rcis_mult)
 
 lemma cis_zero [simp]: "cis 0 = 1"
-by (simp add: cis_def)
-
-lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1"
-by (simp add: cis_def)
+by (simp add: cis_def complex_one_def)
 
 lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
 by (simp add: rcis_def)
@@ -825,8 +770,7 @@
 
 lemma complex_of_real_minus_one:
    "complex_of_real (-(1::real)) = -(1::complex)"
-apply (simp add: complex_of_real_def complex_one_def complex_minus)
-done
+by (simp add: complex_of_real_def complex_one_def complex_minus)
 
 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
 by (simp add: complex_mult_assoc [symmetric])
@@ -834,10 +778,7 @@
 
 lemma cis_real_of_nat_Suc_mult:
    "cis (real (Suc n) * a) = cis a * cis (real n * a)"
-apply (simp add: cis_def)
-apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add left_distrib right_distrib complex_of_real_add complex_of_real_mult mult_ac add_ac)
-apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2)
-done
+by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
 
 lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
 apply (induct_tac "n")
@@ -852,12 +793,7 @@
               complex_diff_def)
 
 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-apply (case_tac "r=0", simp)
-apply (auto simp add: complex_inverse_complex_split right_distrib
-            complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac)
-apply (auto simp add: right_distrib [symmetric] complex_of_real_minus 
-                      complex_diff_def)
-done
+by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
 
 lemma cis_divide: "cis a / cis b = cis (a - b)"
 by (simp add: complex_divide_def cis_mult real_diff_def)
@@ -880,35 +816,13 @@
 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
 by (auto simp add: DeMoivre)
 
-lemma expi_Im_split:
-    "expi (ii * complex_of_real y) =
-     complex_of_real (cos y) + ii * complex_of_real (sin y)"
-by (simp add: expi_def cis_def)
-
-lemma expi_Im_cis:
-    "expi (ii * complex_of_real y) = cis y"
-by (simp add: expi_def)
-
 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
 by (simp add: expi_def complex_Re_add exp_add complex_Im_add 
               cis_mult [symmetric] complex_of_real_mult mult_ac)
 
-lemma expi_complex_split:
-     "expi(complex_of_real x + ii * complex_of_real y) =
-      complex_of_real (exp(x)) * cis y"
-by (simp add: expi_def)
-
 lemma expi_zero [simp]: "expi (0::complex) = 1"
 by (simp add: expi_def)
 
-lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
-by (induct z, induct w, simp add: complex_mult)
-
-lemma complex_Im_mult_eq:
-     "Im (w * z) = Re w * Im z + Im w * Re z"
-apply (induct z, induct w, simp add: complex_mult)
-done
-
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])
 apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
@@ -1023,46 +937,22 @@
 val complexpow_minus = thm"complexpow_minus";
 val complex_mod_inverse = thm"complex_mod_inverse";
 val complex_mod_divide = thm"complex_mod_divide";
-val complex_inverse_divide = thm"complex_inverse_divide";
 val complexpow_i_squared = thm"complexpow_i_squared";
 val complex_i_not_zero = thm"complex_i_not_zero";
 val sgn_zero = thm"sgn_zero";
 val sgn_one = thm"sgn_one";
 val sgn_minus = thm"sgn_minus";
 val sgn_eq = thm"sgn_eq";
-val complex_split = thm"complex_split";
-val Re_complex_i = thm"Re_complex_i";
-val Im_complex_i = thm"Im_complex_i";
 val i_mult_eq = thm"i_mult_eq";
 val i_mult_eq2 = thm"i_mult_eq2";
-val cmod_i = thm"cmod_i";
-val complex_eq_Re_eq = thm"complex_eq_Re_eq";
-val complex_eq_Im_eq = thm"complex_eq_Im_eq";
-val complex_eq_cancel_iff = thm"complex_eq_cancel_iff";
-val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA";
-val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB";
-val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC";
-val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2";
-val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a";
-val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3";
-val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a";
-val complex_split_Re_zero = thm"complex_split_Re_zero";
-val complex_split_Im_zero = thm"complex_split_Im_zero";
 val Re_sgn = thm"Re_sgn";
 val Im_sgn = thm"Im_sgn";
 val complex_inverse_complex_split = thm"complex_inverse_complex_split";
-val Re_mult_i_eq = thm"Re_mult_i_eq";
-val Im_mult_i_eq = thm"Im_mult_i_eq";
-val complex_mod_mult_i = thm"complex_mod_mult_i";
 val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
 val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val complex_split_polar = thm"complex_split_polar";
 val rcis_Ex = thm"rcis_Ex";
-val Re_complex_polar = thm"Re_complex_polar";
 val Re_rcis = thm"Re_rcis";
-val Im_complex_polar = thm"Im_complex_polar";
 val Im_rcis = thm"Im_rcis";
-val complex_mod_complex_polar = thm"complex_mod_complex_polar";
 val complex_mod_rcis = thm"complex_mod_rcis";
 val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
 val complex_Re_cnj = thm"complex_Re_cnj";
@@ -1077,7 +967,6 @@
 val rcis_mult = thm"rcis_mult";
 val cis_mult = thm"cis_mult";
 val cis_zero = thm"cis_zero";
-val cis_zero2 = thm"cis_zero2";
 val rcis_zero_mod = thm"rcis_zero_mod";
 val rcis_zero_arg = thm"rcis_zero_arg";
 val complex_of_real_minus_one = thm"complex_of_real_minus_one";
@@ -1093,10 +982,7 @@
 val Im_cis = thm"Im_cis";
 val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
 val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
-val expi_Im_split = thm"expi_Im_split";
-val expi_Im_cis = thm"expi_Im_cis";
 val expi_add = thm"expi_add";
-val expi_complex_split = thm"expi_complex_split";
 val expi_zero = thm"expi_zero";
 val complex_Re_mult_eq = thm"complex_Re_mult_eq";
 val complex_Im_mult_eq = thm"complex_Im_mult_eq";
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/ComplexBin.ML
--- a/src/HOL/Complex/ComplexBin.ML	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/ComplexBin.ML	Thu Feb 05 10:45:28 2004 +0100
@@ -367,9 +367,9 @@
   val prove_conv      = Bin_Simprocs.prove_conv_nohyps_novars
   fun norm_tac simps  = ALLGOALS (simp_tac (HOL_ss addsimps simps))
   val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
-  end
+  end;
 
-structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData)
+structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData);
 
 (*For addition, we already have rules for the operand 0.
   Multiplication is omitted because there are already special rules for
@@ -386,7 +386,7 @@
      ComplexAbstractNumerals.proc diff_complex_number_of),
     ("complex_eq_eval_numerals",
      ["(m::complex) = 0", "(m::complex) = 1", "(m::complex) = number_of v"],
-     ComplexAbstractNumerals.proc eq_complex_number_of)]
+     ComplexAbstractNumerals.proc eq_complex_number_of)];
 
 end;
 
@@ -447,44 +447,7 @@
 Addsimps [complex_of_real_zero_iff];
 
 
-(*** Real and imaginary stuff ***)
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya = \
-\       number_of xb + ii * number_of yb) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff]));
-qed "complex_number_of_eq_cancel_iff";
-Addsimps [complex_number_of_eq_cancel_iff];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii = \
-\       number_of xb + number_of yb * ii) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffA]));
-qed "complex_number_of_eq_cancel_iffA";
-Addsimps [complex_number_of_eq_cancel_iffA];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii = \
-\       number_of xb + ii * number_of yb) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffB]));
-qed "complex_number_of_eq_cancel_iffB";
-Addsimps [complex_number_of_eq_cancel_iffB];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya = \
-\       number_of xb + number_of yb * ii) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffC]));
-qed "complex_number_of_eq_cancel_iffC";
-Addsimps [complex_number_of_eq_cancel_iffC];
-
+(*Convert???
 Goalw [complex_number_of_def] 
   "((number_of xa :: complex) + ii * number_of ya = \
 \       number_of xb) = \
@@ -524,6 +487,7 @@
     complex_of_real_zero_iff]));
 qed "complex_number_of_eq_cancel_iff3a";
 Addsimps [complex_number_of_eq_cancel_iff3a];
+*)
 
 Goalw [complex_number_of_def] "cnj (number_of v :: complex) = number_of v";
 by (rtac complex_cnj_complex_of_real 1);
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSCA.ML
--- a/src/HOL/Complex/NSCA.ML	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSCA.ML	Thu Feb 05 10:45:28 2004 +0100
@@ -943,11 +943,8 @@
 \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex";
 by (auto_tac (claset(),simpset() addsimps [SComplex_def,
     hcomplex_of_complex_def,SReal_def,hypreal_of_real_def]));
-by (res_inst_tac [("x","complex_of_real r + ii  * complex_of_real ra")] exI 1);
+by (res_inst_tac [("x","Complex r ra")] exI 1);
 by (Ultra_tac 1);
-by (case_tac "X x" 1);
-by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def,
-    complex_add,complex_mult]));
 qed "Reals_Re_Im_SComplex";
 
 Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \
@@ -987,8 +984,7 @@
 by (res_inst_tac [("z","t")] eq_Abs_hypreal 1);
 by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1);
 by Auto_tac;
-by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")]
-    exI 1);
+by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1);
 by Auto_tac;
 qed "stc_part_Ex";
 
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Thu Feb 05 10:45:28 2004 +0100
@@ -37,15 +37,15 @@
   hcomplex_diff_def:
   "w - z == w + -(z::hcomplex)"
 
+  hcinv_def:
+  "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P).
+                    hcomplexrel `` {%n. inverse(X n)})"
+
 constdefs
 
   hcomplex_of_complex :: "complex => hcomplex"
   "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})"
 
-  hcinv  :: "hcomplex => hcomplex"
-  "inverse(P)   == Abs_hcomplex(UN X: Rep_hcomplex(P).
-                    hcomplexrel `` {%n. inverse(X n)})"
-
   (*--- real and Imaginary parts ---*)
 
   hRe :: "hcomplex => hypreal"
@@ -99,6 +99,11 @@
   "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
 
 
+constdefs
+  HComplex :: "[hypreal,hypreal] => hcomplex"
+   "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"
+
+
 defs (overloaded)
 
   (*----------- division ----------*)
@@ -182,8 +187,7 @@
 apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
 done
 
-(*??delete*)
-lemma hcomplexrel_iff [iff]:
+lemma hcomplexrel_iff [simp]:
    "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
 by (simp add: hcomplexrel_def)
 
@@ -195,7 +199,7 @@
       Abs_hypreal(hyprel `` {%n. Re(X n)})"
 apply (simp add: hRe_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hIm:
@@ -203,17 +207,20 @@
       Abs_hypreal(hyprel `` {%n. Im(X n)})"
 apply (simp add: hIm_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_hRe_hIm_cancel_iff:
      "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
 apply (rule eq_Abs_hcomplex [of z])
 apply (rule eq_Abs_hcomplex [of w])
-apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
+apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff)
 apply (ultra+)
 done
 
+lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
+by (simp add: hcomplex_hRe_hIm_cancel_iff) 
+
 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
 by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
 
@@ -231,14 +238,15 @@
 
 lemma hcomplex_add_congruent2:
     "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
-by (auto simp add: congruent2_def, ultra)
+by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) 
 
 lemma hcomplex_add:
-  "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
-   Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
+  "Abs_hcomplex(hcomplexrel``{%n. X n}) + 
+   Abs_hcomplex(hcomplexrel``{%n. Y n}) =
+     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
 apply (simp add: hcomplex_add_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto simp add: iff: hcomplexrel_iff, ultra) 
 done
 
 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
@@ -286,7 +294,7 @@
       Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
 apply (simp add: hcomplex_minus_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
@@ -303,7 +311,7 @@
      Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
 apply (simp add: hcomplex_mult_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
@@ -350,7 +358,7 @@
       Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
 apply (simp add: hcinv_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_mult_inv_left:
@@ -428,6 +436,15 @@
 apply (simp add: minus_equation_iff [of x y])
 done
 
+lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
+by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
+
+lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z"
+by (simp add: mult_assoc [symmetric])
+
+lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
+by (simp add: iii_def hcomplex_zero_def)
+
 
 subsection{*More Multiplication Laws*}
 
@@ -469,7 +486,7 @@
   "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
       Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
 apply (simp add: hcomplex_of_hypreal_def)
-apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_of_hypreal_cancel_iff [iff]:
@@ -541,6 +558,34 @@
 by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
 
 
+subsection{*HComplex theorems*}
+
+lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
+done
+
+lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
+done
+
+text{*Relates the two nonstandard constructions*}
+lemma HComplex_eq_Abs_hcomplex_Complex:
+     "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
+      Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
+by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) 
+
+lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z"
+by (simp add: hcomplex_equality) 
+
+lemma hcomplex_induct [case_names rect, induct type: hcomplex]:
+     "(\<And>x y. P (HComplex x y)) ==> P z"
+by (rule hcomplex_surj [THEN subst], blast)
+
+
 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
 
 lemma hcmod:
@@ -549,12 +594,11 @@
 
 apply (simp add: hcmod_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcmod_zero [simp]: "hcmod(0) = 0"
-apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
-done
+by (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
 
 lemma hcmod_one [simp]: "hcmod(1) = 1"
 by (simp add: hcomplex_one_def hcmod hypreal_one_num)
@@ -569,6 +613,64 @@
       hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
 by simp
 
+lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')"
+apply (rule iffI) 
+ prefer 2 apply simp 
+apply (simp add: HComplex_def iii_def) 
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (rule eq_Abs_hypreal [of x'])
+apply (rule eq_Abs_hypreal [of y'])
+apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
+apply (ultra+) 
+done
+
+lemma HComplex_add [simp]:
+     "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
+by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib) 
+
+lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
+by (simp add: HComplex_def hcomplex_of_hypreal_minus) 
+
+lemma HComplex_diff [simp]:
+     "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
+by (simp add: diff_minus)
+
+lemma HComplex_mult [simp]:
+  "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
+by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus 
+       hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
+       add_ac mult_ac right_distrib)
+
+(*HComplex_inverse is proved below*)
+
+lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0"
+by (simp add: HComplex_def)
+
+lemma HComplex_add_hcomplex_of_hypreal [simp]:
+     "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
+by (simp add: hcomplex_of_hypreal_eq)
+
+lemma hcomplex_of_hypreal_add_HComplex [simp]:
+     "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
+by (simp add: i_def hcomplex_of_hypreal_eq)
+
+lemma HComplex_mult_hcomplex_of_hypreal:
+     "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
+by (simp add: hcomplex_of_hypreal_eq)
+
+lemma hcomplex_of_hypreal_mult_HComplex:
+     "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
+by (simp add: i_def hcomplex_of_hypreal_eq)
+
+lemma i_hcomplex_of_hypreal [simp]:
+     "iii * hcomplex_of_hypreal r = HComplex 0 r"
+by (simp add: HComplex_def)
+
+lemma hcomplex_of_hypreal_i [simp]:
+     "hcomplex_of_hypreal r * iii = HComplex 0 r"
+by (simp add: mult_commute) 
+
 
 subsection{*Conjugation*}
 
@@ -577,7 +679,7 @@
    Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
 apply (simp add: hcnj_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
@@ -777,7 +879,7 @@
    Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
 apply (simp add: hcpow_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcomplex_of_hypreal_hyperpow:
@@ -817,6 +919,9 @@
   show "z^(Suc n) = z * (z^n)" by simp
 qed
 
+lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
+by (simp add: power2_eq_square)
+
 
 lemma hcomplex_of_hypreal_pow:
      "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
@@ -872,15 +977,6 @@
 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
 by (blast intro: ccontr dest: hcpow_not_zero)
 
-lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
-by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
-
-lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
-by (simp add: numeral_2_eq_2)
-
-lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
-by (simp add: iii_def hcomplex_zero_def)
-
 lemma hcomplex_divide:
   "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
    Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
@@ -888,6 +984,7 @@
 
 
 
+
 subsection{*The Function @{term hsgn}*}
 
 lemma hsgn:
@@ -895,7 +992,7 @@
       Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
 apply (simp add: hsgn_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hsgn_zero [simp]: "hsgn 0 = 0"
@@ -914,144 +1011,33 @@
 apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
 done
 
-lemma lemma_hypreal_P_EX2:
-     "(\<exists>(x::hypreal) y. P x y) =
-      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
-apply auto
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal, auto)
-done
 
-lemma complex_split2:
-     "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
-by (blast intro: complex_split)
-
-(* Interesting proof! *)
-lemma hcomplex_split:
-     "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
-apply (rule eq_Abs_hcomplex [of z])
-apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
-apply (cut_tac z = x in complex_split2)
-apply (drule choice, safe)+
-apply (rule_tac x = f in exI)
-apply (rule_tac x = fa in exI, auto)
-done
-
-lemma hRe_hcomplex_i [simp]:
-     "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
-done
-
-lemma hIm_hcomplex_i [simp]:
-     "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
+lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
 apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
-done
-
-lemma hcmod_i:
-     "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
-      ( *f* sqrt) (x ^ 2 + y ^ 2)"
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
-done
-
-lemma hcomplex_eq_hRe_eq:
-     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
-      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
-       ==> xa = xb"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of xa])
-apply (rule eq_Abs_hypreal [of ya])
-apply (rule eq_Abs_hypreal [of xb])
-apply (rule eq_Abs_hypreal [of yb])
-apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
-done
-
-lemma hcomplex_eq_hIm_eq:
-     "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
-      hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
-       ==> ya = yb"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of xa])
-apply (rule eq_Abs_hypreal [of ya])
-apply (rule eq_Abs_hypreal [of xb])
-apply (rule eq_Abs_hypreal [of yb])
-apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
+apply (rule eq_Abs_hypreal [of y]) 
+apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun 
+                 hypreal_mult hypreal_add hcmod numeral_2_eq_2)
 done
 
-lemma hcomplex_eq_cancel_iff [simp]:
-     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
-       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
-      ((xa = xb) & (ya = yb))"
-by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
-
-lemma hcomplex_eq_cancel_iffA [iff]:
-     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
-       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iffB [iff]:
-     "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
-       hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iffC [iff]:
-     "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
-       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
-apply (simp add: hcomplex_mult_commute)
-done
+lemma hcomplex_eq_cancel_iff1 [simp]:
+     "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
+by (simp add: hcomplex_of_hypreal_eq)
 
 lemma hcomplex_eq_cancel_iff2 [simp]:
-     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
-      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
-apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff)
-apply (simp del: hcomplex_eq_cancel_iff)
-done
+     "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
+by (simp add: hcomplex_of_hypreal_eq)
 
-lemma hcomplex_eq_cancel_iff2a [simp]:
-     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
-      hcomplex_of_hypreal xa) = (x = xa & y = 0)"
-apply (simp add: hcomplex_mult_commute)
-done
-
-lemma hcomplex_eq_cancel_iff3 [simp]:
-     "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
-      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
-apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff)
-apply (simp del: hcomplex_eq_cancel_iff)
-done
+lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)"
+by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp)
 
-lemma hcomplex_eq_cancel_iff3a [simp]:
-     "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
-      iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
-apply (simp add: hcomplex_mult_commute)
-done
+lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)"
+by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp)
 
-lemma hcomplex_split_hRe_zero:
-     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
-      ==> x = 0"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
-apply (simp add: complex_split_Re_zero)
-done
+lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
+by (insert hcomplex_of_hypreal_i [of 1], simp)
 
-lemma hcomplex_split_hIm_zero:
-     "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
-      ==> y = 0"
-apply (simp add: iii_def)
-apply (rule eq_Abs_hypreal [of x])
-apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
-apply (simp add: complex_split_Im_zero)
-done
+lemma HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)"
+by (simp add: i_eq_HComplex_0_1) 
 
 lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
 apply (rule eq_Abs_hcomplex [of z])
@@ -1064,8 +1050,7 @@
 done
 
 lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
-apply (auto intro: real_sum_squares_cancel)
-done
+by (auto intro: real_sum_squares_cancel)
 
 lemma hcomplex_inverse_complex_split:
      "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
@@ -1074,8 +1059,16 @@
 apply (rule eq_Abs_hypreal [of x])
 apply (rule eq_Abs_hypreal [of y])
 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)
+apply (simp add: diff_minus) 
 done
 
+lemma HComplex_inverse:
+     "inverse (HComplex x y) =
+      HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
+by (simp only: HComplex_def hcomplex_inverse_complex_split, simp)
+
+
+
 lemma hRe_mult_i_eq[simp]:
     "hRe (iii * hcomplex_of_hypreal y) = 0"
 apply (simp add: iii_def)
@@ -1096,7 +1089,7 @@
 done
 
 lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
-by (simp add: hcomplex_mult_commute)
+by (simp only: hcmod_mult_i hcomplex_mult_commute)
 
 (*---------------------------------------------------------------------------*)
 (*  harg                                                                     *)
@@ -1105,31 +1098,29 @@
 lemma harg:
   "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
       Abs_hypreal(hyprel `` {%n. arg (X n)})"
-
 apply (simp add: harg_def)
 apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto, ultra)
+apply (auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma cos_harg_i_mult_zero_pos:
-     "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
+     "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
 apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
-                hypreal_zero_num hypreal_less starfun harg, ultra)
+apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
+                hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
 
 lemma cos_harg_i_mult_zero_neg:
-     "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
+     "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
 apply (rule eq_Abs_hypreal [of y])
-apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
-                      hypreal_zero_num hypreal_less starfun harg, ultra)
+apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
+                 hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
 done
 
 lemma cos_harg_i_mult_zero [simp]:
-     "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
-apply (cut_tac x = y and y = 0 in linorder_less_linear)
-apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
-done
+     "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
+by (auto simp add: linorder_neq_iff
+                   cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
 
 lemma hcomplex_of_hypreal_zero_iff [simp]:
      "(hcomplex_of_hypreal y = 0) = (y = 0)"
@@ -1141,16 +1132,21 @@
 subsection{*Polar Form for Nonstandard Complex Numbers*}
 
 lemma complex_split_polar2:
-     "\<forall>n. \<exists>r a. (z n) = complex_of_real r *
-      (complex_of_real(cos a) + ii * complex_of_real(sin a))"
-apply (blast intro: complex_split_polar)
+     "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
+by (blast intro: complex_split_polar)
+
+lemma lemma_hypreal_P_EX2:
+     "(\<exists>(x::hypreal) y. P x y) =
+      (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
+apply auto
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal, auto)
 done
 
 lemma hcomplex_split_polar:
-  "\<exists>r a. z = hcomplex_of_hypreal r *
-   (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
+  "\<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
 apply (rule eq_Abs_hcomplex [of z])
-apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
+apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def)
 apply (cut_tac z = x in complex_split_polar2)
 apply (drule choice, safe)+
 apply (rule_tac x = f in exI)
@@ -1161,7 +1157,7 @@
   "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
       Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
 apply (simp add: hcis_def)
-apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
 done
 
 lemma hcis_eq:
@@ -1178,35 +1174,38 @@
 by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
 
 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
-apply (simp add: hrcis_def hcis_eq)
+apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric])
 apply (rule hcomplex_split_polar)
 done
 
 lemma hRe_hcomplex_polar [simp]:
-     "hRe(hcomplex_of_hypreal r *
-      (hcomplex_of_hypreal(( *f* cos) a) +
-       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
-by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
+     "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
+      r * ( *f* cos) a"
+by (simp add: hcomplex_of_hypreal_mult_HComplex)
 
 lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
 by (simp add: hrcis_def hcis_eq)
 
 lemma hIm_hcomplex_polar [simp]:
-     "hIm(hcomplex_of_hypreal r *
-      (hcomplex_of_hypreal(( *f* cos) a) +
-       iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
-by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
+     "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
+      r * ( *f* sin) a"
+by (simp add: hcomplex_of_hypreal_mult_HComplex)
 
 lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
 by (simp add: hrcis_def hcis_eq)
 
+
+lemma hcmod_unit_one [simp]:
+     "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
+apply (rule eq_Abs_hypreal [of a]) 
+apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal 
+                 hcomplex_mult hcmod hcomplex_add hypreal_one_def)
+done
+
 lemma hcmod_complex_polar [simp]:
-     "hcmod (hcomplex_of_hypreal r *
-      (hcomplex_of_hypreal(( *f* cos) a) +
-       iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
-apply (rule eq_Abs_hypreal [of r])
-apply (rule eq_Abs_hypreal [of a])
-apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
+     "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
+      abs r"
+apply (simp only: hcmod_mult hcmod_unit_one, simp)  
 done
 
 lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
@@ -1316,20 +1315,16 @@
 done
 
 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
-apply (simp add: NSDeMoivre)
-done
+by (simp add: NSDeMoivre)
 
 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
-apply (simp add: NSDeMoivre)
-done
+by (simp add: NSDeMoivre)
 
 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
-apply (simp add: NSDeMoivre_ext)
-done
+by (simp add: NSDeMoivre_ext)
 
 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
-apply (simp add: NSDeMoivre_ext)
-done
+by (simp add: NSDeMoivre_ext)
 
 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
 apply (simp add: hexpi_def)
@@ -1545,27 +1540,11 @@
 val hsgn_minus = thm"hsgn_minus";
 val hsgn_eq = thm"hsgn_eq";
 val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
-val complex_split2 = thm"complex_split2";
-val hcomplex_split = thm"hcomplex_split";
-val hRe_hcomplex_i = thm"hRe_hcomplex_i";
-val hIm_hcomplex_i = thm"hIm_hcomplex_i";
 val hcmod_i = thm"hcmod_i";
-val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq";
-val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq";
-val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff";
-val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA";
-val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB";
-val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC";
 val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
-val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a";
-val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3";
-val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a";
-val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero";
-val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero";
 val hRe_hsgn = thm"hRe_hsgn";
 val hIm_hsgn = thm"hIm_hsgn";
 val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
-val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split";
 val hRe_mult_i_eq = thm"hRe_mult_i_eq";
 val hIm_mult_i_eq = thm"hIm_mult_i_eq";
 val hcmod_mult_i = thm"hcmod_mult_i";
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSComplexBin.ML
--- a/src/HOL/Complex/NSComplexBin.ML	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Complex/NSComplexBin.ML	Thu Feb 05 10:45:28 2004 +0100
@@ -482,6 +482,7 @@
 
 (*** Real and imaginary stuff ***)
 
+(*Convert???
 Goalw [hcomplex_number_of_def] 
   "((number_of xa :: hcomplex) + iii * number_of ya = \
 \       number_of xb + iii * number_of yb) = \
@@ -561,6 +562,7 @@
     hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff]));
 qed "hcomplex_number_of_eq_cancel_iff3a";
 Addsimps [hcomplex_number_of_eq_cancel_iff3a];
+*)
 
 Goalw [hcomplex_number_of_def] "hcnj (number_of v :: hcomplex) = number_of v";
 by (rtac (hcomplex_hypreal_number_of RS ssubst) 1);
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Real/PReal.thy	Thu Feb 05 10:45:28 2004 +0100
@@ -386,17 +386,18 @@
   proof (intro exI conjI)
     show "0 < x*y" by (simp add: mult_pos)
     show "x * y \<notin> mult_set A B"
-    proof (auto simp add: mult_set_def)
-      fix u::rat and v::rat
-      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
-      moreover
-      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
-      moreover
-      with prems have "0\<le>v"
-        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
-      moreover
-      hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
-      ultimately show False by force
+    proof -
+      { fix u::rat and v::rat
+	assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
+	moreover
+	with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
+	moreover
+	with prems have "0\<le>v"
+	  by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
+	moreover
+	hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
+	ultimately have False by force}
+      thus ?thesis by (auto simp add: mult_set_def)
     qed
   qed
 qed
@@ -646,14 +647,15 @@
   proof (intro exI conjI)
     show "0 < inverse x" by simp
     show "inverse x \<notin> inverse_set A"
-    proof (auto simp add: inverse_set_def)
-      fix y::rat 
-      assume ygt: "inverse x < y"
-      have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
-      have iyless: "inverse y < x" 
-        by (simp add: inverse_less_imp_less [of x] ygt)
-      show "inverse y \<in> A"
-        by (simp add: preal_downwards_closed [OF A x] iyless) 
+    proof -
+      { fix y::rat 
+	assume ygt: "inverse x < y"
+	have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
+	have iyless: "inverse y < x" 
+	  by (simp add: inverse_less_imp_less [of x] ygt)
+	have "inverse y \<in> A"
+	  by (simp add: preal_downwards_closed [OF A x] iyless)}
+     thus ?thesis by (auto simp add: inverse_set_def)
     qed
   qed
 qed
diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Feb 05 04:30:38 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Feb 05 10:45:28 2004 +0100
@@ -94,10 +94,10 @@
   by (simp add: add_commute)
 
 lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
-  proof (rule add_left_cancel [of "-a", THEN iffD1])
-    show "(-a + -(-a) = -a + a)"
-    by simp
-  qed
+proof (rule add_left_cancel [of "-a", THEN iffD1])
+  show "(-a + -(-a) = -a + a)"
+  by simp
+qed
 
 lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
 apply (rule right_minus_eq [THEN iffD1, symmetric])
@@ -120,15 +120,15 @@
 by (simp add: diff_minus)
 
 lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
-  proof 
-    assume "- a = - b"
-    hence "- (- a) = - (- b)"
-      by simp
-    thus "a=b" by simp
-  next
-    assume "a=b"
-    thus "-a = -b" by simp
-  qed
+proof 
+  assume "- a = - b"
+  hence "- (- a) = - (- b)"
+    by simp
+  thus "a=b" by simp
+next
+  assume "a=b"
+  thus "-a = -b" by simp
+qed
 
 lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
 by (subst neg_equal_iff_equal [symmetric], simp)
@@ -139,16 +139,16 @@
 text{*The next two equations can make the simplifier loop!*}
 
 lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
-  proof -
+proof -
   have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   thus ?thesis by (simp add: eq_commute)
-  qed
+qed
 
 lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
-  proof -
+proof -
   have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   thus ?thesis by (simp add: eq_commute)
-  qed
+qed
 
 
 subsection {* Derived rules for multiplication *}
@@ -263,13 +263,13 @@
 
 lemma add_less_imp_less_left:
       assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
-  proof (rule ccontr)
-    assume "~ a < b"
-    hence "b \<le> a" by (simp add: linorder_not_less)
-    hence "c+b \<le> c+a" by (rule add_left_mono)
-    with this and less show False 
-      by (simp add: linorder_not_less [symmetric])
-  qed
+proof (rule ccontr)
+  assume "~ a < b"
+  hence "b \<le> a" by (simp add: linorder_not_less)
+  hence "c+b \<le> c+a" by (rule add_left_mono)
+  with this and less show False 
+    by (simp add: linorder_not_less [symmetric])
+qed
 
 lemma add_less_imp_less_right:
       "a + c < b + c ==> a < (b::'a::ordered_semiring)"
@@ -306,7 +306,7 @@
 
 lemma le_imp_neg_le:
       assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
-  proof -
+proof -
   have "-a+a \<le> -a+b"
     by (rule add_left_mono) 
   hence "0 \<le> -a+b"
@@ -315,18 +315,18 @@
     by (rule add_right_mono) 
   thus ?thesis
     by (simp add: add_assoc)
-  qed
+qed
 
 lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
-  proof 
-    assume "- b \<le> - a"
-    hence "- (- a) \<le> - (- b)"
-      by (rule le_imp_neg_le)
-    thus "a\<le>b" by simp
-  next
-    assume "a\<le>b"
-    thus "-b \<le> -a" by (rule le_imp_neg_le)
-  qed
+proof 
+  assume "- b \<le> - a"
+  hence "- (- a) \<le> - (- b)"
+    by (rule le_imp_neg_le)
+  thus "a\<le>b" by simp
+next
+  assume "a\<le>b"
+  thus "-b \<le> -a" by (rule le_imp_neg_le)
+qed
 
 lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
 by (subst neg_le_iff_le [symmetric], simp)
@@ -346,16 +346,16 @@
 text{*The next several equations can make the simplifier loop!*}
 
 lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"
-  proof -
+proof -
   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   thus ?thesis by simp
-  qed
+qed
 
 lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"
-  proof -
+proof -
   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   thus ?thesis by simp
-  qed
+qed
 
 lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
 apply (simp add: linorder_not_less [symmetric])
@@ -645,13 +645,13 @@
 lemma mult_less_imp_less_left:
       assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
       shows "a < (b::'a::ordered_semiring)"
-  proof (rule ccontr)
-    assume "~ a < b"
-    hence "b \<le> a" by (simp add: linorder_not_less)
-    hence "c*b \<le> c*a" by (rule mult_left_mono)
-    with this and less show False 
-      by (simp add: linorder_not_less [symmetric])
-  qed
+proof (rule ccontr)
+  assume "~ a < b"
+  hence "b \<le> a" by (simp add: linorder_not_less)
+  hence "c*b \<le> c*a" by (rule mult_left_mono)
+  with this and less show False 
+    by (simp add: linorder_not_less [symmetric])
+qed
 
 lemma mult_less_imp_less_right:
     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
@@ -723,52 +723,50 @@
 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
       of an ordering.*}
 lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
-  proof cases
-    assume "a=0" thus ?thesis by simp
-  next
-    assume anz [simp]: "a\<noteq>0"
-    thus ?thesis
-    proof auto
-      assume "a * b = 0"
-      hence "inverse a * (a * b) = 0" by simp
-      thus "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])
-    qed
-  qed
+proof cases
+  assume "a=0" thus ?thesis by simp
+next
+  assume anz [simp]: "a\<noteq>0"
+  { assume "a * b = 0"
+    hence "inverse a * (a * b) = 0" by simp
+    hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}
+  thus ?thesis by force
+qed
 
 text{*Cancellation of equalities with a common factor*}
 lemma field_mult_cancel_right_lemma:
       assumes cnz: "c \<noteq> (0::'a::field)"
 	  and eq:  "a*c = b*c"
 	 shows "a=b"
-  proof -
+proof -
   have "(a * c) * inverse c = (b * c) * inverse c"
     by (simp add: eq)
   thus "a=b"
     by (simp add: mult_assoc cnz)
-  qed
+qed
 
 lemma field_mult_cancel_right [simp]:
      "(a*c = b*c) = (c = (0::'a::field) | a=b)"
-  proof cases
-    assume "c=0" thus ?thesis by simp
-  next
-    assume "c\<noteq>0" 
-    thus ?thesis by (force dest: field_mult_cancel_right_lemma)
-  qed
+proof cases
+  assume "c=0" thus ?thesis by simp
+next
+  assume "c\<noteq>0" 
+  thus ?thesis by (force dest: field_mult_cancel_right_lemma)
+qed
 
 lemma field_mult_cancel_left [simp]:
      "(c*a = c*b) = (c = (0::'a::field) | a=b)"
   by (simp add: mult_commute [of c] field_mult_cancel_right) 
 
 lemma nonzero_imp_inverse_nonzero: "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::field)"
-  proof
+proof
   assume ianz: "inverse a = 0"
   assume "a \<noteq> 0"
   hence "1 = a * inverse a" by simp
   also have "... = 0" by (simp add: ianz)
   finally have "1 = (0::'a::field)" .
   thus False by (simp add: eq_commute)
-  qed
+qed
 
 
 subsection{*Basic Properties of @{term inverse}*}
@@ -790,35 +788,35 @@
 
 lemma nonzero_inverse_minus_eq:
       assumes [simp]: "a\<noteq>0"  shows "inverse(-a) = -inverse(a::'a::field)"
-  proof -
-    have "-a * inverse (- a) = -a * - inverse a"
-      by simp
-    thus ?thesis 
-      by (simp only: field_mult_cancel_left, simp)
-  qed
+proof -
+  have "-a * inverse (- a) = -a * - inverse a"
+    by simp
+  thus ?thesis 
+    by (simp only: field_mult_cancel_left, simp)
+qed
 
 lemma inverse_minus_eq [simp]:
-     "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
-  proof cases
-    assume "a=0" thus ?thesis by (simp add: inverse_zero)
-  next
-    assume "a\<noteq>0" 
-    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
-  qed
+   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
+proof cases
+  assume "a=0" thus ?thesis by (simp add: inverse_zero)
+next
+  assume "a\<noteq>0" 
+  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
 
 lemma nonzero_inverse_eq_imp_eq:
       assumes inveq: "inverse a = inverse b"
 	  and anz:  "a \<noteq> 0"
 	  and bnz:  "b \<noteq> 0"
 	 shows "a = (b::'a::field)"
-  proof -
+proof -
   have "a * inverse b = a * inverse a"
     by (simp add: inveq)
   hence "(a * inverse b) * b = (a * inverse a) * b"
     by simp
   thus "a = b"
     by (simp add: mult_assoc anz bnz)
-  qed
+qed
 
 lemma inverse_eq_imp_eq:
      "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"