--- 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$ *}
--- 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 *}
--- 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 -
--- 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))"