author huffman Wed, 07 Sep 2011 18:47:55 -0700 changeset 44824 34b83d981380 parent 44823 6ce95c8c0ba8 child 44825 353ddca2e4c0
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
 src/HOL/Complex.thy file | annotate | diff | comparison | revisions src/HOL/NSA/NSComplex.thy file | annotate | diff | comparison | revisions
```--- 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"

-
-lemma cis_real_of_nat_Suc_mult:
-   "cis (real (Suc n) * a) = cis a * cis (real n * a)"
-
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-apply (induct_tac "n")
-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)