# HG changeset patch
# User huffman
# Date 1315453479 25200
# Node ID 4d1384a1fc8293d69d67102e965153016c9d8b2c
# Parent  1120cba9bce438518998ec5b3db8f211f199a653
Complex.thy: move theorems into appropriate subsections

diff -r 1120cba9bce4 -r 4d1384a1fc82 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Sep 07 19:24:28 2011 -0700
+++ b/src/HOL/Complex.thy	Wed Sep 07 20:44:39 2011 -0700
@@ -253,6 +253,10 @@
   shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
   by (simp add: complex_of_real_def)
 
+lemma complex_split_polar:
+     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
+  by (simp add: complex_eq_iff polar_Ex)
+
 
 subsection {* Vector Norm *}
 
@@ -379,7 +383,7 @@
 qed
 
 
-subsection {* The Complex Number @{term "\<i>"} *}
+subsection {* The Complex Number $i$ *}
 
 definition "ii" :: complex  ("\<i>")
   where i_def: "ii \<equiv> Complex 0 1"
@@ -423,6 +427,9 @@
 lemma inverse_i [simp]: "inverse ii = - ii"
   by (rule inverse_unique, simp)
 
+lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
+  by (simp add: mult_assoc [symmetric])
+
 
 subsection {* Complex Conjugation *}
 
@@ -507,6 +514,12 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
   by (simp add: norm_mult power2_eq_square)
 
+lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
+  by (simp add: cmod_def power2_eq_square)
+
+lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
+  by simp
+
 lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR
   by (rule bounded_linear_intro [where K=1], simp)
@@ -518,9 +531,7 @@
   bounded_linear.isCont [OF bounded_linear_cnj]
 
 
-subsection{*The Functions @{term sgn} and @{term arg}*}
-
-text {*------------ Argand -------------*}
+subsection {* Complex Signum and Argument *}
 
 definition arg :: "complex => real" where
   "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
@@ -570,16 +581,84 @@
 
 subsection{*Finally! Polar Form for Complex Numbers*}
 
-text {* An abbreviation for @{text "cos a + i sin a"}. *}
+subsubsection {* $\cos \theta + i \sin \theta$ *}
 
 definition cis :: "real \<Rightarrow> complex" where
   "cis a = Complex (cos a) (sin a)"
 
-text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
+lemma Re_cis [simp]: "Re (cis a) = cos a"
+  by (simp add: cis_def)
+
+lemma Im_cis [simp]: "Im (cis a) = sin a"
+  by (simp add: cis_def)
+
+lemma cis_zero [simp]: "cis 0 = 1"
+  by (simp add: cis_def)
+
+lemma cis_mult: "cis a * cis b = cis (a + b)"
+  by (simp add: cis_def cos_add sin_add)
+
+lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
+  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
+
+lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
+  by (simp add: cis_def)
+
+lemma cis_divide: "cis a / cis b = cis (a - b)"
+  by (simp add: complex_divide_def cis_mult diff_minus)
+
+lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
+  by (auto simp add: DeMoivre)
+
+lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
+  by (auto simp add: DeMoivre)
+
+subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
 
 definition rcis :: "[real, real] \<Rightarrow> complex" where
   "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
+
+lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
+  by (simp add: rcis_def cis_def norm_mult)
+
+lemma cis_rcis_eq: "cis a = rcis 1 a"
+  by (simp add: rcis_def)
+
+lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
+  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
+    right_diff_distrib complex_of_real_def)
+
+lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
+  by (simp add: rcis_def)
+
+lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
+  by (simp add: rcis_def)
+
+lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
+  by (simp add: rcis_def power_mult_distrib DeMoivre)
+
+lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
+  by (simp add: divide_inverse rcis_def)
+
+lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
+apply (simp add: complex_divide_def)
+apply (case_tac "r2=0", simp)
+apply (simp add: rcis_inverse rcis_mult diff_minus)
+done
+
+subsubsection {* Complex exponential *}
+
 abbreviation expi :: "complex \<Rightarrow> complex"
   where "expi \<equiv> exp"
 
@@ -604,87 +683,6 @@
 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 complex_split_polar:
-     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
-apply (induct z)
-apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
-done
-
-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
-
-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 complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
-  by (simp add: rcis_def cis_def norm_mult)
-
-lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
-  by (simp add: cmod_def power2_eq_square)
-
-lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
-  by simp
-
-lemma cis_rcis_eq: "cis a = rcis 1 a"
-  by (simp add: rcis_def)
-
-lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
-    right_diff_distrib complex_of_real_def)
-
-lemma cis_mult: "cis a * cis b = cis (a + b)"
-  by (simp add: cis_rcis_eq rcis_mult)
-
-lemma cis_zero [simp]: "cis 0 = 1"
-  by (simp add: cis_def complex_one_def)
-
-lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
-  by (simp add: rcis_def)
-
-lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
-  by (simp add: rcis_def)
-
-lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
-  by (simp add: mult_assoc [symmetric])
-
-lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-  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)
-
-lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
-  by (simp add: cis_def complex_inverse_complex_split diff_minus)
-
-lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-  by (simp add: divide_inverse rcis_def)
-
-lemma cis_divide: "cis a / cis b = cis (a - b)"
-  by (simp add: complex_divide_def cis_mult diff_minus)
-
-lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
-apply (simp add: complex_divide_def)
-apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_minus)
-done
-
-lemma Re_cis [simp]: "Re(cis a) = cos a"
-  by (simp add: cis_def)
-
-lemma Im_cis [simp]: "Im(cis a) = sin a"
-  by (simp add: cis_def)
-
-lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
-  by (auto simp add: DeMoivre)
-
-lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
-  by (auto simp add: DeMoivre)
-
 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])