author huffman Wed, 07 Sep 2011 20:44:39 -0700 changeset 44827 4d1384a1fc82 parent 44826 1120cba9bce4 child 44828 3d6a79e0e1d0
Complex.thy: move theorems into appropriate subsections
 src/HOL/Complex.thy file | annotate | diff | comparison | revisions
--- 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)"

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

+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"
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"
+
+lemma Im_cis [simp]: "Im (cis a) = sin a"
+
+lemma cis_zero [simp]: "cis 0 = 1"
+
+lemma cis_mult: "cis a * cis b = cis (a + b)"
+
+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)"
+
+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"
+
+lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
+    right_diff_distrib complex_of_real_def)
+
+lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
+
+lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
+
+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 (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"
-
-lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-    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"
-
-lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
-
-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 (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_minus)
-done
-
-lemma Re_cis [simp]: "Re(cis a) = cos a"
apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])