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.30
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.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