src/HOL/Complex.thy
 author paulson Wed Jan 04 16:18:50 2017 +0000 (2017-01-04) changeset 64773 223b2ebdda79 parent 64290 fb5c74a58796 child 65064 a4abec71279a permissions -rw-r--r--
Many new theorems, and more tidying
 wenzelm@41959  1 (* Title: HOL/Complex.thy  wenzelm@63569  2  Author: Jacques D. Fleuriot, 2001 University of Edinburgh  wenzelm@63569  3  Author: Lawrence C Paulson, 2003/4  paulson@13957  4 *)  paulson@13957  5 wenzelm@60758  6 section \Complex Numbers: Rectangular and Polar Representations\  paulson@14373  7 nipkow@15131  8 theory Complex  haftmann@28952  9 imports Transcendental  nipkow@15131  10 begin  paulson@13957  11 wenzelm@60758  12 text \  wenzelm@63569  13  We use the \<^theory_text>\codatatype\ command to define the type of complex numbers. This  wenzelm@63569  14  allows us to use \<^theory_text>\primcorec\ to define complex functions by defining their  wenzelm@63569  15  real and imaginary result separately.  wenzelm@60758  16 \  paulson@14373  17 hoelzl@56889  18 codatatype complex = Complex (Re: real) (Im: real)  hoelzl@56889  19 hoelzl@56889  20 lemma complex_surj: "Complex (Re z) (Im z) = z"  hoelzl@56889  21  by (rule complex.collapse)  paulson@13957  22 wenzelm@63569  23 lemma complex_eqI [intro?]: "Re x = Re y \ Im x = Im y \ x = y"  hoelzl@56889  24  by (rule complex.expand) simp  huffman@23125  25 huffman@44065  26 lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y"  hoelzl@56889  27  by (auto intro: complex.expand)  huffman@23125  28 wenzelm@63569  29 wenzelm@60758  30 subsection \Addition and Subtraction\  huffman@23125  31 haftmann@25599  32 instantiation complex :: ab_group_add  haftmann@25571  33 begin  haftmann@25571  34 wenzelm@63569  35 primcorec zero_complex  wenzelm@63569  36  where  wenzelm@63569  37  "Re 0 = 0"  wenzelm@63569  38  | "Im 0 = 0"  haftmann@25571  39 wenzelm@63569  40 primcorec plus_complex  wenzelm@63569  41  where  wenzelm@63569  42  "Re (x + y) = Re x + Re y"  wenzelm@63569  43  | "Im (x + y) = Im x + Im y"  haftmann@25712  44 wenzelm@63569  45 primcorec uminus_complex  wenzelm@63569  46  where  wenzelm@63569  47  "Re (- x) = - Re x"  wenzelm@63569  48  | "Im (- x) = - Im x"  huffman@23125  49 wenzelm@63569  50 primcorec minus_complex  wenzelm@63569  51  where  wenzelm@63569  52  "Re (x - y) = Re x - Re y"  wenzelm@63569  53  | "Im (x - y) = Im x - Im y"  huffman@23125  54 haftmann@25712  55 instance  wenzelm@63569  56  by standard (simp_all add: complex_eq_iff)  haftmann@25712  57 haftmann@25712  58 end  haftmann@25712  59 wenzelm@63569  60 wenzelm@60758  61 subsection \Multiplication and Division\  huffman@23125  62 haftmann@59867  63 instantiation complex :: field  haftmann@25571  64 begin  haftmann@25571  65 wenzelm@63569  66 primcorec one_complex  wenzelm@63569  67  where  wenzelm@63569  68  "Re 1 = 1"  wenzelm@63569  69  | "Im 1 = 0"  paulson@14323  70 wenzelm@63569  71 primcorec times_complex  wenzelm@63569  72  where  wenzelm@63569  73  "Re (x * y) = Re x * Re y - Im x * Im y"  wenzelm@63569  74  | "Im (x * y) = Re x * Im y + Im x * Re y"  paulson@14323  75 wenzelm@63569  76 primcorec inverse_complex  wenzelm@63569  77  where  wenzelm@63569  78  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"  wenzelm@63569  79  | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"  paulson@14335  80 wenzelm@63569  81 definition "x div y = x * inverse y" for x y :: complex  paulson@14335  82 haftmann@25712  83 instance  wenzelm@63569  84  by standard  hoelzl@56889  85  (simp_all add: complex_eq_iff divide_complex_def  hoelzl@56889  86  distrib_left distrib_right right_diff_distrib left_diff_distrib  hoelzl@56889  87  power2_eq_square add_divide_distrib [symmetric])  paulson@14335  88 haftmann@25712  89 end  huffman@23125  90 hoelzl@56889  91 lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"  wenzelm@63569  92  by (simp add: divide_complex_def add_divide_distrib)  huffman@23125  93 hoelzl@56889  94 lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"  hoelzl@56889  95  unfolding divide_complex_def times_complex.sel inverse_complex.sel  wenzelm@63569  96  by (simp add: divide_simps)  huffman@23125  97 hoelzl@56889  98 lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"  hoelzl@56889  99  by (simp add: power2_eq_square)  huffman@20556  100 hoelzl@56889  101 lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x"  hoelzl@56889  102  by (simp add: power2_eq_square)  hoelzl@56889  103 lp15@59862  104 lemma Re_power_real [simp]: "Im x = 0 \ Re (x ^ n) = Re x ^ n "  huffman@44724  105  by (induct n) simp_all  huffman@23125  106 lp15@59862  107 lemma Im_power_real [simp]: "Im x = 0 \ Im (x ^ n) = 0"  hoelzl@56889  108  by (induct n) simp_all  huffman@23125  109 wenzelm@63569  110 wenzelm@60758  111 subsection \Scalar Multiplication\  huffman@20556  112 haftmann@25712  113 instantiation complex :: real_field  haftmann@25571  114 begin  haftmann@25571  115 wenzelm@63569  116 primcorec scaleR_complex  wenzelm@63569  117  where  wenzelm@63569  118  "Re (scaleR r x) = r * Re x"  wenzelm@63569  119  | "Im (scaleR r x) = r * Im x"  huffman@22972  120 haftmann@25712  121 instance  huffman@20556  122 proof  huffman@23125  123  fix a b :: real and x y :: complex  huffman@23125  124  show "scaleR a (x + y) = scaleR a x + scaleR a y"  webertj@49962  125  by (simp add: complex_eq_iff distrib_left)  huffman@23125  126  show "scaleR (a + b) x = scaleR a x + scaleR b x"  webertj@49962  127  by (simp add: complex_eq_iff distrib_right)  huffman@23125  128  show "scaleR a (scaleR b x) = scaleR (a * b) x"  haftmann@57512  129  by (simp add: complex_eq_iff mult.assoc)  huffman@23125  130  show "scaleR 1 x = x"  huffman@44065  131  by (simp add: complex_eq_iff)  huffman@23125  132  show "scaleR a x * y = scaleR a (x * y)"  huffman@44065  133  by (simp add: complex_eq_iff algebra_simps)  huffman@23125  134  show "x * scaleR a y = scaleR a (x * y)"  huffman@44065  135  by (simp add: complex_eq_iff algebra_simps)  huffman@20556  136 qed  huffman@20556  137 haftmann@25712  138 end  haftmann@25712  139 wenzelm@63569  140 wenzelm@60758  141 subsection \Numerals, Arithmetic, and Embedding from Reals\  paulson@14323  142 huffman@44724  143 abbreviation complex_of_real :: "real \ complex"  huffman@44724  144  where "complex_of_real \ of_real"  huffman@20557  145 hoelzl@59000  146 declare [[coercion "of_real :: real \ complex"]]  hoelzl@59000  147 declare [[coercion "of_rat :: rat \ complex"]]  hoelzl@56889  148 declare [[coercion "of_int :: int \ complex"]]  hoelzl@56889  149 declare [[coercion "of_nat :: nat \ complex"]]  hoelzl@56331  150 hoelzl@56889  151 lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"  hoelzl@56889  152  by (induct n) simp_all  hoelzl@56889  153 hoelzl@56889  154 lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0"  hoelzl@56889  155  by (induct n) simp_all  hoelzl@56889  156 hoelzl@56889  157 lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z"  hoelzl@56889  158  by (cases z rule: int_diff_cases) simp  hoelzl@56889  159 hoelzl@56889  160 lemma complex_Im_of_int [simp]: "Im (of_int z) = 0"  hoelzl@56889  161  by (cases z rule: int_diff_cases) simp  hoelzl@56889  162 hoelzl@56889  163 lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"  hoelzl@56889  164  using complex_Re_of_int [of "numeral v"] by simp  hoelzl@56889  165 hoelzl@56889  166 lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"  hoelzl@56889  167  using complex_Im_of_int [of "numeral v"] by simp  huffman@20557  168 huffman@20557  169 lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z"  hoelzl@56889  170  by (simp add: of_real_def)  huffman@20557  171 huffman@20557  172 lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"  hoelzl@56889  173  by (simp add: of_real_def)  hoelzl@56889  174 lp15@59613  175 lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"  lp15@59613  176  by (simp add: Re_divide sqr_conv_mult)  lp15@59613  177 lp15@59613  178 lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"  lp15@59613  179  by (simp add: Im_divide sqr_conv_mult)  lp15@61609  180 lp15@62379  181 lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n"  eberlm@61552  182  by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc)  eberlm@61552  183 lp15@62379  184 lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"  eberlm@61552  185  by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc)  lp15@59613  186 wenzelm@63569  187 lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z"  lp15@60017  188  by (auto simp: Reals_def)  lp15@60017  189 eberlm@61531  190 lemma complex_Re_fact [simp]: "Re (fact n) = fact n"  eberlm@61531  191 proof -  wenzelm@63569  192  have "(fact n :: complex) = of_real (fact n)"  wenzelm@63569  193  by simp  wenzelm@63569  194  also have "Re \ = fact n"  wenzelm@63569  195  by (subst Re_complex_of_real) simp_all  eberlm@61531  196  finally show ?thesis .  eberlm@61531  197 qed  eberlm@61531  198 eberlm@61531  199 lemma complex_Im_fact [simp]: "Im (fact n) = 0"  eberlm@61531  200  by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)  eberlm@61531  201 eberlm@61531  202 wenzelm@60758  203 subsection \The Complex Number $i$\  hoelzl@56889  204 wenzelm@63569  205 primcorec "ii" :: complex ("\")  wenzelm@63569  206  where  wenzelm@63569  207  "Re \ = 0"  wenzelm@63569  208  | "Im \ = 1"  huffman@20557  209 hoelzl@57259  210 lemma Complex_eq[simp]: "Complex a b = a + \ * b"  hoelzl@57259  211  by (simp add: complex_eq_iff)  hoelzl@57259  212 hoelzl@57259  213 lemma complex_eq: "a = Re a + \ * Im a"  hoelzl@57259  214  by (simp add: complex_eq_iff)  hoelzl@57259  215 hoelzl@57259  216 lemma fun_complex_eq: "f = (\x. Re (f x) + \ * Im (f x))"  hoelzl@57259  217  by (simp add: fun_eq_iff complex_eq)  hoelzl@57259  218 wenzelm@63569  219 lemma i_squared [simp]: "\ * \ = -1"  hoelzl@56889  220  by (simp add: complex_eq_iff)  hoelzl@56889  221 wenzelm@63569  222 lemma power2_i [simp]: "\\<^sup>2 = -1"  hoelzl@56889  223  by (simp add: power2_eq_square)  paulson@14377  224 wenzelm@63569  225 lemma inverse_i [simp]: "inverse \ = - \"  hoelzl@56889  226  by (rule inverse_unique) simp  hoelzl@56889  227 wenzelm@63569  228 lemma divide_i [simp]: "x / \ = - \ * x"  hoelzl@56889  229  by (simp add: divide_complex_def)  paulson@14377  230 wenzelm@63569  231 lemma complex_i_mult_minus [simp]: "\ * (\ * x) = - x"  haftmann@57512  232  by (simp add: mult.assoc [symmetric])  paulson@14377  233 wenzelm@63569  234 lemma complex_i_not_zero [simp]: "\ \ 0"  hoelzl@56889  235  by (simp add: complex_eq_iff)  huffman@20557  236 wenzelm@63569  237 lemma complex_i_not_one [simp]: "\ \ 1"  hoelzl@56889  238  by (simp add: complex_eq_iff)  hoelzl@56889  239 wenzelm@63569  240 lemma complex_i_not_numeral [simp]: "\ \ numeral w"  hoelzl@56889  241  by (simp add: complex_eq_iff)  huffman@44841  242 wenzelm@63569  243 lemma complex_i_not_neg_numeral [simp]: "\ \ - numeral w"  hoelzl@56889  244  by (simp add: complex_eq_iff)  hoelzl@56889  245 hoelzl@56889  246 lemma complex_split_polar: "\r a. z = complex_of_real r * (cos a + \ * sin a)"  huffman@44827  247  by (simp add: complex_eq_iff polar_Ex)  huffman@44827  248 lp15@59613  249 lemma i_even_power [simp]: "\ ^ (n * 2) = (-1) ^ n"  lp15@59613  250  by (metis mult.commute power2_i power_mult)  lp15@59613  251 wenzelm@63569  252 lemma Re_ii_times [simp]: "Re (\ * z) = - Im z"  lp15@59741  253  by simp  lp15@59741  254 wenzelm@63569  255 lemma Im_ii_times [simp]: "Im (\ * z) = Re z"  lp15@59741  256  by simp  lp15@59741  257 wenzelm@63569  258 lemma ii_times_eq_iff: "\ * w = z \ w = - (\ * z)"  lp15@59741  259  by auto  lp15@59741  260 wenzelm@63569  261 lemma divide_numeral_i [simp]: "z / (numeral n * \) = - (\ * z) / numeral n"  lp15@59741  262  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)  lp15@59741  263 wenzelm@63569  264 wenzelm@60758  265 subsection \Vector Norm\  paulson@14323  266 haftmann@25712  267 instantiation complex :: real_normed_field  haftmann@25571  268 begin  haftmann@25571  269 hoelzl@56889  270 definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"  haftmann@25571  271 huffman@44724  272 abbreviation cmod :: "complex \ real"  huffman@44724  273  where "cmod \ norm"  haftmann@25571  274 wenzelm@63569  275 definition complex_sgn_def: "sgn x = x /\<^sub>R cmod x"  haftmann@25571  276 wenzelm@63569  277 definition dist_complex_def: "dist x y = cmod (x - y)"  huffman@31413  278 hoelzl@62101  279 definition uniformity_complex_def [code del]:  hoelzl@62101  280  "(uniformity :: (complex \ complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"  hoelzl@62101  281 hoelzl@62101  282 definition open_complex_def [code del]:  hoelzl@62101  283  "open (U :: complex set) \ (\x\U. eventually ($$x', y). x' = x \ y \ U) uniformity)"  huffman@31292  284 wenzelm@63569  285 instance  wenzelm@63569  286 proof  huffman@31492  287  fix r :: real and x y :: complex and S :: "complex set"  huffman@23125  288  show "(norm x = 0) = (x = 0)"  hoelzl@56889  289  by (simp add: norm_complex_def complex_eq_iff)  huffman@23125  290  show "norm (x + y) \ norm x + norm y"  hoelzl@56889  291  by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq)  huffman@23125  292  show "norm (scaleR r x) = \r\ * norm x"  wenzelm@63569  293  by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric]  wenzelm@63569  294  real_sqrt_mult)  huffman@23125  295  show "norm (x * y) = norm x * norm y"  wenzelm@63569  296  by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric]  wenzelm@63569  297  power2_eq_square algebra_simps)  hoelzl@62101  298 qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+  huffman@20557  299 haftmann@25712  300 end  haftmann@25712  301 wenzelm@63569  302 declare uniformity_Abort[where 'a = complex, code]  hoelzl@62102  303 wenzelm@63569  304 lemma norm_ii [simp]: "norm \ = 1"  hoelzl@56889  305  by (simp add: norm_complex_def)  paulson@14323  306 hoelzl@56889  307 lemma cmod_unit_one: "cmod (cos a + \ * sin a) = 1"  hoelzl@56889  308  by (simp add: norm_complex_def)  hoelzl@56889  309 hoelzl@56889  310 lemma cmod_complex_polar: "cmod (r * (cos a + \ * sin a)) = \r\"  hoelzl@56889  311  by (simp add: norm_mult cmod_unit_one)  huffman@22861  312 huffman@22861  313 lemma complex_Re_le_cmod: "Re x \ cmod x"  wenzelm@63569  314  unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1)  huffman@22861  315 huffman@44761  316 lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x"  hoelzl@56889  317  by (rule order_trans [OF _ norm_ge_zero]) simp  huffman@22861  318 hoelzl@56889  319 lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \ cmod a"  hoelzl@56889  320  by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp  paulson@14323  321 chaieb@26117  322 lemma abs_Re_le_cmod: "\Re x\ \ cmod x"  hoelzl@56889  323  by (simp add: norm_complex_def)  chaieb@26117  324 chaieb@26117  325 lemma abs_Im_le_cmod: "\Im x\ \ cmod x"  hoelzl@56889  326  by (simp add: norm_complex_def)  hoelzl@56889  327 hoelzl@57259  328 lemma cmod_le: "cmod z \ \Re z\ + \Im z\"  hoelzl@57259  329  apply (subst complex_eq)  hoelzl@57259  330  apply (rule order_trans)  wenzelm@63569  331  apply (rule norm_triangle_ineq)  hoelzl@57259  332  apply (simp add: norm_mult)  hoelzl@57259  333  done  hoelzl@57259  334 hoelzl@56889  335 lemma cmod_eq_Re: "Im z = 0 \ cmod z = \Re z\"  hoelzl@56889  336  by (simp add: norm_complex_def)  hoelzl@56889  337 hoelzl@56889  338 lemma cmod_eq_Im: "Re z = 0 \ cmod z = \Im z\"  hoelzl@56889  339  by (simp add: norm_complex_def)  huffman@44724  340 wenzelm@63569  341 lemma cmod_power2: "(cmod z)\<^sup>2 = (Re z)\<^sup>2 + (Im z)\<^sup>2"  hoelzl@56889  342  by (simp add: norm_complex_def)  hoelzl@56889  343 hoelzl@56889  344 lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \ 0 \ Re z = - cmod z"  hoelzl@56889  345  using abs_Re_le_cmod[of z] by auto  hoelzl@56889  346 wenzelm@63569  347 lemma cmod_Re_le_iff: "Im x = Im y \ cmod x \ cmod y \ \Re x\ \ \Re y\"  lp15@62379  348  by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)  lp15@62379  349 wenzelm@63569  350 lemma cmod_Im_le_iff: "Re x = Re y \ cmod x \ cmod y \ \Im x\ \ \Im y\"  lp15@62379  351  by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)  lp15@62379  352 hoelzl@56889  353 lemma Im_eq_0: "\Re z\ = cmod z \ Im z = 0"  wenzelm@63569  354  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) (auto simp add: norm_complex_def)  hoelzl@56369  355 wenzelm@63569  356 lemma abs_sqrt_wlog: "(\x. x \ 0 \ P x (x\<^sup>2)) \ P \x\ (x\<^sup>2)"  wenzelm@63569  357  for x::"'a::linordered_idom"  wenzelm@63569  358  by (metis abs_ge_zero power2_abs)  hoelzl@56369  359 hoelzl@56369  360 lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z"  hoelzl@56889  361  unfolding norm_complex_def  hoelzl@56369  362  apply (rule abs_sqrt_wlog [where x="Re z"])  hoelzl@56369  363  apply (rule abs_sqrt_wlog [where x="Im z"])  hoelzl@56369  364  apply (rule power2_le_imp_le)  wenzelm@63569  365  apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])  hoelzl@56369  366  done  hoelzl@56369  367 lp15@59741  368 lemma complex_unit_circle: "z \ 0 \ (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"  lp15@59741  369  by (simp add: norm_complex_def divide_simps complex_eq_iff)  lp15@59741  370 hoelzl@56369  371 wenzelm@60758  372 text \Properties of complex signum.\  huffman@44843  373 huffman@44843  374 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"  haftmann@57512  375  by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)  huffman@44843  376 huffman@44843  377 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"  huffman@44843  378  by (simp add: complex_sgn_def divide_inverse)  huffman@44843  379 huffman@44843  380 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"  huffman@44843  381  by (simp add: complex_sgn_def divide_inverse)  huffman@44843  382 paulson@14354  383 haftmann@64290  384 subsection \Absolute value\  haftmann@64290  385 haftmann@64290  386 instantiation complex :: field_abs_sgn  haftmann@64290  387 begin  haftmann@64290  388 haftmann@64290  389 definition abs_complex :: "complex \ complex"  haftmann@64290  390  where "abs_complex = of_real \ norm"  haftmann@64290  391 haftmann@64290  392 instance  haftmann@64290  393  apply standard  haftmann@64290  394  apply (auto simp add: abs_complex_def complex_sgn_def norm_mult)  haftmann@64290  395  apply (auto simp add: scaleR_conv_of_real field_simps)  haftmann@64290  396  done  haftmann@64290  397 haftmann@64290  398 end  haftmann@64290  399 haftmann@64290  400 wenzelm@60758  401 subsection \Completeness of the Complexes\  huffman@23123  402 huffman@44290  403 lemma bounded_linear_Re: "bounded_linear Re"  wenzelm@63569  404  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)  huffman@44290  405 huffman@44290  406 lemma bounded_linear_Im: "bounded_linear Im"  wenzelm@63569  407  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)  huffman@23123  408 huffman@44290  409 lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]  huffman@44290  410 lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]  hoelzl@56381  411 lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]  hoelzl@56381  412 lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]  hoelzl@56381  413 lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]  hoelzl@56381  414 lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]  hoelzl@56381  415 lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]  hoelzl@56381  416 lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]  hoelzl@56381  417 lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]  hoelzl@56381  418 lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]  hoelzl@56381  419 lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]  hoelzl@56381  420 lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]  hoelzl@56381  421 lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]  hoelzl@56381  422 lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]  hoelzl@56369  423 huffman@36825  424 lemma tendsto_Complex [tendsto_intros]:  wenzelm@61973  425  "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F"  hoelzl@56889  426  by (auto intro!: tendsto_intros)  hoelzl@56369  427 hoelzl@56369  428 lemma tendsto_complex_iff:  wenzelm@61973  429  "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)"  hoelzl@56889  430 proof safe  wenzelm@61973  431  assume "((\x. Re (f x)) \ Re x) F" "((\x. Im (f x)) \ Im x) F"  wenzelm@61973  432  from tendsto_Complex[OF this] show "(f \ x) F"  hoelzl@56889  433  unfolding complex.collapse .  hoelzl@56889  434 qed (auto intro: tendsto_intros)  hoelzl@56369  435 wenzelm@63569  436 lemma continuous_complex_iff:  wenzelm@63569  437  "continuous F f \ continuous F (\x. Re (f x)) \ continuous F (\x. Im (f x))"  wenzelm@63569  438  by (simp only: continuous_def tendsto_complex_iff)  hoelzl@57259  439 lp15@64773  440 lemma continuous_on_of_real_o_iff [simp]:  lp15@64773  441  "continuous_on S (\x. complex_of_real (g x)) = continuous_on S g"  lp15@64773  442  using continuous_on_Re continuous_on_of_real by fastforce  lp15@64773  443 lp15@64773  444 lemma continuous_on_of_real_id [simp]:  lp15@64773  445  "continuous_on S (of_real :: real \ 'a::real_normed_algebra_1)"  lp15@64773  446  by (rule continuous_on_of_real [OF continuous_on_id])  lp15@64773  447 hoelzl@57259  448 lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \  hoelzl@57259  449  ((\x. Re (f x)) has_field_derivative (Re x)) F \  hoelzl@57259  450  ((\x. Im (f x)) has_field_derivative (Im x)) F"  wenzelm@63569  451  by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def  wenzelm@63569  452  tendsto_complex_iff field_simps bounded_linear_scaleR_left bounded_linear_mult_right)  hoelzl@57259  453 hoelzl@57259  454 lemma has_field_derivative_Re[derivative_intros]:  hoelzl@57259  455  "(f has_vector_derivative D) F \ ((\x. Re (f x)) has_field_derivative (Re D)) F"  hoelzl@57259  456  unfolding has_vector_derivative_complex_iff by safe  hoelzl@57259  457 hoelzl@57259  458 lemma has_field_derivative_Im[derivative_intros]:  hoelzl@57259  459  "(f has_vector_derivative D) F \ ((\x. Im (f x)) has_field_derivative (Im D)) F"  hoelzl@57259  460  unfolding has_vector_derivative_complex_iff by safe  hoelzl@57259  461 huffman@23123  462 instance complex :: banach  huffman@23123  463 proof  huffman@23123  464  fix X :: "nat \ complex"  huffman@23123  465  assume X: "Cauchy X"  wenzelm@63569  466  then have "(\n. Complex (Re (X n)) (Im (X n))) \  wenzelm@63569  467  Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))"  wenzelm@63569  468  by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1]  wenzelm@63569  469  Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)  hoelzl@56889  470  then show "convergent X"  hoelzl@56889  471  unfolding complex.collapse by (rule convergentI)  huffman@23123  472 qed  huffman@23123  473 wenzelm@63569  474 declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]  wenzelm@63569  475 lp15@56238  476 wenzelm@60758  477 subsection \Complex Conjugation\  huffman@23125  478 wenzelm@63569  479 primcorec cnj :: "complex \ complex"  wenzelm@63569  480  where  wenzelm@63569  481  "Re (cnj z) = Re z"  wenzelm@63569  482  | "Im (cnj z) = - Im z"  huffman@23125  483 wenzelm@63569  484 lemma complex_cnj_cancel_iff [simp]: "cnj x = cnj y \ x = y"  huffman@44724  485  by (simp add: complex_eq_iff)  huffman@23125  486 huffman@23125  487 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"  hoelzl@56889  488  by (simp add: complex_eq_iff)  huffman@23125  489 huffman@23125  490 lemma complex_cnj_zero [simp]: "cnj 0 = 0"  huffman@44724  491  by (simp add: complex_eq_iff)  huffman@23125  492 wenzelm@63569  493 lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \ z = 0"  huffman@44724  494  by (simp add: complex_eq_iff)  huffman@23125  495 hoelzl@56889  496 lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"  huffman@44724  497  by (simp add: complex_eq_iff)  huffman@23125  498 nipkow@64267  499 lemma cnj_sum [simp]: "cnj (sum f s) = (\x\s. cnj (f x))"  hoelzl@56889  500  by (induct s rule: infinite_finite_induct) auto  hoelzl@56369  501 hoelzl@56889  502 lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y"  huffman@44724  503  by (simp add: complex_eq_iff)  huffman@23125  504 hoelzl@56889  505 lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x"  huffman@44724  506  by (simp add: complex_eq_iff)  huffman@23125  507 huffman@23125  508 lemma complex_cnj_one [simp]: "cnj 1 = 1"  huffman@44724  509  by (simp add: complex_eq_iff)  huffman@23125  510 hoelzl@56889  511 lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"  huffman@44724  512  by (simp add: complex_eq_iff)  huffman@23125  513 nipkow@64272  514 lemma cnj_prod [simp]: "cnj (prod f s) = (\x\s. cnj (f x))"  hoelzl@56889  515  by (induct s rule: infinite_finite_induct) auto  hoelzl@56369  516 hoelzl@56889  517 lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"  hoelzl@56889  518  by (simp add: complex_eq_iff)  paulson@14323  519 hoelzl@56889  520 lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y"  hoelzl@56889  521  by (simp add: divide_complex_def)  huffman@23125  522 hoelzl@56889  523 lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n"  hoelzl@56889  524  by (induct n) simp_all  huffman@23125  525 huffman@23125  526 lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"  huffman@44724  527  by (simp add: complex_eq_iff)  huffman@23125  528 huffman@23125  529 lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"  huffman@44724  530  by (simp add: complex_eq_iff)  huffman@23125  531 huffman@47108  532 lemma complex_cnj_numeral [simp]: "cnj (numeral w) = numeral w"  huffman@47108  533  by (simp add: complex_eq_iff)  huffman@47108  534 haftmann@54489  535 lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"  huffman@44724  536  by (simp add: complex_eq_iff)  huffman@23125  537 hoelzl@56889  538 lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)"  huffman@44724  539  by (simp add: complex_eq_iff)  huffman@23125  540 huffman@23125  541 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"  hoelzl@56889  542  by (simp add: norm_complex_def)  paulson@14323  543 huffman@23125  544 lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"  huffman@44724  545  by (simp add: complex_eq_iff)  huffman@23125  546 wenzelm@63569  547 lemma complex_cnj_i [simp]: "cnj \ = - \"  huffman@44724  548  by (simp add: complex_eq_iff)  huffman@23125  549 huffman@23125  550 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"  huffman@44724  551  by (simp add: complex_eq_iff)  huffman@23125  552 wenzelm@63569  553 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \"  huffman@44724  554  by (simp add: complex_eq_iff)  paulson@14354  555 wenzelm@53015  556 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"  huffman@44724  557  by (simp add: complex_eq_iff power2_eq_square)  huffman@23125  558 wenzelm@53015  559 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"  huffman@44724  560  by (simp add: norm_mult power2_eq_square)  huffman@23125  561 huffman@44827  562 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"  hoelzl@56889  563  by (simp add: norm_complex_def power2_eq_square)  huffman@44827  564 huffman@44827  565 lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"  huffman@44827  566  by simp  huffman@44827  567 eberlm@61531  568 lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n"  eberlm@61531  569  by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp  eberlm@61531  570 eberlm@61531  571 lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"  wenzelm@63569  572  by (induct n arbitrary: z) (simp_all add: pochhammer_rec)  eberlm@61531  573 huffman@44290  574 lemma bounded_linear_cnj: "bounded_linear cnj"  wenzelm@63569  575  using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp  paulson@14354  576 hoelzl@56381  577 lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]  wenzelm@63569  578  and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]  wenzelm@63569  579  and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]  wenzelm@63569  580  and continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]  wenzelm@63569  581  and has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]  huffman@44290  582 wenzelm@61973  583 lemma lim_cnj: "((\x. cnj(f x)) \ cnj l) F \ (f \ l) F"  hoelzl@56889  584  by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)  hoelzl@56369  585 hoelzl@56369  586 lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)"  nipkow@64267  587  by (simp add: sums_def lim_cnj cnj_sum [symmetric] del: cnj_sum)  hoelzl@56369  588 paulson@14354  589 wenzelm@63569  590 subsection \Basic Lemmas\  lp15@55734  591 lp15@55734  592 lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"  hoelzl@56889  593  by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)  lp15@55734  594 lp15@55734  595 lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"  hoelzl@56889  596  by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)  lp15@55734  597 lp15@55734  598 lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"  wenzelm@63569  599  by (cases z)  wenzelm@63569  600  (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]  wenzelm@63569  601  simp del: of_real_power)  lp15@55734  602 wenzelm@63569  603 lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)\<^sup>2"  paulson@61104  604  using complex_norm_square by auto  paulson@61104  605 lp15@59741  606 lemma Re_complex_div_eq_0: "Re (a / b) = 0 \ Re (a * cnj b) = 0"  hoelzl@56889  607  by (auto simp add: Re_divide)  lp15@59613  608 lp15@59741  609 lemma Im_complex_div_eq_0: "Im (a / b) = 0 \ Im (a * cnj b) = 0"  hoelzl@56889  610  by (auto simp add: Im_divide)  hoelzl@56889  611 wenzelm@63569  612 lemma complex_div_gt_0: "(Re (a / b) > 0 \ Re (a * cnj b) > 0) \ (Im (a / b) > 0 \ Im (a * cnj b) > 0)"  wenzelm@63569  613 proof (cases "b = 0")  wenzelm@63569  614  case True  wenzelm@63569  615  then show ?thesis by auto  lp15@55734  616 next  wenzelm@63569  617  case False  hoelzl@56889  618  then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2"  hoelzl@56889  619  by (simp add: complex_eq_iff sum_power2_gt_zero_iff)  hoelzl@56889  620  then show ?thesis  hoelzl@56889  621  by (simp add: Re_divide Im_divide zero_less_divide_iff)  lp15@55734  622 qed  lp15@55734  623 lp15@59741  624 lemma Re_complex_div_gt_0: "Re (a / b) > 0 \ Re (a * cnj b) > 0"  lp15@59741  625  and Im_complex_div_gt_0: "Im (a / b) > 0 \ Im (a * cnj b) > 0"  hoelzl@56889  626  using complex_div_gt_0 by auto  lp15@55734  627 wenzelm@63569  628 lemma Re_complex_div_ge_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0"  lp15@59741  629  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)  lp15@55734  630 wenzelm@63569  631 lemma Im_complex_div_ge_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0"  lp15@59741  632  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)  lp15@55734  633 wenzelm@63569  634 lemma Re_complex_div_lt_0: "Re (a / b) < 0 \ Re (a * cnj b) < 0"  lp15@59741  635  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)  lp15@55734  636 wenzelm@63569  637 lemma Im_complex_div_lt_0: "Im (a / b) < 0 \ Im (a * cnj b) < 0"  lp15@59741  638  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)  lp15@55734  639 wenzelm@63569  640 lemma Re_complex_div_le_0: "Re (a / b) \ 0 \ Re (a * cnj b) \ 0"  lp15@59741  641  by (metis not_le Re_complex_div_gt_0)  lp15@55734  642 wenzelm@63569  643 lemma Im_complex_div_le_0: "Im (a / b) \ 0 \ Im (a * cnj b) \ 0"  lp15@59741  644  by (metis Im_complex_div_gt_0 not_le)  lp15@55734  645 paulson@61104  646 lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"  paulson@61104  647  by (simp add: Re_divide power2_eq_square)  paulson@61104  648 paulson@61104  649 lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"  paulson@61104  650  by (simp add: Im_divide power2_eq_square)  paulson@61104  651 paulson@61104  652 lemma Re_divide_Reals: "r \ Reals \ Re (z / r) = Re z / Re r"  paulson@61104  653  by (metis Re_divide_of_real of_real_Re)  paulson@61104  654 paulson@61104  655 lemma Im_divide_Reals: "r \ Reals \ Im (z / r) = Im z / Re r"  paulson@61104  656  by (metis Im_divide_of_real of_real_Re)  paulson@61104  657 nipkow@64267  658 lemma Re_sum[simp]: "Re (sum f s) = (\x\s. Re (f x))"  hoelzl@56369  659  by (induct s rule: infinite_finite_induct) auto  lp15@55734  660 nipkow@64267  661 lemma Im_sum[simp]: "Im (sum f s) = (\x\s. Im(f x))"  hoelzl@56369  662  by (induct s rule: infinite_finite_induct) auto  hoelzl@56369  663 hoelzl@56369  664 lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)"  nipkow@64267  665  unfolding sums_def tendsto_complex_iff Im_sum Re_sum ..  lp15@59613  666 hoelzl@56369  667 lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))"  hoelzl@56889  668  unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)  hoelzl@56369  669 hoelzl@56369  670 lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f"  hoelzl@56369  671  unfolding summable_complex_iff by simp  hoelzl@56369  672 hoelzl@56369  673 lemma summable_Re: "summable f \ summable (\x. Re (f x))"  hoelzl@56369  674  unfolding summable_complex_iff by blast  hoelzl@56369  675 hoelzl@56369  676 lemma summable_Im: "summable f \ summable (\x. Im (f x))"  hoelzl@56369  677  unfolding summable_complex_iff by blast  lp15@56217  678 paulson@61104  679 lemma complex_is_Nat_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_nat i)"  paulson@61104  680  by (auto simp: Nats_def complex_eq_iff)  paulson@61104  681 paulson@61104  682 lemma complex_is_Int_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_int i)"  paulson@61104  683  by (auto simp: Ints_def complex_eq_iff)  paulson@61104  684 hoelzl@56889  685 lemma complex_is_Real_iff: "z \ \ \ Im z = 0"  hoelzl@56889  686  by (auto simp: Reals_def complex_eq_iff)  lp15@55734  687 lp15@55734  688 lemma Reals_cnj_iff: "z \ \ \ cnj z = z"  hoelzl@56889  689  by (auto simp: complex_is_Real_iff complex_eq_iff)  lp15@55734  690 wenzelm@61944  691 lemma in_Reals_norm: "z \ \ \ norm z = \Re z\"  hoelzl@56889  692  by (simp add: complex_is_Real_iff norm_complex_def)  hoelzl@56369  693 hoelzl@56369  694 lemma series_comparison_complex:  hoelzl@56369  695  fixes f:: "nat \ 'a::banach"  hoelzl@56369  696  assumes sg: "summable g"  wenzelm@63569  697  and "\n. g n \ \" "\n. Re (g n) \ 0"  wenzelm@63569  698  and fg: "\n. n \ N \ norm(f n) \ norm(g n)"  hoelzl@56369  699  shows "summable f"  hoelzl@56369  700 proof -  wenzelm@63569  701  have g: "\n. cmod (g n) = Re (g n)"  wenzelm@63569  702  using assms by (metis abs_of_nonneg in_Reals_norm)  hoelzl@56369  703  show ?thesis  hoelzl@56369  704  apply (rule summable_comparison_test' [where g = "\n. norm (g n)" and N=N])  hoelzl@56369  705  using sg  wenzelm@63569  706  apply (auto simp: summable_def)  wenzelm@63569  707  apply (rule_tac x = "Re s" in exI)  wenzelm@63569  708  apply (auto simp: g sums_Re)  hoelzl@56369  709  apply (metis fg g)  hoelzl@56369  710  done  hoelzl@56369  711 qed  lp15@55734  712 wenzelm@63569  713 wenzelm@63569  714 subsection \Polar Form for Complex Numbers\  lp15@59746  715 lp15@62620  716 lemma complex_unimodular_polar:  wenzelm@63569  717  assumes "norm z = 1"  wenzelm@63569  718  obtains t where "0 \ t" "t < 2 * pi" "z = Complex (cos t) (sin t)"  wenzelm@63569  719  by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)  wenzelm@63569  720 paulson@14323  721 wenzelm@60758  722 subsubsection \\cos \theta + i \sin \theta\  huffman@20557  723 wenzelm@63569  724 primcorec cis :: "real \ complex"  wenzelm@63569  725  where  wenzelm@63569  726  "Re (cis a) = cos a"  wenzelm@63569  727  | "Im (cis a) = sin a"  huffman@44827  728 huffman@44827  729 lemma cis_zero [simp]: "cis 0 = 1"  hoelzl@56889  730  by (simp add: complex_eq_iff)  huffman@44827  731 huffman@44828  732 lemma norm_cis [simp]: "norm (cis a) = 1"  hoelzl@56889  733  by (simp add: norm_complex_def)  huffman@44828  734 huffman@44828  735 lemma sgn_cis [simp]: "sgn (cis a) = cis a"  huffman@44828  736  by (simp add: sgn_div_norm)  huffman@44828  737 huffman@44828  738 lemma cis_neq_zero [simp]: "cis a \ 0"  huffman@44828  739  by (metis norm_cis norm_zero zero_neq_one)  huffman@44828  740 huffman@44827  741 lemma cis_mult: "cis a * cis b = cis (a + b)"  hoelzl@56889  742  by (simp add: complex_eq_iff cos_add sin_add)  huffman@44827  743 huffman@44827  744 lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"  wenzelm@63569  745  by (induct n) (simp_all add: algebra_simps cis_mult)  huffman@44827  746 wenzelm@63569  747 lemma cis_inverse [simp]: "inverse (cis a) = cis (- a)"  hoelzl@56889  748  by (simp add: complex_eq_iff)  huffman@44827  749 huffman@44827  750 lemma cis_divide: "cis a / cis b = cis (a - b)"  hoelzl@56889  751  by (simp add: divide_complex_def cis_mult)  huffman@44827  752 wenzelm@63569  753 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"  huffman@44827  754  by (auto simp add: DeMoivre)  huffman@44827  755 wenzelm@63569  756 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"  huffman@44827  757  by (auto simp add: DeMoivre)  huffman@44827  758 hoelzl@56889  759 lemma cis_pi: "cis pi = -1"  hoelzl@56889  760  by (simp add: complex_eq_iff)  hoelzl@56889  761 wenzelm@63569  762 wenzelm@60758  763 subsubsection \r(\cos \theta + i \sin \theta)\  huffman@44715  764 wenzelm@63569  765 definition rcis :: "real \ real \ complex"  wenzelm@63569  766  where "rcis r a = complex_of_real r * cis a"  huffman@20557  767 huffman@44827  768 lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"  huffman@44828  769  by (simp add: rcis_def)  huffman@44827  770 huffman@44827  771 lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"  huffman@44828  772  by (simp add: rcis_def)  huffman@44827  773 huffman@44827  774 lemma rcis_Ex: "\r a. z = rcis r a"  huffman@44828  775  by (simp add: complex_eq_iff polar_Ex)  huffman@44827  776 wenzelm@61944  777 lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \r\"  huffman@44828  778  by (simp add: rcis_def norm_mult)  huffman@44827  779 huffman@44827  780 lemma cis_rcis_eq: "cis a = rcis 1 a"  huffman@44827  781  by (simp add: rcis_def)  huffman@44827  782 wenzelm@63569  783 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1 * r2) (a + b)"  huffman@44828  784  by (simp add: rcis_def cis_mult)  huffman@44827  785 huffman@44827  786 lemma rcis_zero_mod [simp]: "rcis 0 a = 0"  huffman@44827  787  by (simp add: rcis_def)  huffman@44827  788 huffman@44827  789 lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"  huffman@44827  790  by (simp add: rcis_def)  huffman@44827  791 huffman@44828  792 lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \ r = 0"  huffman@44828  793  by (simp add: rcis_def)  huffman@44828  794 huffman@44827  795 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"  huffman@44827  796  by (simp add: rcis_def power_mult_distrib DeMoivre)  huffman@44827  797 wenzelm@63569  798 lemma rcis_inverse: "inverse(rcis r a) = rcis (1 / r) (- a)"  huffman@44827  799  by (simp add: divide_inverse rcis_def)  huffman@44827  800 wenzelm@63569  801 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)"  huffman@44828  802  by (simp add: rcis_def cis_divide [symmetric])  huffman@44827  803 wenzelm@63569  804 wenzelm@60758  805 subsubsection \Complex exponential\  huffman@44827  806 hoelzl@56889  807 lemma cis_conv_exp: "cis b = exp (\ * b)"  hoelzl@56889  808 proof -  wenzelm@63569  809  have "(\ * complex_of_real b) ^ n /\<^sub>R fact n =  wenzelm@63569  810  of_real (cos_coeff n * b^n) + \ * of_real (sin_coeff n * b^n)"  wenzelm@63569  811  for n :: nat  wenzelm@63569  812  proof -  hoelzl@56889  813  have "\ ^ n = fact n *\<^sub>R (cos_coeff n + \ * sin_coeff n)"  hoelzl@56889  814  by (induct n)  wenzelm@63569  815  (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps  wenzelm@63569  816  power2_eq_square add_nonneg_eq_0_iff)  wenzelm@63569  817  then show ?thesis  wenzelm@63569  818  by (simp add: field_simps)  wenzelm@63569  819  qed  wenzelm@63569  820  then show ?thesis  wenzelm@63569  821  using sin_converges [of b] cos_converges [of b]  hoelzl@56889  822  by (auto simp add: cis.ctr exp_def simp del: of_real_mult  wenzelm@63569  823  intro!: sums_unique sums_add sums_mult sums_of_real)  huffman@44291  824 qed  huffman@44291  825 lp15@61762  826 lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"  wenzelm@63569  827  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp  wenzelm@63569  828  by (cases z) simp  huffman@20557  829 huffman@44828  830 lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"  lp15@61762  831  unfolding exp_eq_polar by simp  huffman@44828  832 huffman@44828  833 lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"  lp15@61762  834  unfolding exp_eq_polar by simp  huffman@44828  835 lp15@59746  836 lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"  lp15@59746  837  by (simp add: norm_complex_def)  lp15@59746  838 lp15@59746  839 lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"  lp15@61762  840  by (simp add: cis.code cmod_complex_polar exp_eq_polar)  lp15@59746  841 lp15@61762  842 lemma complex_exp_exists: "\a r. z = complex_of_real r * exp a"  lp15@59746  843  apply (insert rcis_Ex [of z])  lp15@61762  844  apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric])  wenzelm@63569  845  apply (rule_tac x = "\ * complex_of_real a" in exI)  wenzelm@63569  846  apply auto  lp15@59746  847  done  paulson@14323  848 wenzelm@63569  849 lemma exp_pi_i [simp]: "exp (of_real pi *$$ = -1"  lp15@61848  850  by (metis cis_conv_exp cis_pi mult.commute)  lp15@61848  851 wenzelm@63569  852 lemma exp_pi_i' [simp]: "exp (\ * of_real pi) = -1"  lp15@63114  853  using cis_conv_exp cis_pi by auto  lp15@63114  854 wenzelm@63569  855 lemma exp_two_pi_i [simp]: "exp (2 * of_real pi * \) = 1"  lp15@61762  856  by (simp add: exp_eq_polar complex_eq_iff)  paulson@14387  857 lp15@63114  858 lemma exp_two_pi_i' [simp]: "exp (\ * (of_real pi * 2)) = 1"  lp15@63114  859  by (metis exp_two_pi_i mult.commute)  lp15@63114  860 wenzelm@63569  861 wenzelm@60758  862 subsubsection \Complex argument\  huffman@44844  863 wenzelm@63569  864 definition arg :: "complex \ real"  wenzelm@63569  865  where "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \ - pi < a \ a \ pi))"  huffman@44844  866 huffman@44844  867 lemma arg_zero: "arg 0 = 0"  huffman@44844  868  by (simp add: arg_def)  huffman@44844  869 huffman@44844  870 lemma arg_unique:  huffman@44844  871  assumes "sgn z = cis x" and "-pi < x" and "x \ pi"  huffman@44844  872  shows "arg z = x"  huffman@44844  873 proof -  huffman@44844  874  from assms have "z \ 0" by auto  huffman@44844  875  have "(SOME a. sgn z = cis a \ -pi < a \ a \ pi) = x"  huffman@44844  876  proof  wenzelm@63040  877  fix a  wenzelm@63040  878  define d where "d = a - x"  huffman@44844  879  assume a: "sgn z = cis a \ - pi < a \ a \ pi"  huffman@44844  880  from a assms have "- (2*pi) < d \ d < 2*pi"  huffman@44844  881  unfolding d_def by simp  wenzelm@63569  882  moreover  wenzelm@63569  883  from a assms have "cos a = cos x" and "sin a = sin x"  huffman@44844  884  by (simp_all add: complex_eq_iff)  wenzelm@63569  885  then have cos: "cos d = 1"  wenzelm@63569  886  by (simp add: d_def cos_diff)  wenzelm@63569  887  moreover from cos have "sin d = 0"  wenzelm@63569  888  by (rule cos_one_sin_zero)  huffman@44844  889  ultimately have "d = 0"  wenzelm@63569  890  by (auto simp: sin_zero_iff elim!: evenE dest!: less_2_cases)  wenzelm@63569  891  then show "a = x"  wenzelm@63569  892  by (simp add: d_def)  huffman@44844  893  qed (simp add: assms del: Re_sgn Im_sgn)  wenzelm@60758  894  with \z \ 0\ show "arg z = x"  wenzelm@63569  895  by (simp add: arg_def)  huffman@44844  896 qed  huffman@44844  897 huffman@44844  898 lemma arg_correct:  wenzelm@63569  899  assumes "z \ 0"  wenzelm@63569  900  shows "sgn z = cis (arg z) \ -pi < arg z \ arg z \ pi"  huffman@44844  901 proof (simp add: arg_def assms, rule someI_ex)  wenzelm@63569  902  obtain r a where z: "z = rcis r a"  wenzelm@63569  903  using rcis_Ex by fast  huffman@44844  904  with assms have "r \ 0" by auto  wenzelm@63040  905  define b where "b = (if 0 < r then a else a + pi)"  huffman@44844  906  have b: "sgn z = cis b"  wenzelm@63569  907  using \r \ 0\ by (simp add: z b_def rcis_def of_real_def sgn_scaleR sgn_if complex_eq_iff)  wenzelm@63569  908  have cis_2pi_nat: "cis (2 * pi * real_of_nat n) = 1" for n  wenzelm@63569  909  by (induct n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)  wenzelm@63569  910  have cis_2pi_int: "cis (2 * pi * real_of_int x) = 1" for x  wenzelm@63569  911  by (cases x rule: int_diff_cases)  wenzelm@63569  912  (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)  wenzelm@63040  913  define c where "c = b - 2 * pi * of_int $$b - pi) / (2 * pi)\"  huffman@44844  914  have "sgn z = cis c"  wenzelm@63569  915  by (simp add: b c_def cis_divide [symmetric] cis_2pi_int)  huffman@44844  916  moreover have "- pi < c \ c \ pi"  huffman@44844  917  using ceiling_correct [of "(b - pi) / (2*pi)"]  lp15@61649  918  by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)  wenzelm@63569  919  ultimately show "\a. sgn z = cis a \ -pi < a \ a \ pi"  wenzelm@63569  920  by fast  huffman@44844  921 qed  huffman@44844  922 huffman@44844  923 lemma arg_bounded: "- pi < arg z \ arg z \ pi"  hoelzl@56889  924  by (cases "z = 0") (simp_all add: arg_zero arg_correct)  huffman@44844  925 huffman@44844  926 lemma cis_arg: "z \ 0 \ cis (arg z) = sgn z"  huffman@44844  927  by (simp add: arg_correct)  huffman@44844  928 huffman@44844  929 lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"  hoelzl@56889  930  by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)  hoelzl@56889  931 hoelzl@56889  932 lemma cos_arg_i_mult_zero [simp]: "y \ 0 \ Re y = 0 \ cos (arg y) = 0"  hoelzl@56889  933  using cis_arg [of y] by (simp add: complex_eq_iff)  hoelzl@56889  934 wenzelm@63569  935 wenzelm@60758  936 subsection \Square root of complex numbers\  hoelzl@56889  937 wenzelm@63569  938 primcorec csqrt :: "complex \ complex"  wenzelm@63569  939  where  wenzelm@63569  940  "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"  wenzelm@63569  941  | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"  hoelzl@56889  942 hoelzl@56889  943 lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = sqrt (Re x)"  hoelzl@56889  944  by (simp add: complex_eq_iff norm_complex_def)  hoelzl@56889  945 hoelzl@56889  946 lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\"  hoelzl@56889  947  by (simp add: complex_eq_iff norm_complex_def)  hoelzl@56889  948 lp15@59862  949 lemma of_real_sqrt: "x \ 0 \ of_real (sqrt x) = csqrt (of_real x)"  lp15@59862  950  by (simp add: complex_eq_iff norm_complex_def)  lp15@59862  951 hoelzl@56889  952 lemma csqrt_0 [simp]: "csqrt 0 = 0"  hoelzl@56889  953  by simp  hoelzl@56889  954 hoelzl@56889  955 lemma csqrt_1 [simp]: "csqrt 1 = 1"  hoelzl@56889  956  by simp  hoelzl@56889  957 hoelzl@56889  958 lemma csqrt_ii [simp]: "csqrt \ = (1 +$$ / sqrt 2"  hoelzl@56889  959  by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)  huffman@44844  960 lp15@59741  961 lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"  wenzelm@63569  962 proof (cases "Im z = 0")  wenzelm@63569  963  case True  wenzelm@63569  964  then show ?thesis  hoelzl@56889  965  using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]  hoelzl@56889  966  by (cases "0::real" "Re z" rule: linorder_cases)  wenzelm@63569  967  (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)  hoelzl@56889  968 next  wenzelm@63569  969  case False  wenzelm@63569  970  moreover have "cmod z * cmod z - Re z * Re z = Im z * Im z"  hoelzl@56889  971  by (simp add: norm_complex_def power2_eq_square)  wenzelm@63569  972  moreover have "\Re z\ \ cmod z"  hoelzl@56889  973  by (simp add: norm_complex_def)  hoelzl@56889  974  ultimately show ?thesis  hoelzl@56889  975  by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq  wenzelm@63569  976  field_simps real_sqrt_mult[symmetric] real_sqrt_divide)  hoelzl@56889  977 qed  hoelzl@56889  978 hoelzl@56889  979 lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0"  hoelzl@56889  980  by auto (metis power2_csqrt power_eq_0_iff)  hoelzl@56889  981 hoelzl@56889  982 lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1"  hoelzl@56889  983  by auto (metis power2_csqrt power2_eq_1_iff)  hoelzl@56889  984 hoelzl@56889  985 lemma csqrt_principal: "0 < Re (csqrt z) \ Re (csqrt z) = 0 \ 0 \ Im (csqrt z)"  hoelzl@56889  986  by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0)  hoelzl@56889  987 hoelzl@56889  988 lemma Re_csqrt: "0 \ Re (csqrt z)"  hoelzl@56889  989  by (metis csqrt_principal le_less)  hoelzl@56889  990 hoelzl@56889  991 lemma csqrt_square:  hoelzl@56889  992  assumes "0 < Re b \ (Re b = 0 \ 0 \ Im b)"  hoelzl@56889  993  shows "csqrt (b^2) = b"  hoelzl@56889  994 proof -  hoelzl@56889  995  have "csqrt (b^2) = b \ csqrt (b^2) = - b"  wenzelm@63569  996  by (simp add: power2_eq_iff[symmetric])  hoelzl@56889  997  moreover have "csqrt (b^2) \ -b \ b = 0"  wenzelm@63569  998  using csqrt_principal[of "b ^ 2"] assms  wenzelm@63569  999  by (intro disjCI notI) (auto simp: complex_eq_iff)  hoelzl@56889  1000  ultimately show ?thesis  hoelzl@56889  1001  by auto  hoelzl@56889  1002 qed  hoelzl@56889  1003 wenzelm@63569  1004 lemma csqrt_unique: "w\<^sup>2 = z \ 0 < Re w \ Re w = 0 \ 0 \ Im w \ csqrt z = w"  lp15@59746  1005  by (auto simp: csqrt_square)  lp15@59746  1006 lp15@59613  1007 lemma csqrt_minus [simp]:  hoelzl@56889  1008  assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)"  hoelzl@56889  1009  shows "csqrt (- x) = \ * csqrt x"  hoelzl@56889  1010 proof -  hoelzl@56889  1011  have "csqrt ((\ * csqrt x)^2) = \ * csqrt x"  hoelzl@56889  1012  proof (rule csqrt_square)  hoelzl@56889  1013  have "Im (csqrt x) \ 0"  hoelzl@56889  1014  using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod)  hoelzl@56889  1015  then show "0 < Re (\ * csqrt x) \ Re (\ * csqrt x) = 0 \ 0 \ Im (\ * csqrt x)"  hoelzl@56889  1016  by (auto simp add: Re_csqrt simp del: csqrt.simps)  hoelzl@56889  1017  qed  hoelzl@56889  1018  also have "(\ * csqrt x)^2 = - x"  lp15@59746  1019  by (simp add: power_mult_distrib)  hoelzl@56889  1020  finally show ?thesis .  hoelzl@56889  1021 qed  huffman@44844  1022 wenzelm@63569  1023 wenzelm@60758  1024 text \Legacy theorem names\  huffman@44065  1025 huffman@44065  1026 lemmas expand_complex_eq = complex_eq_iff  huffman@44065  1027 lemmas complex_Re_Im_cancel_iff = complex_eq_iff  huffman@44065  1028 lemmas complex_equality = complex_eqI  hoelzl@56889  1029 lemmas cmod_def = norm_complex_def  hoelzl@56889  1030 lemmas complex_norm_def = norm_complex_def  hoelzl@56889  1031 lemmas complex_divide_def = divide_complex_def  hoelzl@56889  1032 hoelzl@56889  1033 lemma legacy_Complex_simps:  hoelzl@56889  1034  shows Complex_eq_0: "Complex a b = 0 \ a = 0 \ b = 0"  hoelzl@56889  1035  and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)"  hoelzl@56889  1036  and complex_minus: "- (Complex a b) = Complex (- a) (- b)"  hoelzl@56889  1037  and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)"  hoelzl@56889  1038  and Complex_eq_1: "Complex a b = 1 \ a = 1 \ b = 0"  hoelzl@56889  1039  and Complex_eq_neg_1: "Complex a b = - 1 \ a = - 1 \ b = 0"  hoelzl@56889  1040  and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)"  hoelzl@56889  1041  and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"  hoelzl@56889  1042  and Complex_eq_numeral: "Complex a b = numeral w \ a = numeral w \ b = 0"  hoelzl@56889  1043  and Complex_eq_neg_numeral: "Complex a b = - numeral w \ a = - numeral w \ b = 0"  hoelzl@56889  1044  and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)"  wenzelm@63569  1045  and Complex_eq_i: "Complex x y = \ \ x = 0 \ y = 1"  wenzelm@63569  1046  and i_mult_Complex: "\ * Complex a b = Complex (- b) a"  wenzelm@63569  1047  and Complex_mult_i: "Complex a b * \ = Complex (- b) a"  wenzelm@63569  1048  and i_complex_of_real: "\ * complex_of_real r = Complex 0 r"  wenzelm@63569  1049  and complex_of_real_i: "complex_of_real r * \ = Complex 0 r"  hoelzl@56889  1050  and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y"  hoelzl@56889  1051  and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y"  hoelzl@56889  1052  and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"  hoelzl@56889  1053  and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"  wenzelm@63569  1054  and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \ y = 0)"  hoelzl@56889  1055  and complex_cn: "cnj (Complex a b) = Complex a (- b)"  nipkow@64267  1056  and Complex_sum': "sum (\x. Complex (f x) 0) s = Complex (sum f s) 0"  nipkow@64267  1057  and Complex_sum: "Complex (sum f s) 0 = sum (\x. Complex (f x) 0) s"  hoelzl@56889  1058  and complex_of_real_def: "complex_of_real r = Complex r 0"  hoelzl@56889  1059  and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"  hoelzl@56889  1060  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq)  hoelzl@56889  1061 hoelzl@56889  1062 lemma Complex_in_Reals: "Complex x 0 \ \"  hoelzl@56889  1063  by (metis Reals_of_real complex_of_real_def)  huffman@44065  1064 paulson@13957  1065 end