Complex.thy: move theorems into appropriate subsections
authorhuffman
Wed Sep 07 20:44:39 2011 -0700 (2011-09-07)
changeset 448274d1384a1fc82
parent 44826 1120cba9bce4
child 44828 3d6a79e0e1d0
Complex.thy: move theorems into appropriate subsections
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 19:24:28 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 20:44:39 2011 -0700
     1.3 @@ -253,6 +253,10 @@
     1.4    shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
     1.5    by (simp add: complex_of_real_def)
     1.6  
     1.7 +lemma complex_split_polar:
     1.8 +     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
     1.9 +  by (simp add: complex_eq_iff polar_Ex)
    1.10 +
    1.11  
    1.12  subsection {* Vector Norm *}
    1.13  
    1.14 @@ -379,7 +383,7 @@
    1.15  qed
    1.16  
    1.17  
    1.18 -subsection {* The Complex Number @{term "\<i>"} *}
    1.19 +subsection {* The Complex Number $i$ *}
    1.20  
    1.21  definition "ii" :: complex  ("\<i>")
    1.22    where i_def: "ii \<equiv> Complex 0 1"
    1.23 @@ -423,6 +427,9 @@
    1.24  lemma inverse_i [simp]: "inverse ii = - ii"
    1.25    by (rule inverse_unique, simp)
    1.26  
    1.27 +lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
    1.28 +  by (simp add: mult_assoc [symmetric])
    1.29 +
    1.30  
    1.31  subsection {* Complex Conjugation *}
    1.32  
    1.33 @@ -507,6 +514,12 @@
    1.34  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
    1.35    by (simp add: norm_mult power2_eq_square)
    1.36  
    1.37 +lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
    1.38 +  by (simp add: cmod_def power2_eq_square)
    1.39 +
    1.40 +lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
    1.41 +  by simp
    1.42 +
    1.43  lemma bounded_linear_cnj: "bounded_linear cnj"
    1.44    using complex_cnj_add complex_cnj_scaleR
    1.45    by (rule bounded_linear_intro [where K=1], simp)
    1.46 @@ -518,9 +531,7 @@
    1.47    bounded_linear.isCont [OF bounded_linear_cnj]
    1.48  
    1.49  
    1.50 -subsection{*The Functions @{term sgn} and @{term arg}*}
    1.51 -
    1.52 -text {*------------ Argand -------------*}
    1.53 +subsection {* Complex Signum and Argument *}
    1.54  
    1.55  definition arg :: "complex => real" where
    1.56    "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
    1.57 @@ -570,16 +581,84 @@
    1.58  
    1.59  subsection{*Finally! Polar Form for Complex Numbers*}
    1.60  
    1.61 -text {* An abbreviation for @{text "cos a + i sin a"}. *}
    1.62 +subsubsection {* $\cos \theta + i \sin \theta$ *}
    1.63  
    1.64  definition cis :: "real \<Rightarrow> complex" where
    1.65    "cis a = Complex (cos a) (sin a)"
    1.66  
    1.67 -text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
    1.68 +lemma Re_cis [simp]: "Re (cis a) = cos a"
    1.69 +  by (simp add: cis_def)
    1.70 +
    1.71 +lemma Im_cis [simp]: "Im (cis a) = sin a"
    1.72 +  by (simp add: cis_def)
    1.73 +
    1.74 +lemma cis_zero [simp]: "cis 0 = 1"
    1.75 +  by (simp add: cis_def)
    1.76 +
    1.77 +lemma cis_mult: "cis a * cis b = cis (a + b)"
    1.78 +  by (simp add: cis_def cos_add sin_add)
    1.79 +
    1.80 +lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
    1.81 +  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
    1.82 +
    1.83 +lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
    1.84 +  by (simp add: cis_def)
    1.85 +
    1.86 +lemma cis_divide: "cis a / cis b = cis (a - b)"
    1.87 +  by (simp add: complex_divide_def cis_mult diff_minus)
    1.88 +
    1.89 +lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
    1.90 +  by (auto simp add: DeMoivre)
    1.91 +
    1.92 +lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
    1.93 +  by (auto simp add: DeMoivre)
    1.94 +
    1.95 +subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
    1.96  
    1.97  definition rcis :: "[real, real] \<Rightarrow> complex" where
    1.98    "rcis r a = complex_of_real r * cis a"
    1.99  
   1.100 +lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
   1.101 +  by (simp add: rcis_def cis_def)
   1.102 +
   1.103 +lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
   1.104 +  by (simp add: rcis_def cis_def)
   1.105 +
   1.106 +lemma rcis_Ex: "\<exists>r a. z = rcis r a"
   1.107 +apply (induct z)
   1.108 +apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
   1.109 +done
   1.110 +
   1.111 +lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
   1.112 +  by (simp add: rcis_def cis_def norm_mult)
   1.113 +
   1.114 +lemma cis_rcis_eq: "cis a = rcis 1 a"
   1.115 +  by (simp add: rcis_def)
   1.116 +
   1.117 +lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   1.118 +  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
   1.119 +    right_diff_distrib complex_of_real_def)
   1.120 +
   1.121 +lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
   1.122 +  by (simp add: rcis_def)
   1.123 +
   1.124 +lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
   1.125 +  by (simp add: rcis_def)
   1.126 +
   1.127 +lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
   1.128 +  by (simp add: rcis_def power_mult_distrib DeMoivre)
   1.129 +
   1.130 +lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
   1.131 +  by (simp add: divide_inverse rcis_def)
   1.132 +
   1.133 +lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
   1.134 +apply (simp add: complex_divide_def)
   1.135 +apply (case_tac "r2=0", simp)
   1.136 +apply (simp add: rcis_inverse rcis_mult diff_minus)
   1.137 +done
   1.138 +
   1.139 +subsubsection {* Complex exponential *}
   1.140 +
   1.141  abbreviation expi :: "complex \<Rightarrow> complex"
   1.142    where "expi \<equiv> exp"
   1.143  
   1.144 @@ -604,87 +683,6 @@
   1.145  lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
   1.146    unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
   1.147  
   1.148 -lemma complex_split_polar:
   1.149 -     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
   1.150 -apply (induct z)
   1.151 -apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
   1.152 -done
   1.153 -
   1.154 -lemma rcis_Ex: "\<exists>r a. z = rcis r a"
   1.155 -apply (induct z)
   1.156 -apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
   1.157 -done
   1.158 -
   1.159 -lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
   1.160 -  by (simp add: rcis_def cis_def)
   1.161 -
   1.162 -lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
   1.163 -  by (simp add: rcis_def cis_def)
   1.164 -
   1.165 -lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
   1.166 -  by (simp add: rcis_def cis_def norm_mult)
   1.167 -
   1.168 -lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
   1.169 -  by (simp add: cmod_def power2_eq_square)
   1.170 -
   1.171 -lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
   1.172 -  by simp
   1.173 -
   1.174 -lemma cis_rcis_eq: "cis a = rcis 1 a"
   1.175 -  by (simp add: rcis_def)
   1.176 -
   1.177 -lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   1.178 -  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
   1.179 -    right_diff_distrib complex_of_real_def)
   1.180 -
   1.181 -lemma cis_mult: "cis a * cis b = cis (a + b)"
   1.182 -  by (simp add: cis_rcis_eq rcis_mult)
   1.183 -
   1.184 -lemma cis_zero [simp]: "cis 0 = 1"
   1.185 -  by (simp add: cis_def complex_one_def)
   1.186 -
   1.187 -lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
   1.188 -  by (simp add: rcis_def)
   1.189 -
   1.190 -lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
   1.191 -  by (simp add: rcis_def)
   1.192 -
   1.193 -lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   1.194 -  by (simp add: mult_assoc [symmetric])
   1.195 -
   1.196 -lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
   1.197 -  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
   1.198 -
   1.199 -lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
   1.200 -  by (simp add: rcis_def power_mult_distrib DeMoivre)
   1.201 -
   1.202 -lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
   1.203 -  by (simp add: cis_def complex_inverse_complex_split diff_minus)
   1.204 -
   1.205 -lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
   1.206 -  by (simp add: divide_inverse rcis_def)
   1.207 -
   1.208 -lemma cis_divide: "cis a / cis b = cis (a - b)"
   1.209 -  by (simp add: complex_divide_def cis_mult diff_minus)
   1.210 -
   1.211 -lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
   1.212 -apply (simp add: complex_divide_def)
   1.213 -apply (case_tac "r2=0", simp)
   1.214 -apply (simp add: rcis_inverse rcis_mult diff_minus)
   1.215 -done
   1.216 -
   1.217 -lemma Re_cis [simp]: "Re(cis a) = cos a"
   1.218 -  by (simp add: cis_def)
   1.219 -
   1.220 -lemma Im_cis [simp]: "Im(cis a) = sin a"
   1.221 -  by (simp add: cis_def)
   1.222 -
   1.223 -lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
   1.224 -  by (auto simp add: DeMoivre)
   1.225 -
   1.226 -lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
   1.227 -  by (auto simp add: DeMoivre)
   1.228 -
   1.229  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
   1.230  apply (insert rcis_Ex [of z])
   1.231  apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])