src/HOL/Complex.thy

     Author:      Jacques D. Fleuriot
     Copyright:   2001 University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
 *)
 
-section {* Complex Numbers: Rectangular and Polar Representations *}
+section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
 
 theory Complex
 imports Transcendental
 begin
 
-text {*
+text \<open>
 We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
 @{text primcorec} to define complex functions by defining their real and imaginary result
 separately.
-*}
+\<close>
 
 codatatype complex = Complex (Re: real) (Im: real)
 
 lemma complex_surj: "Complex (Re z) (Im z) = z"
   by (rule complex.collapse)

   by (rule complex.expand) simp
 
 lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
   by (auto intro: complex.expand)
 
-subsection {* Addition and Subtraction *}
+subsection \<open>Addition and Subtraction\<close>
 
 instantiation complex :: ab_group_add
 begin
 
 primcorec zero_complex where

 instance
   by intro_classes (simp_all add: complex_eq_iff)
 
 end
 
-subsection {* Multiplication and Division *}
+subsection \<open>Multiplication and Division\<close>
 
 instantiation complex :: field
 begin
 
 primcorec one_complex where

   by (induct n) simp_all
 
 lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
   by (induct n) simp_all
 
-subsection {* Scalar Multiplication *}
+subsection \<open>Scalar Multiplication\<close>
 
 instantiation complex :: real_field
 begin
 
 primcorec scaleR_complex where

     by (simp add: complex_eq_iff algebra_simps)
 qed
 
 end
 
-subsection {* Numerals, Arithmetic, and Embedding from Reals *}
+subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
 
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
 
 declare [[coercion "of_real :: real \<Rightarrow> complex"]]

 
 lemma of_real_Re [simp]:
     "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
   by (auto simp: Reals_def)
 
-subsection {* The Complex Number $i$ *}
+subsection \<open>The Complex Number $i$\<close>
 
 primcorec "ii" :: complex  ("\<i>") where
   "Re ii = 0"
 | "Im ii = 1"
 

   by auto
 
 lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
   by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
 
-subsection {* Vector Norm *}
+subsection \<open>Vector Norm\<close>
 
 instantiation complex :: real_normed_field
 begin
 
 definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"

 
 lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
   by (simp add: norm_complex_def divide_simps complex_eq_iff)
 
 
-text {* Properties of complex signum. *}
+text \<open>Properties of complex signum.\<close>
 
 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
   by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)
 
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"

 
 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
   by (simp add: complex_sgn_def divide_inverse)
 
 
-subsection {* Completeness of the Complexes *}
+subsection \<open>Completeness of the Complexes\<close>
 
 lemma bounded_linear_Re: "bounded_linear Re"
   by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
 
 lemma bounded_linear_Im: "bounded_linear Im"

 qed
 
 declare
   DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
 
-subsection {* Complex Conjugation *}
+subsection \<open>Complex Conjugation\<close>
 
 primcorec cnj :: "complex \<Rightarrow> complex" where
   "Re (cnj z) = Re z"
 | "Im (cnj z) = - Im z"
 

 
 lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
   by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum)
 
 
-subsection{*Basic Lemmas*}
+subsection\<open>Basic Lemmas\<close>
 
 lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
   by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
 
 lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"

     apply (auto simp: g sums_Re)
     apply (metis fg g)
     done
 qed
 
-subsection{*Polar Form for Complex Numbers*}
+subsection\<open>Polar Form for Complex Numbers\<close>
 
 lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
   using sincos_total_2pi [of "Re z" "Im z"]
   by auto (metis cmod_power2 complex_eq power_one)
 
-subsubsection {* $\cos \theta + i \sin \theta$ *}
+subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
 
 primcorec cis :: "real \<Rightarrow> complex" where
   "Re (cis a) = cos a"
 | "Im (cis a) = sin a"
 

   by (auto simp add: DeMoivre)
 
 lemma cis_pi: "cis pi = -1"
   by (simp add: complex_eq_iff)
 
-subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
+subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
 
 definition rcis :: "real \<Rightarrow> 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: divide_inverse rcis_def)
 
 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
   by (simp add: rcis_def cis_divide [symmetric])
 
-subsubsection {* Complex exponential *}
+subsubsection \<open>Complex exponential\<close>
 
 abbreviation Exp :: "complex \<Rightarrow> complex"
   where "Exp \<equiv> exp"
 
 lemma cis_conv_exp: "cis b = exp (\<i> * b)"

   done
 
 lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
   by (simp add: Exp_eq_polar complex_eq_iff)
 
-subsubsection {* Complex argument *}
+subsubsection \<open>Complex argument\<close>
 
 definition arg :: "complex \<Rightarrow> real" where
   "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi))"
 
 lemma arg_zero: "arg 0 = 0"

     ultimately have "d = 0"
       unfolding sin_zero_iff
       by (auto elim!: evenE dest!: less_2_cases)
     thus "a = x" unfolding d_def by simp
   qed (simp add: assms del: Re_sgn Im_sgn)
-  with `z \<noteq> 0` show "arg z = x"
+  with \<open>z \<noteq> 0\<close> show "arg z = x"
     unfolding arg_def by simp
 qed
 
 lemma arg_correct:
   assumes "z \<noteq> 0" shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
 proof (simp add: arg_def assms, rule someI_ex)
   obtain r a where z: "z = rcis r a" using rcis_Ex by fast
   with assms have "r \<noteq> 0" by auto
   def b \<equiv> "if 0 < r then a else a + pi"
   have b: "sgn z = cis b"
-    unfolding z b_def rcis_def using `r \<noteq> 0`
+    unfolding z b_def rcis_def using \<open>r \<noteq> 0\<close>
     by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
   have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
     by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
   have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
     by (case_tac x rule: int_diff_cases)

   by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
 
 lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
   using cis_arg [of y] by (simp add: complex_eq_iff)
 
-subsection {* Square root of complex numbers *}
+subsection \<open>Square root of complex numbers\<close>
 
 primcorec csqrt :: "complex \<Rightarrow> complex" where
   "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
 | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"
 

   also have "(\<i> * csqrt x)^2 = - x"
     by (simp add: power_mult_distrib)
   finally show ?thesis .
 qed
 
-text {* Legacy theorem names *}
+text \<open>Legacy theorem names\<close>
 
 lemmas expand_complex_eq = complex_eq_iff
 lemmas complex_Re_Im_cancel_iff = complex_eq_iff
 lemmas complex_equality = complex_eqI
 lemmas cmod_def = norm_complex_def