simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
authorhuffman
Wed Sep 07 18:47:55 2011 -0700 (2011-09-07)
changeset 4482434b83d981380
parent 44823 6ce95c8c0ba8
child 44825 353ddca2e4c0
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
src/HOL/Complex.thy
src/HOL/NSA/NSComplex.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 10:04:07 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 18:47:55 2011 -0700
     1.3 @@ -656,15 +656,8 @@
     1.4  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
     1.5    by (simp add: mult_assoc [symmetric])
     1.6  
     1.7 -
     1.8 -lemma cis_real_of_nat_Suc_mult:
     1.9 -   "cis (real (Suc n) * a) = cis a * cis (real n * a)"
    1.10 -  by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
    1.11 -
    1.12  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
    1.13 -apply (induct_tac "n")
    1.14 -apply (auto simp add: cis_real_of_nat_Suc_mult)
    1.15 -done
    1.16 +  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
    1.17  
    1.18  lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
    1.19    by (simp add: rcis_def power_mult_distrib DeMoivre)
     2.1 --- a/src/HOL/NSA/NSComplex.thy	Wed Sep 07 10:04:07 2011 -0700
     2.2 +++ b/src/HOL/NSA/NSComplex.thy	Wed Sep 07 18:47:55 2011 -0700
     2.3 @@ -561,8 +561,7 @@
     2.4     "!!a. hcis (hypreal_of_nat (Suc n) * a) =
     2.5       hcis a * hcis (hypreal_of_nat n * a)"
     2.6  apply transfer
     2.7 -apply (fold real_of_nat_def)
     2.8 -apply (rule cis_real_of_nat_Suc_mult)
     2.9 +apply (simp add: left_distrib cis_mult)
    2.10  done
    2.11  
    2.12  lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
    2.13 @@ -574,7 +573,7 @@
    2.14  lemma hcis_hypreal_of_hypnat_Suc_mult:
    2.15       "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
    2.16        hcis a * hcis (hypreal_of_hypnat n * a)"
    2.17 -by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
    2.18 +by transfer (simp add: left_distrib cis_mult)
    2.19  
    2.20  lemma NSDeMoivre_ext:
    2.21    "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"