author huffman Wed Sep 07 18:47:55 2011 -0700 (2011-09-07) 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 | revisions src/HOL/NSA/NSComplex.thy file | annotate | diff | revisions
```     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.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)"
```