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.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"]
```