src/HOL/Complex.thy
changeset 60758 d8d85a8172b5
parent 60429 d3d1e185cd63
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Complex.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Complex.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -4,17 +4,17 @@
     1.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     1.5  *)
     1.6  
     1.7 -section {* Complex Numbers: Rectangular and Polar Representations *}
     1.8 +section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
     1.9  
    1.10  theory Complex
    1.11  imports Transcendental
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16  We use the @{text codatatype} command to define the type of complex numbers. This allows us to use
    1.17  @{text primcorec} to define complex functions by defining their real and imaginary result
    1.18  separately.
    1.19 -*}
    1.20 +\<close>
    1.21  
    1.22  codatatype complex = Complex (Re: real) (Im: real)
    1.23  
    1.24 @@ -27,7 +27,7 @@
    1.25  lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
    1.26    by (auto intro: complex.expand)
    1.27  
    1.28 -subsection {* Addition and Subtraction *}
    1.29 +subsection \<open>Addition and Subtraction\<close>
    1.30  
    1.31  instantiation complex :: ab_group_add
    1.32  begin
    1.33 @@ -53,7 +53,7 @@
    1.34  
    1.35  end
    1.36  
    1.37 -subsection {* Multiplication and Division *}
    1.38 +subsection \<open>Multiplication and Division\<close>
    1.39  
    1.40  instantiation complex :: field
    1.41  begin
    1.42 @@ -99,7 +99,7 @@
    1.43  lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
    1.44    by (induct n) simp_all
    1.45  
    1.46 -subsection {* Scalar Multiplication *}
    1.47 +subsection \<open>Scalar Multiplication\<close>
    1.48  
    1.49  instantiation complex :: real_field
    1.50  begin
    1.51 @@ -127,7 +127,7 @@
    1.52  
    1.53  end
    1.54  
    1.55 -subsection {* Numerals, Arithmetic, and Embedding from Reals *}
    1.56 +subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
    1.57  
    1.58  abbreviation complex_of_real :: "real \<Rightarrow> complex"
    1.59    where "complex_of_real \<equiv> of_real"
    1.60 @@ -171,7 +171,7 @@
    1.61      "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
    1.62    by (auto simp: Reals_def)
    1.63  
    1.64 -subsection {* The Complex Number $i$ *}
    1.65 +subsection \<open>The Complex Number $i$\<close>
    1.66  
    1.67  primcorec "ii" :: complex  ("\<i>") where
    1.68    "Re ii = 0"
    1.69 @@ -231,7 +231,7 @@
    1.70  lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
    1.71    by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
    1.72  
    1.73 -subsection {* Vector Norm *}
    1.74 +subsection \<open>Vector Norm\<close>
    1.75  
    1.76  instantiation complex :: real_normed_field
    1.77  begin
    1.78 @@ -329,7 +329,7 @@
    1.79    by (simp add: norm_complex_def divide_simps complex_eq_iff)
    1.80  
    1.81  
    1.82 -text {* Properties of complex signum. *}
    1.83 +text \<open>Properties of complex signum.\<close>
    1.84  
    1.85  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    1.86    by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult.commute)
    1.87 @@ -341,7 +341,7 @@
    1.88    by (simp add: complex_sgn_def divide_inverse)
    1.89  
    1.90  
    1.91 -subsection {* Completeness of the Complexes *}
    1.92 +subsection \<open>Completeness of the Complexes\<close>
    1.93  
    1.94  lemma bounded_linear_Re: "bounded_linear Re"
    1.95    by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
    1.96 @@ -407,7 +407,7 @@
    1.97  declare
    1.98    DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
    1.99  
   1.100 -subsection {* Complex Conjugation *}
   1.101 +subsection \<open>Complex Conjugation\<close>
   1.102  
   1.103  primcorec cnj :: "complex \<Rightarrow> complex" where
   1.104    "Re (cnj z) = Re z"
   1.105 @@ -514,7 +514,7 @@
   1.106    by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum)
   1.107  
   1.108  
   1.109 -subsection{*Basic Lemmas*}
   1.110 +subsection\<open>Basic Lemmas\<close>
   1.111  
   1.112  lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
   1.113    by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
   1.114 @@ -616,13 +616,13 @@
   1.115      done
   1.116  qed
   1.117  
   1.118 -subsection{*Polar Form for Complex Numbers*}
   1.119 +subsection\<open>Polar Form for Complex Numbers\<close>
   1.120  
   1.121  lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
   1.122    using sincos_total_2pi [of "Re z" "Im z"]
   1.123    by auto (metis cmod_power2 complex_eq power_one)
   1.124  
   1.125 -subsubsection {* $\cos \theta + i \sin \theta$ *}
   1.126 +subsubsection \<open>$\cos \theta + i \sin \theta$\<close>
   1.127  
   1.128  primcorec cis :: "real \<Rightarrow> complex" where
   1.129    "Re (cis a) = cos a"
   1.130 @@ -661,7 +661,7 @@
   1.131  lemma cis_pi: "cis pi = -1"
   1.132    by (simp add: complex_eq_iff)
   1.133  
   1.134 -subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
   1.135 +subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
   1.136  
   1.137  definition rcis :: "real \<Rightarrow> real \<Rightarrow> complex" where
   1.138    "rcis r a = complex_of_real r * cis a"
   1.139 @@ -702,7 +702,7 @@
   1.140  lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
   1.141    by (simp add: rcis_def cis_divide [symmetric])
   1.142  
   1.143 -subsubsection {* Complex exponential *}
   1.144 +subsubsection \<open>Complex exponential\<close>
   1.145  
   1.146  abbreviation Exp :: "complex \<Rightarrow> complex"
   1.147    where "Exp \<equiv> exp"
   1.148 @@ -747,7 +747,7 @@
   1.149  lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
   1.150    by (simp add: Exp_eq_polar complex_eq_iff)
   1.151  
   1.152 -subsubsection {* Complex argument *}
   1.153 +subsubsection \<open>Complex argument\<close>
   1.154  
   1.155  definition arg :: "complex \<Rightarrow> real" where
   1.156    "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi))"
   1.157 @@ -775,7 +775,7 @@
   1.158        by (auto elim!: evenE dest!: less_2_cases)
   1.159      thus "a = x" unfolding d_def by simp
   1.160    qed (simp add: assms del: Re_sgn Im_sgn)
   1.161 -  with `z \<noteq> 0` show "arg z = x"
   1.162 +  with \<open>z \<noteq> 0\<close> show "arg z = x"
   1.163      unfolding arg_def by simp
   1.164  qed
   1.165  
   1.166 @@ -786,7 +786,7 @@
   1.167    with assms have "r \<noteq> 0" by auto
   1.168    def b \<equiv> "if 0 < r then a else a + pi"
   1.169    have b: "sgn z = cis b"
   1.170 -    unfolding z b_def rcis_def using `r \<noteq> 0`
   1.171 +    unfolding z b_def rcis_def using \<open>r \<noteq> 0\<close>
   1.172      by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
   1.173    have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
   1.174      by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
   1.175 @@ -815,7 +815,7 @@
   1.176  lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
   1.177    using cis_arg [of y] by (simp add: complex_eq_iff)
   1.178  
   1.179 -subsection {* Square root of complex numbers *}
   1.180 +subsection \<open>Square root of complex numbers\<close>
   1.181  
   1.182  primcorec csqrt :: "complex \<Rightarrow> complex" where
   1.183    "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
   1.184 @@ -902,7 +902,7 @@
   1.185    finally show ?thesis .
   1.186  qed
   1.187  
   1.188 -text {* Legacy theorem names *}
   1.189 +text \<open>Legacy theorem names\<close>
   1.190  
   1.191  lemmas expand_complex_eq = complex_eq_iff
   1.192  lemmas complex_Re_Im_cancel_iff = complex_eq_iff