# HG changeset patch # User huffman # Date 1178728000 -7200 # Node ID 9449c991cc33efffce13ce5c30f7c8eccb4b6ee6 # Parent f3bb32a68f16dd486f3d1e44787fafc67bba9162 remove redundant lemmas diff -r f3bb32a68f16 -r 9449c991cc33 src/HOL/Complex/Complex.thy --- 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) diff -r f3bb32a68f16 -r 9449c991cc33 src/HOL/Complex/NSComplex.thy --- 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)"