src/HOL/Complex.thy
changeset 59741 5b762cd73a8e
parent 59658 0cc388370041
child 59746 ddae5727c5a9
     1.1 --- a/src/HOL/Complex.thy	Tue Mar 17 17:45:03 2015 +0000
     1.2 +++ b/src/HOL/Complex.thy	Wed Mar 18 14:13:27 2015 +0000
     1.3 @@ -215,6 +215,18 @@
     1.4  lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
     1.5    by (metis mult.commute power2_i power_mult)
     1.6  
     1.7 +lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
     1.8 +  by simp
     1.9 +
    1.10 +lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
    1.11 +  by simp
    1.12 +
    1.13 +lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
    1.14 +  by auto
    1.15 +
    1.16 +lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
    1.17 +  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
    1.18 +
    1.19  subsection {* Vector Norm *}
    1.20  
    1.21  instantiation complex :: real_normed_field
    1.22 @@ -309,6 +321,9 @@
    1.23    apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
    1.24    done
    1.25  
    1.26 +lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
    1.27 +  by (simp add: norm_complex_def divide_simps complex_eq_iff)
    1.28 +
    1.29  
    1.30  text {* Properties of complex signum. *}
    1.31  
    1.32 @@ -508,10 +523,10 @@
    1.33     (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
    1.34           simp del: of_real_power)
    1.35  
    1.36 -lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    1.37 +lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    1.38    by (auto simp add: Re_divide)
    1.39  
    1.40 -lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
    1.41 +lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
    1.42    by (auto simp add: Im_divide)
    1.43  
    1.44  lemma complex_div_gt_0:
    1.45 @@ -526,27 +541,27 @@
    1.46      by (simp add: Re_divide Im_divide zero_less_divide_iff)
    1.47  qed
    1.48  
    1.49 -lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
    1.50 -  and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
    1.51 +lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
    1.52 +  and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
    1.53    using complex_div_gt_0 by auto
    1.54  
    1.55 -lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
    1.56 -  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
    1.57 +lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
    1.58 +  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
    1.59  
    1.60 -lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
    1.61 -  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
    1.62 +lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
    1.63 +  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
    1.64  
    1.65 -lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
    1.66 -  by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
    1.67 +lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
    1.68 +  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
    1.69  
    1.70 -lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
    1.71 -  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
    1.72 +lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
    1.73 +  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
    1.74  
    1.75 -lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
    1.76 -  by (metis not_le re_complex_div_gt_0)
    1.77 +lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
    1.78 +  by (metis not_le Re_complex_div_gt_0)
    1.79  
    1.80 -lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
    1.81 -  by (metis im_complex_div_gt_0 not_le)
    1.82 +lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
    1.83 +  by (metis Im_complex_div_gt_0 not_le)
    1.84  
    1.85  lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
    1.86    by (induct s rule: infinite_finite_induct) auto
    1.87 @@ -807,7 +822,7 @@
    1.88  lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
    1.89    by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
    1.90  
    1.91 -lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
    1.92 +lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
    1.93  proof cases
    1.94    assume "Im z = 0" then show ?thesis
    1.95      using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]