# HG changeset patch
# User huffman
# Date 1315446475 25200
# Node ID 34b83d981380eac2232c6eeb716b1331ede0e265
# Parent  6ce95c8c0ba813636b0cf2e0d59cb0cfe5fe9655
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma

diff -r 6ce95c8c0ba8 -r 34b83d981380 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Sep 07 10:04:07 2011 -0700
+++ b/src/HOL/Complex.thy	Wed Sep 07 18:47:55 2011 -0700
@@ -656,15 +656,8 @@
 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   by (simp add: mult_assoc [symmetric])
 
-
-lemma cis_real_of_nat_Suc_mult:
-   "cis (real (Suc n) * a) = cis a * cis (real n * a)"
-  by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
-
 lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-apply (induct_tac "n")
-apply (auto simp add: cis_real_of_nat_Suc_mult)
-done
+  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
 
 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
   by (simp add: rcis_def power_mult_distrib DeMoivre)
diff -r 6ce95c8c0ba8 -r 34b83d981380 src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Wed Sep 07 10:04:07 2011 -0700
+++ b/src/HOL/NSA/NSComplex.thy	Wed Sep 07 18:47:55 2011 -0700
@@ -561,8 +561,7 @@
    "!!a. hcis (hypreal_of_nat (Suc n) * a) =
      hcis a * hcis (hypreal_of_nat n * a)"
 apply transfer
-apply (fold real_of_nat_def)
-apply (rule cis_real_of_nat_Suc_mult)
+apply (simp add: left_distrib cis_mult)
 done
 
 lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
@@ -574,7 +573,7 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
+by transfer (simp add: left_distrib cis_mult)
 
 lemma NSDeMoivre_ext:
   "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"