remove redundant lemmas expi_add and expi_zero
authorhuffman
Sun Sep 04 10:05:52 2011 -0700 (2011-09-04)
changeset 44711cd8dbfc272df
parent 44710 9caf6883f1f4
child 44712 1e490e891c88
remove redundant lemmas expi_add and expi_zero
NEWS
src/HOL/Complex.thy
src/HOL/NSA/NSComplex.thy
     1.1 --- a/NEWS	Sun Sep 04 09:49:45 2011 -0700
     1.2 +++ b/NEWS	Sun Sep 04 10:05:52 2011 -0700
     1.3 @@ -277,6 +277,8 @@
     1.4    realpow_two_diff ~> square_diff_square_factored
     1.5    reals_complete2 ~> complete_real
     1.6    exp_ln_eq ~> ln_unique
     1.7 +  expi_add ~> exp_add
     1.8 +  expi_zero ~> exp_zero
     1.9    lemma_DERIV_subst ~> DERIV_cong
    1.10    LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
    1.11    LIMSEQ_const ~> tendsto_const
     2.1 --- a/src/HOL/Complex.thy	Sun Sep 04 09:49:45 2011 -0700
     2.2 +++ b/src/HOL/Complex.thy	Sun Sep 04 10:05:52 2011 -0700
     2.3 @@ -736,12 +736,6 @@
     2.4  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
     2.5  by (auto simp add: DeMoivre)
     2.6  
     2.7 -lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
     2.8 -  by (rule exp_add) (* FIXME: redundant *)
     2.9 -
    2.10 -lemma expi_zero: "expi (0::complex) = 1"
    2.11 -  by (rule exp_zero) (* FIXME: redundant *)
    2.12 -
    2.13  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
    2.14  apply (insert rcis_Ex [of z])
    2.15  apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])
     3.1 --- a/src/HOL/NSA/NSComplex.thy	Sun Sep 04 09:49:45 2011 -0700
     3.2 +++ b/src/HOL/NSA/NSComplex.thy	Sun Sep 04 10:05:52 2011 -0700
     3.3 @@ -613,7 +613,7 @@
     3.4  by (simp add: NSDeMoivre_ext)
     3.5  
     3.6  lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
     3.7 -by transfer (rule expi_add)
     3.8 +by transfer (rule exp_add)
     3.9  
    3.10  
    3.11  subsection{*@{term hcomplex_of_complex}: the Injection from