--- a/src/HOL/Complex/Complex.thy Wed May 09 18:25:44 2007 +0200
+++ b/src/HOL/Complex/Complex.thy Wed May 09 18:26:40 2007 +0200
@@ -474,18 +474,11 @@
show "z^(Suc n) = z * (z^n)" by simp
qed
-
-lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
-by (rule of_real_power)
-
lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
apply (induct_tac "n")
apply (auto simp add: complex_cnj_mult)
done
-lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
-by (rule norm_power)
-
lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
by (simp add: i_def complex_one_def numeral_2_eq_2)
@@ -693,7 +686,7 @@
done
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
-by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
+by (simp add: rcis_def power_mult_distrib DeMoivre)
lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
by (simp add: cis_def complex_inverse_complex_split diff_minus)
--- a/src/HOL/Complex/NSComplex.thy Wed May 09 18:25:44 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed May 09 18:26:40 2007 +0200
@@ -79,11 +79,7 @@
definition
HComplex :: "[hypreal,hypreal] => hcomplex" where
"HComplex = *f2* Complex"
-(*
-definition
- hcpow :: "[hcomplex,hypnat] => hcomplex" (infixr "hcpow" 80) where
- "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n"
-*)
+
lemmas hcomplex_defs [transfer_unfold] =
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
hrcis_def hexpi_def HComplex_def
@@ -356,16 +352,6 @@
by transfer (rule complex_mod_diff_ineq)
-subsection{*A Few Nonlinear Theorems*}
-
-lemma hcomplex_of_hypreal_hyperpow:
- "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) pow n"
-by transfer (rule complex_of_real_pow)
-
-lemma hcmod_hcpow: "!!x n. hcmod(x pow n) = hcmod(x) pow n"
-by transfer (rule complex_mod_complexpow)
-
-
subsection{*Exponentiation*}
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)"