author paulson Tue Feb 25 16:17:20 2014 +0000 (2014-02-25) changeset 55734 3f5b2745d659 parent 55733 e6edd47f1483 child 55735 81ba62493610
More complex-related lemmas
 src/HOL/Complex.thy file | annotate | diff | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Complex.thy	Tue Feb 25 15:02:54 2014 +0100
1.2 +++ b/src/HOL/Complex.thy	Tue Feb 25 16:17:20 2014 +0000
1.3 @@ -557,6 +557,109 @@
1.4    bounded_linear.isCont [OF bounded_linear_cnj]
1.5
1.6
1.7 +subsection{*Basic Lemmas*}
1.8 +
1.9 +lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
1.10 +  by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff)
1.11 +
1.12 +lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
1.13 +by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
1.14 +
1.15 +lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
1.16 +apply (cases z, auto)
1.17 +by (metis complex_of_real_def of_real_add of_real_power power2_eq_square)
1.18 +
1.19 +lemma complex_div_eq_0:
1.20 +    "(Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0) & (Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0)"
1.21 +proof (cases "b=0")
1.22 +  case True then show ?thesis by auto
1.23 +next
1.24 +  case False
1.25 +  show ?thesis
1.26 +  proof (cases b)
1.27 +    case (Complex x y)
1.28 +    then have "x\<^sup>2 + y\<^sup>2 > 0"
1.29 +      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
1.30 +    then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
1.31 +      by (metis add_divide_distrib)
1.32 +    with Complex False show ?thesis
1.33 +      by (auto simp: complex_divide_def)
1.34 +  qed
1.35 +qed
1.36 +
1.37 +lemma re_complex_div_eq_0: "Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0"
1.38 +  and im_complex_div_eq_0: "Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0"
1.39 +using complex_div_eq_0 by auto
1.40 +
1.41 +
1.42 +lemma complex_div_gt_0:
1.43 +    "(Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0) & (Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0)"
1.44 +proof (cases "b=0")
1.45 +  case True then show ?thesis by auto
1.46 +next
1.47 +  case False
1.48 +  show ?thesis
1.49 +  proof (cases b)
1.50 +    case (Complex x y)
1.51 +    then have "x\<^sup>2 + y\<^sup>2 > 0"
1.52 +      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
1.53 +    moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
1.54 +      by (metis add_divide_distrib)
1.55 +    ultimately show ?thesis using Complex False 0 < x\<^sup>2 + y\<^sup>2
1.56 +      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
1.57 +      apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
1.58 +      done
1.59 +  qed
1.60 +qed
1.61 +
1.62 +lemma re_complex_div_gt_0: "Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0"
1.63 +  and im_complex_div_gt_0: "Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0"
1.64 +using complex_div_gt_0 by auto
1.65 +
1.66 +lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
1.67 +  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
1.68 +
1.69 +lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
1.70 +  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
1.71 +
1.72 +lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
1.73 +  by (smt re_complex_div_eq_0 re_complex_div_gt_0)
1.74 +
1.75 +lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
1.76 +  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
1.77 +
1.78 +lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
1.79 +  by (metis not_le re_complex_div_gt_0)
1.80 +
1.81 +lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
1.82 +  by (metis im_complex_div_gt_0 not_le)
1.83 +
1.84 +lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
1.85 +  by (induct s rule: finite_induct) auto
1.86 +
1.87 +lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
1.88 +  by (induct s rule: finite_induct) auto
1.89 +
1.90 +lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
1.91 +  by (induct s rule: finite_induct) auto
1.92 +
1.93 +lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
1.94 +  by (metis Complex_setsum')
1.95 +
1.96 +lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
1.97 +  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
1.98 +
1.99 +lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
1.100 +by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj
1.101 +          complex_of_real_def equal_neg_zero)
1.102 +
1.103 +lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
1.104 +  by (metis Reals_of_real complex_of_real_def)
1.105 +
1.106 +lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
1.107 +  by (metis Re_complex_of_real Reals_cases norm_of_real)
1.108 +
1.109 +
1.110  subsection{*Finally! Polar Form for Complex Numbers*}
1.111
1.112  subsubsection {* $\cos \theta + i \sin \theta$ *}

     2.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 15:02:54 2014 +0100
2.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 16:17:20 2014 +0000
2.3 @@ -7,6 +7,7 @@
2.4  begin
2.5
2.6  subsection {* Square root of complex numbers *}
2.7 +
2.8  definition csqrt :: "complex \<Rightarrow> complex" where
2.9  "csqrt z = (if Im z = 0 then
2.10              if 0 \<le> Re z then Complex (sqrt(Re z)) 0
2.11 @@ -54,6 +55,39 @@
2.12    ultimately show ?thesis by blast
2.13  qed
2.14
2.15 +lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
2.16 +  by (simp add: csqrt_def)
2.17 +
2.18 +lemma csqrt_0 [simp]: "csqrt 0 = 0"
2.19 +  by (simp add: csqrt_def)
2.20 +
2.21 +lemma csqrt_1 [simp]: "csqrt 1 = 1"
2.22 +  by (simp add: csqrt_def)
2.23 +
2.24 +lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
2.25 +proof (cases z)
2.26 +  case (Complex x y)
2.27 +  then show ?thesis
2.28 +    using real_sqrt_sum_squares_ge1 [of "x" y]
2.29 +          real_sqrt_sum_squares_ge1 [of "-x" y]
2.30 +          real_sqrt_sum_squares_eq_cancel [of x y]
2.31 +    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
2.33 +    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
2.34 +qed
2.35 +
2.36 +lemma Re_csqrt: "0 \<le> Re(csqrt z)"
2.37 +  by (metis csqrt_principal le_less)
2.38 +
2.39 +lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
2.40 +  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
2.41 +  by (cases z) (auto simp: power2_eq_iff)
2.42 +
2.43 +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
2.44 +  by auto (metis csqrt power_eq_0_iff)
2.45 +
2.46 +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
2.47 +  by auto (metis csqrt power2_eq_1_iff)
2.48
2.49  subsection{* More lemmas about module of complex numbers *}
2.50

     3.1 --- a/src/HOL/Topological_Spaces.thy	Tue Feb 25 15:02:54 2014 +0100
3.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Feb 25 16:17:20 2014 +0000
3.3 @@ -1706,6 +1706,11 @@
3.4    unfolding continuous_on_open_invariant
3.5    by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
3.6
3.7 +corollary continuous_imp_open_vimage:
3.8 +  assumes "continuous_on s f" "open s" "open B" "f - B \<subseteq> s"
3.9 +    shows "open (f - B)"
3.10 +by (metis assms continuous_on_open_vimage le_iff_inf)
3.11 +
3.12  lemma continuous_on_closed_invariant:
3.13    "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f - B \<inter> s))"
3.14  proof -

     4.1 --- a/src/HOL/Transcendental.thy	Tue Feb 25 15:02:54 2014 +0100
4.2 +++ b/src/HOL/Transcendental.thy	Tue Feb 25 16:17:20 2014 +0000
4.3 @@ -52,6 +52,12 @@
4.4    finally show ?case .
4.5  qed
4.6
4.7 +corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
4.8 +  fixes x :: "'a::{comm_ring,monoid_mult}"
4.9 +  shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
4.10 +using lemma_realpow_diff_sumr2[of x "n - 1" y]
4.11 +by (cases "n = 0") (simp_all add: field_simps)
4.12 +
4.13  lemma lemma_realpow_rev_sumr:
4.14     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
4.15      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
`