--- 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)
--- 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)"