More complex-related lemmas
authorpaulson <lp15@cam.ac.uk>
Tue Feb 25 16:17:20 2014 +0000 (2014-02-25)
changeset 557343f5b2745d659
parent 55733 e6edd47f1483
child 55735 81ba62493610
More complex-related lemmas
src/HOL/Complex.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     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.32 +    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
    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))"