author huffman Wed, 07 Sep 2011 22:44:26 -0700 changeset 44828 3d6a79e0e1d0 parent 44827 4d1384a1fc82 child 44829 5a2cd5db0a11
 src/HOL/Complex.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complex.thy	Wed Sep 07 20:44:39 2011 -0700
+++ b/src/HOL/Complex.thy	Wed Sep 07 22:44:26 2011 -0700
@@ -595,6 +595,15 @@
lemma cis_zero [simp]: "cis 0 = 1"

+lemma norm_cis [simp]: "norm (cis a) = 1"
+
+lemma sgn_cis [simp]: "sgn (cis a) = cis a"
+
+lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
+  by (metis norm_cis norm_zero zero_neq_one)
+
lemma cis_mult: "cis a * cis b = cis (a + b)"

@@ -619,25 +628,22 @@
"rcis r a = complex_of_real r * cis a"

lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
-  by (simp add: rcis_def cis_def)

lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
-  by (simp add: rcis_def cis_def)

lemma rcis_Ex: "\<exists>r a. z = rcis r a"
-apply (induct z)
-apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
-done
+  by (simp add: complex_eq_iff polar_Ex)

lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
-  by (simp add: rcis_def cis_def norm_mult)
+  by (simp add: rcis_def norm_mult)

lemma cis_rcis_eq: "cis a = rcis 1 a"

lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-    right_diff_distrib complex_of_real_def)
+  by (simp add: rcis_def cis_mult)

lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
@@ -645,6 +651,9 @@
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"

+lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \<longleftrightarrow> r = 0"
+
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
by (simp add: rcis_def power_mult_distrib DeMoivre)

@@ -652,10 +661,7 @@

lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
-apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_minus)
-done
+  by (simp add: rcis_def cis_divide [symmetric])

subsubsection {* Complex exponential *}

@@ -683,6 +689,12 @@
lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp

+lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
+  unfolding expi_def by simp
+
+lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
+  unfolding expi_def by simp
+
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
apply (insert rcis_Ex [of z])
apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])```