# HG changeset patch
# User paulson
# Date 1073986672 -3600
# Node ID 988aa464859722e060241ef33c57e7a61ee999fd
# Parent  79f9fbef910679f43851d514d6146d6de0b15cd2
types complex and hcomplex are now instances of class ringpower:
omitting redundant lemmas

diff -r 79f9fbef9106 -r 988aa4648597 src/HOL/Complex/CLim.ML
--- a/src/HOL/Complex/CLim.ML	Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/CLim.ML	Tue Jan 13 10:37:52 2004 +0100
@@ -1097,7 +1097,7 @@
 \     ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
 by (rtac (complex_mult_commute RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [complex_minus_mult_eq1,
-    complexpow_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
+    power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym,
 complex_minus_mult_eq1 RS sym]) 1);
 by (fold_goals_tac [o_def]);
 by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1);
@@ -1127,7 +1127,7 @@
 by (REPEAT(assume_tac 1));
 by (asm_full_simp_tac
     (simpset() addsimps [complex_divide_def, complex_add_mult_distrib2,
-                         complexpow_inverse,complex_minus_mult_eq1] @ complex_mult_ac 
+                         power_inverse,complex_minus_mult_eq1] @ complex_mult_ac 
        delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
 qed "CDERIV_quotient";
 
diff -r 79f9fbef9106 -r 988aa4648597 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Tue Jan 13 10:37:52 2004 +0100
@@ -51,7 +51,7 @@
   "sgn z == z / complex_of_real(cmod z)"
 
   arg :: "complex => real"
-  "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a <= pi"
+  "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
 
 
 defs (overloaded)
@@ -94,11 +94,6 @@
   "w / (z::complex) == w * inverse z"
 
 
-primrec
-     complexpow_0:   "z ^ 0       = complex_of_real 1"
-     complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
-
-
 constdefs
 
   (* abbreviation for (cos a + i sin a) *)
@@ -280,7 +275,7 @@
 by (auto dest: sym)
 declare complex_minus_zero_iff2 [simp]
 
-lemma complex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::complex))"
+lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))"
 by auto
 
 
@@ -494,7 +489,7 @@
 apply (simp (no_asm) add: complex_mult_commute)
 done
 
-lemma complex_zero_not_eq_one: "(0::complex) ~= 1"
+lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1"
 apply (unfold complex_zero_def complex_one_def)
 apply (simp (no_asm) add: complex_Re_Im_cancel_iff)
 done
@@ -504,8 +499,9 @@
 
 subsection{*Inverse*}
 
-lemma complex_inverse: "inverse (Abs_complex(x,y)) =
-     Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
+lemma complex_inverse:
+     "inverse (Abs_complex(x,y)) =
+      Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
 apply (unfold complex_inverse_def)
 apply (simp (no_asm))
 done
@@ -524,7 +520,7 @@
   show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 
 qed
 
-lemma complex_mult_inv_left: "z ~= (0::complex) ==> inverse(z) * z = 1"
+lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
 apply (rule_tac z = z in eq_Abs_complex)
 apply (auto simp add: complex_mult complex_inverse complex_one_def 
        complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
@@ -533,7 +529,7 @@
 done
 declare complex_mult_inv_left [simp]
 
-lemma complex_mult_inv_right: "z ~= (0::complex) ==> z * inverse(z) = 1"
+lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1"
 by (auto intro: complex_mult_commute [THEN subst])
 declare complex_mult_inv_right [simp]
 
@@ -641,11 +637,6 @@
 apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
 done
 
-lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_of_real_mult [symmetric])
-done
-
 lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)"
 apply (unfold cmod_def)
 apply (simp (no_asm))
@@ -744,11 +735,6 @@
 done
 declare complex_cnj_one [simp]
 
-lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_cnj_mult)
-done
-
 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
 apply (rule_tac z = z in eq_Abs_complex)
 apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def)
@@ -756,12 +742,12 @@
 
 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
 apply (rule_tac z = z in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def complex_diff_def complex_minus i_def complex_mult)
+apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def 
+                 complex_minus i_def complex_mult)
 done
 
-lemma complex_cnj_zero: "cnj 0 = 0"
+lemma complex_cnj_zero [simp]: "cnj 0 = 0"
 by (simp add: cnj_def complex_zero_def)
-declare complex_cnj_zero [simp]
 
 lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"
 apply (rule_tac z = z in eq_Abs_complex)
@@ -826,7 +812,7 @@
 lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
 by (unfold cmod_def, auto)
 
-lemma complex_mod_ge_zero: "0 <= cmod x"
+lemma complex_mod_ge_zero: "0 \<le> cmod x"
 apply (unfold cmod_def)
 apply (auto intro: real_sqrt_ge_zero)
 done
@@ -852,14 +838,14 @@
 apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
 done
 
-lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) <= cmod(x * cnj y)"
+lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"
 apply (rule_tac z = x in eq_Abs_complex)
 apply (rule_tac z = y in eq_Abs_complex)
 apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
 done
 declare complex_Re_mult_cnj_le_cmod [simp]
 
-lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) <= cmod(x * y)"
+lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"
 apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod)
 apply (simp add: complex_mod_mult)
 done
@@ -869,25 +855,25 @@
 apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
 done
 
-lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 <= (cmod(x) + cmod(y)) ^ 2"
+lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
 apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
 done
 declare complex_mod_triangle_squared [simp]
 
-lemma complex_mod_minus_le_complex_mod: "- cmod x <= cmod x"
+lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
 apply (rule order_trans [OF _ complex_mod_ge_zero]) 
 apply (simp (no_asm))
 done
 declare complex_mod_minus_le_complex_mod [simp]
 
-lemma complex_mod_triangle_ineq: "cmod (x + y) <= cmod(x) + cmod(y)"
+lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"
 apply (rule_tac n = 1 in realpow_increasing)
 apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
             simp add: power2_eq_square [symmetric])
 done
 declare complex_mod_triangle_ineq [simp]
 
-lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b <= cmod a"
+lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
 apply (cut_tac x1 = b and y1 = a and c = "-cmod b" 
        in complex_mod_triangle_ineq [THEN add_right_mono])
 apply (simp (no_asm))
@@ -906,7 +892,7 @@
 lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
 by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)
 
-lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) <= cmod(a + b)"
+lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)"
 apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])
 apply auto
 apply (rule order_trans [of _ 0], rule order_less_imp_le)
@@ -919,13 +905,13 @@
 done
 declare complex_mod_diff_ineq [simp]
 
-lemma complex_Re_le_cmod: "Re z <= cmod z"
+lemma complex_Re_le_cmod: "Re z \<le> cmod z"
 apply (rule_tac z = z in eq_Abs_complex)
 apply (auto simp add: complex_mod simp del: realpow_Suc)
 done
 declare complex_Re_le_cmod [simp]
 
-lemma complex_mod_gt_zero: "z ~= 0 ==> 0 < cmod z"
+lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
 apply (cut_tac x = z in complex_mod_ge_zero)
 apply (drule order_le_imp_less_or_eq, auto)
 done
@@ -933,25 +919,6 @@
 
 subsection{*A Few More Theorems*}
 
-lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: complex_mod_mult)
-done
-
-lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-by (induct_tac "n", auto)
-
-lemma complex_inverse_minus: "inverse (-x) = - inverse (x::complex)"
-apply (rule_tac z = x in eq_Abs_complex)
-apply (simp (no_asm_simp) add: complex_inverse complex_minus power2_eq_square)
-done
-
-lemma complex_divide_one: "x / (1::complex) = x"
-apply (unfold complex_divide_def)
-apply (simp (no_asm))
-done
-declare complex_divide_one [simp]
-
 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"
 apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO)
 apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])
@@ -971,59 +938,51 @@
 done
 declare complex_inverse_divide [simp]
 
-lemma complexpow_mult: "((r::complex) * s) ^ n = (r ^ n) * (s ^ n)"
-apply (induct_tac "n")
-apply (auto simp add: complex_mult_ac)
-done
+
+subsection{*Exponentiation*}
+
+primrec
+     complexpow_0:   "z ^ 0       = 1"
+     complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
+
+
+instance complex :: ringpower
+proof
+  fix z :: complex
+  fix n :: nat
+  show "z^0 = 1" by simp
+  show "z^(Suc n) = z * (z^n)" by simp
+qed
 
 
-subsection{*More Exponentiation*}
-
-lemma complexpow_zero: "(0::complex) ^ (Suc n) = 0"
-by auto
-declare complexpow_zero [simp]
-
-lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0"
+lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
 apply (induct_tac "n")
-apply (auto simp add: )
-done
-declare complexpow_not_zero [simp]
-declare complexpow_not_zero [intro]
-
-lemma complexpow_zero_zero: "r ^ n = (0::complex) ==> r = 0"
-by (blast intro: ccontr dest: complexpow_not_zero)
-
-lemma complexpow_i_squared: "ii ^ 2 = -(1::complex)"
-apply (unfold i_def)
-apply (auto simp add: complex_mult complex_one_def complex_minus numeral_2_eq_2)
+apply (auto simp add: complex_of_real_mult [symmetric])
 done
-declare complexpow_i_squared [simp]
 
-lemma complex_i_not_zero: "ii ~= 0"
-by (unfold i_def complex_zero_def, auto)
-declare complex_i_not_zero [simp]
-
-lemma complex_mult_eq_zero_cancel1: "x * y ~= (0::complex) ==> x ~= 0"
-by auto
-
-lemma complex_mult_eq_zero_cancel2: "x * y ~= 0 ==> y ~= (0::complex)"
-by auto
-
-lemma complex_mult_not_eq_zero_iff: "(x * y ~= 0) = (x ~= 0 & y ~= (0::complex))"
-by auto
-declare complex_mult_not_eq_zero_iff [iff]
-
-lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n"
+lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
 apply (induct_tac "n")
-apply (auto simp add: inverse_mult_distrib)
+apply (auto simp add: complex_cnj_mult)
 done
 
-(*---------------------------------------------------------------------------*)
-(* sgn                                                                       *)
-(*---------------------------------------------------------------------------*)
+lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: complex_mod_mult)
+done
+
+lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
+by (induct_tac "n", auto)
+
+lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
+by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
+
+lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
+by (unfold i_def complex_zero_def, auto)
+
+
+subsection{*The Function @{term sgn}*}
 
 lemma sgn_zero: "sgn 0 = 0"
-
 apply (unfold sgn_def)
 apply (simp (no_asm))
 done
@@ -1044,7 +1003,7 @@
 apply (simp (no_asm))
 done
 
-lemma complex_split: "EX x y. z = complex_of_real(x) + ii * complex_of_real(y)"
+lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
 apply (rule_tac z = z in eq_Abs_complex)
 apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
 done
@@ -1184,6 +1143,9 @@
 (* many of the theorems are not used - so should they be kept?                *)
 (*----------------------------------------------------------------------------*)
 
+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:
     "Re (ii * complex_of_real y) = 0"
 apply (unfold i_def complex_of_real_def)
@@ -1205,50 +1167,37 @@
 done
 declare complex_mod_mult_i [simp]
 
-lemma cos_arg_i_mult_zero:
+lemma cos_arg_i_mult_zero_pos:
    "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
 apply (unfold arg_def)
 apply (auto simp add: abs_eqI2)
 apply (rule_tac a = "pi/2" in someI2, auto)
 apply (rule order_less_trans [of _ 0], auto)
 done
-declare cos_arg_i_mult_zero [simp]
 
-lemma cos_arg_i_mult_zero2:
+lemma cos_arg_i_mult_zero_neg:
    "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
 apply (unfold arg_def)
 apply (auto simp add: abs_minus_eqI2)
 apply (rule_tac a = "- pi/2" in someI2, auto)
 apply (rule order_trans [of _ 0], auto)
 done
-declare cos_arg_i_mult_zero2 [simp]
 
-lemma complex_of_real_not_zero_iff:
-      "(complex_of_real y ~= 0) = (y ~= 0)"
-apply (unfold complex_zero_def complex_of_real_def, auto)
-done
-declare complex_of_real_not_zero_iff [simp]
-
-lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)"
-apply auto
-apply (rule ccontr, drule complex_of_real_not_zero_iff [THEN iffD2], simp)
-done
-declare complex_of_real_zero_iff [simp]
-
-lemma cos_arg_i_mult_zero3: "y ~= 0 ==> cos (arg(ii * complex_of_real y)) = 0"
-by (cut_tac x = y and y = 0 in linorder_less_linear, auto)
-declare cos_arg_i_mult_zero3 [simp]
+lemma cos_arg_i_mult_zero [simp]
+    : "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
+by (cut_tac x = y and y = 0 in linorder_less_linear, 
+    auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
 
 
 subsection{*Finally! Polar Form for Complex Numbers*}
 
-lemma complex_split_polar: "EX r a. z = complex_of_real r *
+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 complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
+apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
 done
 
-lemma rcis_Ex: "EX r a. z = rcis r a"
+lemma rcis_Ex: "\<exists>r a. z = rcis r a"
 apply (unfold rcis_def cis_def)
 apply (rule complex_split_polar)
 done
@@ -1415,7 +1364,7 @@
 lemma DeMoivre2:
    "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
 apply (unfold rcis_def)
-apply (auto simp add: complexpow_mult DeMoivre complex_of_real_pow)
+apply (auto simp add: power_mult_distrib DeMoivre complex_of_real_pow)
 done
 
 lemma cis_inverse: "inverse(cis a) = cis (-a)"
@@ -1425,9 +1374,9 @@
 declare cis_inverse [simp]
 
 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-apply (case_tac "r=0")
-apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
-apply (auto simp add: complex_inverse_complex_split complex_add_mult_distrib2 complex_of_real_mult rcis_def cis_def power2_eq_square complex_mult_ac mult_ac)
+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
 
@@ -1436,8 +1385,7 @@
 apply (auto simp add: cis_mult real_diff_def)
 done
 
-lemma rcis_divide:
- "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
+lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
 apply (unfold complex_divide_def)
 apply (case_tac "r2=0")
 apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
@@ -1461,13 +1409,11 @@
 lemma expi_Im_split:
     "expi (ii * complex_of_real y) =
      complex_of_real (cos y) + ii * complex_of_real (sin y)"
-apply (unfold expi_def cis_def, auto)
-done
+by (unfold expi_def cis_def, auto)
 
 lemma expi_Im_cis:
     "expi (ii * complex_of_real y) = cis y"
-apply (unfold expi_def, auto)
-done
+by (unfold expi_def, auto)
 
 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
 apply (unfold expi_def)
@@ -1477,8 +1423,7 @@
 lemma expi_complex_split:
      "expi(complex_of_real x + ii * complex_of_real y) =
       complex_of_real (exp(x)) * cis y"
-apply (unfold expi_def, auto)
-done
+by (unfold expi_def, auto)
 
 lemma expi_zero: "expi (0::complex) = 1"
 by (unfold expi_def, auto)
@@ -1498,7 +1443,7 @@
 done
 
 lemma complex_expi_Ex: 
-   "EX a r. z = complex_of_real r * expi a"
+   "\<exists>a r. z = complex_of_real r * expi a"
 apply (cut_tac z = z in rcis_Ex)
 apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
 apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
@@ -1506,12 +1451,12 @@
 
 
 (****
-Goal "[| - pi < a; a <= pi |] ==> (-pi < a & a <= 0) | (0 <= a & a <= pi)"
+Goal "[| - pi < a; a \<le> pi |] ==> (-pi < a & a \<le> 0) | (0 \<le> a & a \<le> pi)"
 by Auto_tac
 qed "lemma_split_interval";
 
 Goalw [arg_def]
-  "[| r ~= 0; - pi < a; a <= pi |] \
+  "[| r \<noteq> 0; - pi < a; a \<le> pi |] \
 \  ==> arg(complex_of_real r * \
 \      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
 by Auto_tac
@@ -1680,21 +1625,11 @@
 val complex_mod_gt_zero = thm"complex_mod_gt_zero";
 val complex_mod_complexpow = thm"complex_mod_complexpow";
 val complexpow_minus = thm"complexpow_minus";
-val complex_inverse_minus = thm"complex_inverse_minus";
-val complex_divide_one = thm"complex_divide_one";
 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_mult = thm"complexpow_mult";
-val complexpow_zero = thm"complexpow_zero";
-val complexpow_not_zero = thm"complexpow_not_zero";
-val complexpow_zero_zero = thm"complexpow_zero_zero";
 val complexpow_i_squared = thm"complexpow_i_squared";
 val complex_i_not_zero = thm"complex_i_not_zero";
-val complex_mult_eq_zero_cancel1 = thm"complex_mult_eq_zero_cancel1";
-val complex_mult_eq_zero_cancel2 = thm"complex_mult_eq_zero_cancel2";
-val complex_mult_not_eq_zero_iff = thm"complex_mult_not_eq_zero_iff";
-val complexpow_inverse = thm"complexpow_inverse";
 val sgn_zero = thm"sgn_zero";
 val sgn_one = thm"sgn_one";
 val sgn_minus = thm"sgn_minus";
@@ -1724,10 +1659,7 @@
 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 cos_arg_i_mult_zero2 = thm"cos_arg_i_mult_zero2";
-val complex_of_real_not_zero_iff = thm"complex_of_real_not_zero_iff";
 val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val cos_arg_i_mult_zero3 = thm"cos_arg_i_mult_zero3";
 val complex_split_polar = thm"complex_split_polar";
 val rcis_Ex = thm"rcis_Ex";
 val Re_complex_polar = thm"Re_complex_polar";
diff -r 79f9fbef9106 -r 988aa4648597 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Mon Jan 12 16:51:45 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Tue Jan 13 10:37:52 2004 +0100
@@ -6,9 +6,6 @@
 
 theory NSComplex = NSInduct:
 
-(*for Ring_and_Field?*)
-declare field_mult_eq_0_iff [simp]
-
 (* Move to one of the hyperreal theories *)
 lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
 apply (induct_tac "m")
@@ -17,13 +14,13 @@
 
 (* not proved already? strange! *)
 lemma hypreal_of_nat_le_iff:
-      "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"
+      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
 apply (unfold hypreal_le_def)
 apply auto
 done
 declare hypreal_of_nat_le_iff [simp]
 
-lemma hypreal_of_nat_ge_zero: "0 <= hypreal_of_nat n"
+lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
 apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
          del: hypreal_of_nat_zero)
 done
@@ -31,7 +28,7 @@
 
 declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
 
-lemma hypreal_of_hypnat_ge_zero: "0 <= hypreal_of_hypnat n"
+lemma hypreal_of_hypnat_ge_zero: "0 \<le> hypreal_of_hypnat n"
 apply (rule_tac z = "n" in eq_Abs_hypnat)
 apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
 done
@@ -40,7 +37,7 @@
 
 constdefs
     hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
-    "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) &
+    "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
                         {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
 
 typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
@@ -147,10 +144,6 @@
 		      hcomplexrel `` {%n. X n * Y n})"
 
 
-primrec
-     hcomplexpow_0:   "z ^ 0       = 1"
-     hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
-
 
 consts
   "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr 80)
@@ -220,13 +213,13 @@
 done
 declare lemma_hcomplexrel_refl [simp]
 
-lemma hcomplex_empty_not_mem: "{} ~: hcomplex"
+lemma hcomplex_empty_not_mem: "{} \<notin> hcomplex"
 apply (unfold hcomplex_def)
 apply (auto elim!: quotientE)
 done
 declare hcomplex_empty_not_mem [simp]
 
-lemma Rep_hcomplex_nonempty: "Rep_hcomplex x ~= {}"
+lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \<noteq> {}"
 apply (cut_tac x = "x" in Rep_hcomplex)
 apply auto
 done
@@ -290,23 +283,8 @@
 done
 declare hcomplex_hIm_one [simp]
 
-(*-----------------------------------------------------------------------*)
-(*   hcomplex_of_complex: the injection from complex to hcomplex         *)
-(* ----------------------------------------------------------------------*)
 
-lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
-apply (rule inj_onI , rule ccontr)
-apply (auto simp add: hcomplex_of_complex_def)
-done
-
-lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
-apply (unfold iii_def hcomplex_of_complex_def)
-apply (simp (no_asm))
-done
-
-(*-----------------------------------------------------------------------*)
-(*   Addition for nonstandard complex numbers: hcomplex_add              *)
-(* ----------------------------------------------------------------------*)
+subsection{*Addition for Nonstandard Complex Numbers*}
 
 lemma hcomplex_add_congruent2:
     "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
@@ -358,9 +336,8 @@
 apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
 done
 
-(*-----------------------------------------------------------------------*)
-(* hypreal_minus: additive inverse on nonstandard complex                *)
-(* ----------------------------------------------------------------------*)
+
+subsection{*Additive Inverse on Nonstandard Complex Numbers*}
 
 lemma hcomplex_minus_congruent:
   "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
@@ -427,7 +404,7 @@
 apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib)
 done
 
-lemma hcomplex_zero_not_eq_one: "(0::hcomplex) ~= (1::hcomplex)"
+lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
 apply (unfold hcomplex_zero_def hcomplex_one_def)
 apply auto
 done
@@ -446,7 +423,7 @@
 done
 
 lemma hcomplex_mult_inv_left:
-      "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
+      "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
 apply (unfold hcomplex_zero_def hcomplex_one_def)
 apply (rule_tac z = "z" in eq_Abs_hcomplex)
 apply (auto simp add: hcomplex_inverse hcomplex_mult)
@@ -553,11 +530,11 @@
 declare hcomplex_mult_minus_one_right [simp]
 
 lemma hcomplex_mult_left_cancel:
-     "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"
+     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
 by (simp add: field_mult_cancel_left) 
 
 lemma hcomplex_mult_right_cancel:
-     "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"
+     "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
 apply (simp add: Ring_and_Field.field_mult_cancel_right); 
 done
 
@@ -661,12 +638,6 @@
 apply (auto simp add: hcomplex_of_hypreal)
 done
 
-lemma hcomplex_of_hypreal_pow:
-     "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
-done
-
 lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
 apply (rule_tac z = "z" in eq_Abs_hypreal)
 apply (auto simp add: hcomplex_of_hypreal hRe)
@@ -679,7 +650,7 @@
 done
 declare hIm_hcomplex_of_hypreal [simp]
 
-lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon ~= 0"
+lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \<noteq> 0"
 apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
 done
 declare hcomplex_of_hypreal_epsilon_not_zero [simp]
@@ -802,10 +773,6 @@
 done
 declare hcnj_one [simp]
 
-lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcomplex_hcnj_mult)
-done
 
 (* MOVE to NSComplexBin
 Goal "z + hcnj z =
@@ -844,9 +811,7 @@
 done
 
 
-(*---------------------------------------------------------------------------*)
-(*  More theorems about hcmod                                                *)
-(*---------------------------------------------------------------------------*)
+subsection{*More Theorems about the Function @{term hcmod}*}
 
 lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
@@ -877,7 +842,7 @@
 apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
 done
 
-lemma hcmod_ge_zero: "(0::hypreal) <= hcmod x"
+lemma hcmod_ge_zero: "(0::hypreal) \<le> hcmod x"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
 apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
 done
@@ -906,20 +871,20 @@
                  hypreal_of_real_def [symmetric])
 done
 
-lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) <= hcmod(x * hcnj y)"
+lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
 apply (rule_tac z = "y" in eq_Abs_hcomplex)
 apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
 done
 declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
 
-lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) <= hcmod(x * y)"
+lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \<le> hcmod(x * y)"
 apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
 apply (simp add: hcmod_mult)
 done
 declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
 
-lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 <= (hcmod(x) + hcmod(y)) ^ 2"
+lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
 apply (rule_tac z = "y" in eq_Abs_hcomplex)
 apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
@@ -929,14 +894,14 @@
 done
 declare hcmod_triangle_squared [simp]
 
-lemma hcmod_triangle_ineq: "hcmod (x + y) <= hcmod(x) + hcmod(y)"
+lemma hcmod_triangle_ineq: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
 apply (rule_tac z = "y" in eq_Abs_hcomplex)
 apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
 done
 declare hcmod_triangle_ineq [simp]
 
-lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a"
+lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \<le> hcmod a"
 apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
 apply (simp add: add_ac)
 done
@@ -970,7 +935,7 @@
 apply (auto intro: complex_mod_mult_less)
 done
 
-lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) <= hcmod(a + b)"
+lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
 apply (rule_tac z = "a" in eq_Abs_hcomplex)
 apply (rule_tac z = "b" in eq_Abs_hcomplex)
 apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
@@ -997,45 +962,12 @@
 apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
 done
 
-lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: hcmod_mult)
-done
-
 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
 apply (rule_tac z = "x" in eq_Abs_hcomplex)
 apply (rule_tac z = "n" in eq_Abs_hypnat)
 apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
 done
 
-lemma hcomplexpow_minus:
-     "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
-apply (induct_tac "n")
-apply auto
-done
-
-lemma hcpow_minus:
-     "(-x::hcomplex) hcpow n =
-      (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
-apply (rule_tac z = "x" in eq_Abs_hcomplex)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
-apply ultra
-apply (auto simp add: complexpow_minus) 
-apply ultra
-done
-
-lemma hccomplex_inverse_minus: "inverse(-x) = - inverse (x::hcomplex)"
-apply (rule_tac z = "x" in eq_Abs_hcomplex)
-apply (auto simp add: hcomplex_inverse hcomplex_minus complex_inverse_minus)
-done
-
-lemma hcomplex_div_one: "x / (1::hcomplex) = x"
-apply (unfold hcomplex_divide_def)
-apply (simp (no_asm))
-done
-declare hcomplex_div_one [simp]
-
 lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
 apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
 apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
@@ -1055,58 +987,78 @@
 done
 declare hcomplex_inverse_divide [simp]
 
-lemma hcomplexpow_mult: "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"
+
+subsection{*Exponentiation*}
+
+primrec
+     hcomplexpow_0:   "z ^ 0       = 1"
+     hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
+
+instance hcomplex :: ringpower
+proof
+  fix z :: hcomplex
+  fix n :: nat
+  show "z^0 = 1" by simp
+  show "z^(Suc n) = z * (z^n)" by simp
+qed
+
+
+lemma hcomplex_of_hypreal_pow:
+     "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: hcomplex_of_hypreal_mult [symmetric])
+done
+
+lemma hcomplex_hcnj_pow: "hcnj(z ^ n) = hcnj(z) ^ n"
 apply (induct_tac "n")
-apply (auto simp add: mult_ac)
+apply (auto simp add: hcomplex_hcnj_mult)
+done
+
+lemma hcmod_hcomplexpow: "hcmod(x ^ n) = hcmod(x) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: hcmod_mult)
+done
+
+lemma hcomplexpow_minus:
+     "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
+apply (induct_tac "n")
+apply auto
+done
+
+lemma hcpow_minus:
+     "(-x::hcomplex) hcpow n =
+      (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
+apply (rule_tac z = "x" in eq_Abs_hcomplex)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
+apply ultra
+apply (auto simp add: complexpow_minus) 
+apply ultra
 done
 
 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
 apply (rule_tac z = "r" in eq_Abs_hcomplex)
 apply (rule_tac z = "s" in eq_Abs_hcomplex)
 apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (auto simp add: hcpow hypreal_mult hcomplex_mult complexpow_mult)
+apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
 done
 
-lemma hcomplexpow_zero: "(0::hcomplex) ^ (Suc n) = 0"
-apply auto
-done
-declare hcomplexpow_zero [simp]
-
-lemma hcpow_zero:
-   "0 hcpow (n + 1) = 0"
+lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
 apply (unfold hcomplex_zero_def hypnat_one_def)
 apply (rule_tac z = "n" in eq_Abs_hypnat)
 apply (auto simp add: hcpow hypnat_add)
 done
-declare hcpow_zero [simp]
 
-lemma hcpow_zero2:
-   "0 hcpow (hSuc n) = 0"
+lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
 apply (unfold hSuc_def)
 apply (simp (no_asm))
 done
-declare hcpow_zero2 [simp]
 
-lemma hcomplexpow_not_zero [rule_format (no_asm)]:
-     "r ~= (0::hcomplex) --> r ^ n ~= 0"
-apply (induct_tac "n")
-apply (auto)
-done
-declare hcomplexpow_not_zero [simp]
-declare hcomplexpow_not_zero [intro]
-
-lemma hcpow_not_zero: "r ~= 0 ==> r hcpow n ~= (0::hcomplex)"
+lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
 apply (rule_tac z = "r" in eq_Abs_hcomplex)
 apply (rule_tac z = "n" in eq_Abs_hypnat)
 apply (auto simp add: hcpow hcomplex_zero_def)
 apply ultra
-apply (auto dest: complexpow_zero_zero)
-done
-declare hcpow_not_zero [simp]
-declare hcpow_not_zero [intro]
-
-lemma hcomplexpow_zero_zero: "r ^ n = (0::hcomplex) ==> r = 0"
-apply (blast intro: ccontr dest: hcomplexpow_not_zero)
 done
 
 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
@@ -1124,26 +1076,12 @@
 done
 declare hcomplexpow_i_squared [simp]
 
-lemma hcomplex_i_not_zero: "iii ~= 0"
+lemma hcomplex_i_not_zero: "iii \<noteq> 0"
 apply (unfold iii_def hcomplex_zero_def)
 apply auto
 done
 declare hcomplex_i_not_zero [simp]
 
-lemma hcomplex_mult_eq_zero_cancel1: "x * y ~= (0::hcomplex) ==> x ~= 0"
-apply auto
-done
-
-lemma hcomplex_mult_eq_zero_cancel2: "x * y ~= (0::hcomplex) ==> y ~= 0"
-apply auto
-done
-
-lemma hcomplex_mult_not_eq_zero_iff:
-     "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"
-apply auto
-done
-declare hcomplex_mult_not_eq_zero_iff [iff]
-
 lemma hcomplex_divide:
   "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
    Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
@@ -1186,8 +1124,8 @@
 done
 
 lemma lemma_hypreal_P_EX2:
-     "(EX (x::hypreal) y. P x y) =
-      (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
+     "(\<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)
@@ -1195,13 +1133,13 @@
 done
 
 lemma complex_split2:
-     "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
+     "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
 apply (blast intro: complex_split)
 done
 
 (* Interesting proof! *)
 lemma hcomplex_split:
-     "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
+     "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
 apply (rule_tac z = "z" in eq_Abs_hcomplex)
 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)
@@ -1409,54 +1347,45 @@
 apply (auto, ultra)
 done
 
-lemma cos_harg_i_mult_zero:
+lemma cos_harg_i_mult_zero_pos:
      "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
 apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
+apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult 
+                hypreal_zero_num hypreal_less starfun harg)
 apply (ultra)
 done
-declare cos_harg_i_mult_zero [simp]
 
-lemma cos_harg_i_mult_zero2:
+lemma cos_harg_i_mult_zero_neg:
      "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
 apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult hypreal_zero_num hypreal_less starfun harg)
+apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
+                      hypreal_zero_num hypreal_less starfun harg)
 apply (ultra)
 done
-declare cos_harg_i_mult_zero2 [simp]
 
-lemma hcomplex_of_hypreal_not_zero_iff:
-     "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"
+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 hypreal_linear)
+apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
+done
+
+lemma hcomplex_of_hypreal_zero_iff [simp]:
+     "(hcomplex_of_hypreal y = 0) = (y = 0)"
 apply (rule_tac z = "y" in eq_Abs_hypreal)
 apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
 done
-declare hcomplex_of_hypreal_not_zero_iff [simp]
 
-lemma hcomplex_of_hypreal_zero_iff: "(hcomplex_of_hypreal y = 0) = (y = 0)"
-apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
-done
-declare hcomplex_of_hypreal_zero_iff [simp]
 
-lemma cos_harg_i_mult_zero3:
-     "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
-apply (cut_tac x = "y" and y = "0" in hypreal_linear)
-apply auto
-done
-declare cos_harg_i_mult_zero3 [simp]
-
-(*---------------------------------------------------------------------------*)
-(* Polar form for nonstandard complex numbers                                 *)
-(*---------------------------------------------------------------------------*)
+subsection{*Polar Form for Nonstandard Complex Numbers*}
 
 lemma complex_split_polar2:
-     "ALL n. EX r a. (z n) = complex_of_real r *
+     "\<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)
 done
 
 lemma hcomplex_split_polar:
-  "EX r a. z = hcomplex_of_hypreal r *
+  "\<exists>r a. z = hcomplex_of_hypreal r *
    (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
 apply (rule_tac z = "z" in eq_Abs_hcomplex)
 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
@@ -1491,7 +1420,7 @@
 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
 done
 
-lemma hrcis_Ex: "EX r a. z = hrcis r a"
+lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
 apply (simp (no_asm) add: hrcis_def hcis_eq)
 apply (rule hcomplex_split_polar)
 done
@@ -1627,7 +1556,7 @@
 lemma DeMoivre2:
   "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
 apply (unfold hrcis_def)
-apply (auto simp add: hcomplexpow_mult NSDeMoivre hcomplex_of_hypreal_pow)
+apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
 done
 
 lemma DeMoivre2_ext:
@@ -1691,7 +1620,18 @@
 done
 
 
-subsection{*@{term hcomplex_of_complex} Preserves Field Properties*}
+subsection{*@{term hcomplex_of_complex}: the Injection from 
+  type @{typ complex} to to @{typ hcomplex}*}
+
+lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
+apply (rule inj_onI , rule ccontr)
+apply (auto simp add: hcomplex_of_complex_def)
+done
+
+lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
+apply (unfold iii_def hcomplex_of_complex_def)
+apply (simp (no_asm))
+done
 
 lemma hcomplex_of_complex_add:
      "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
@@ -1905,26 +1845,17 @@
 val hcmod_hcpow = thm"hcmod_hcpow";
 val hcomplexpow_minus = thm"hcomplexpow_minus";
 val hcpow_minus = thm"hcpow_minus";
-val hccomplex_inverse_minus = thm"hccomplex_inverse_minus";
-val hcomplex_div_one = thm"hcomplex_div_one";
 val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
 val hcmod_divide = thm"hcmod_divide";
 val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
-val hcomplexpow_mult = thm"hcomplexpow_mult";
 val hcpow_mult = thm"hcpow_mult";
-val hcomplexpow_zero = thm"hcomplexpow_zero";
 val hcpow_zero = thm"hcpow_zero";
 val hcpow_zero2 = thm"hcpow_zero2";
-val hcomplexpow_not_zero = thm"hcomplexpow_not_zero";
 val hcpow_not_zero = thm"hcpow_not_zero";
-val hcomplexpow_zero_zero = thm"hcomplexpow_zero_zero";
 val hcpow_zero_zero = thm"hcpow_zero_zero";
 val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
 val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
 val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
-val hcomplex_mult_eq_zero_cancel1 = thm"hcomplex_mult_eq_zero_cancel1";
-val hcomplex_mult_eq_zero_cancel2 = thm"hcomplex_mult_eq_zero_cancel2";
-val hcomplex_mult_not_eq_zero_iff = thm"hcomplex_mult_not_eq_zero_iff";
 val hcomplex_divide = thm"hcomplex_divide";
 val hsgn = thm"hsgn";
 val hsgn_zero = thm"hsgn_zero";
@@ -1959,10 +1890,7 @@
 val hcmod_mult_i2 = thm"hcmod_mult_i2";
 val harg = thm"harg";
 val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
-val cos_harg_i_mult_zero2 = thm"cos_harg_i_mult_zero2";
-val hcomplex_of_hypreal_not_zero_iff = thm"hcomplex_of_hypreal_not_zero_iff";
 val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
-val cos_harg_i_mult_zero3 = thm"cos_harg_i_mult_zero3";
 val complex_split_polar2 = thm"complex_split_polar2";
 val hcomplex_split_polar = thm"hcomplex_split_polar";
 val hcis = thm"hcis";