# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1393345040 0
# Node ID 3f5b2745d65909eba25b512127b9b9b47be45c76
# Parent  e6edd47f14831af58d0f801c18d791f8563a0155
More complex-related lemmas

diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Feb 25 15:02:54 2014 +0100
+++ b/src/HOL/Complex.thy	Tue Feb 25 16:17:20 2014 +0000
@@ -557,6 +557,109 @@
   bounded_linear.isCont [OF bounded_linear_cnj]
 
 
+subsection{*Basic Lemmas*}
+
+lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
+  by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff)
+
+lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
+by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
+
+lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
+apply (cases z, auto)
+by (metis complex_of_real_def of_real_add of_real_power power2_eq_square)
+
+lemma complex_div_eq_0: 
+    "(Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0) & (Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0)"
+proof (cases "b=0")
+  case True then show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof (cases b)
+    case (Complex x y)
+    then have "x\<^sup>2 + y\<^sup>2 > 0"
+      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+    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)"
+      by (metis add_divide_distrib)
+    with Complex False show ?thesis
+      by (auto simp: complex_divide_def)
+  qed
+qed
+
+lemma re_complex_div_eq_0: "Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0"
+  and im_complex_div_eq_0: "Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0"
+using complex_div_eq_0 by auto
+
+
+lemma complex_div_gt_0: 
+    "(Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0) & (Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0)"
+proof (cases "b=0")
+  case True then show ?thesis by auto
+next
+  case False
+  show ?thesis
+  proof (cases b)
+    case (Complex x y)
+    then have "x\<^sup>2 + y\<^sup>2 > 0"
+      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
+    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)"
+      by (metis add_divide_distrib)
+    ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
+      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
+      apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
+      done
+  qed
+qed
+
+lemma re_complex_div_gt_0: "Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0"
+  and im_complex_div_gt_0: "Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0"
+using complex_div_gt_0 by auto
+
+lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+
+lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+  by (smt re_complex_div_eq_0 re_complex_div_gt_0)
+
+lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+
+lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+  by (metis not_le re_complex_div_gt_0)
+
+lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+  by (metis im_complex_div_gt_0 not_le)
+
+lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
+  by (induct s rule: finite_induct) auto
+
+lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
+  by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
+  by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
+  by (metis Complex_setsum')
+
+lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
+  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
+
+lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
+by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
+          complex_of_real_def equal_neg_zero)
+
+lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
+  by (metis Reals_of_real complex_of_real_def)
+
+lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
+  by (metis Re_complex_of_real Reals_cases norm_of_real)
+
+
 subsection{*Finally! Polar Form for Complex Numbers*}
 
 subsubsection {* $\cos \theta + i \sin \theta$ *}
diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 15:02:54 2014 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 16:17:20 2014 +0000
@@ -7,6 +7,7 @@
 begin
 
 subsection {* Square root of complex numbers *}
+
 definition csqrt :: "complex \<Rightarrow> complex" where
 "csqrt z = (if Im z = 0 then
             if 0 \<le> Re z then Complex (sqrt(Re z)) 0
@@ -54,6 +55,39 @@
   ultimately show ?thesis by blast
 qed
 
+lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
+  by (simp add: csqrt_def)
+
+lemma csqrt_0 [simp]: "csqrt 0 = 0"
+  by (simp add: csqrt_def)
+
+lemma csqrt_1 [simp]: "csqrt 1 = 1"
+  by (simp add: csqrt_def)
+
+lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
+proof (cases z)
+  case (Complex x y)
+  then show ?thesis
+    using real_sqrt_sum_squares_ge1 [of "x" y]
+          real_sqrt_sum_squares_ge1 [of "-x" y]
+          real_sqrt_sum_squares_eq_cancel [of x y]
+    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
+    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
+    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
+qed
+
+lemma Re_csqrt: "0 \<le> Re(csqrt z)"
+  by (metis csqrt_principal le_less)
+
+lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
+  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
+  by (cases z) (auto simp: power2_eq_iff)
+
+lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
+  by auto (metis csqrt power_eq_0_iff)
+
+lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
+  by auto (metis csqrt power2_eq_1_iff)
 
 subsection{* More lemmas about module of complex numbers *}
 
diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 25 15:02:54 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Feb 25 16:17:20 2014 +0000
@@ -1706,6 +1706,11 @@
   unfolding continuous_on_open_invariant
   by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
 
+corollary continuous_imp_open_vimage:
+  assumes "continuous_on s f" "open s" "open B" "f -` B \<subseteq> s"
+    shows "open (f -` B)"
+by (metis assms continuous_on_open_vimage le_iff_inf)
+
 lemma continuous_on_closed_invariant:
   "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
 proof -
diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Feb 25 15:02:54 2014 +0100
+++ b/src/HOL/Transcendental.thy	Tue Feb 25 16:17:20 2014 +0000
@@ -52,6 +52,12 @@
   finally show ?case .
 qed
 
+corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
+using lemma_realpow_diff_sumr2[of x "n - 1" y]
+by (cases "n = 0") (simp_all add: field_simps)
+
 lemma lemma_realpow_rev_sumr:
    "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
     (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"