src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 55734 3f5b2745d659
parent 55358 85d81bc281d0
child 55735 81ba62493610
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 15:02:54 2014 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 16:17:20 2014 +0000
     1.3 @@ -7,6 +7,7 @@
     1.4  begin
     1.5  
     1.6  subsection {* Square root of complex numbers *}
     1.7 +
     1.8  definition csqrt :: "complex \<Rightarrow> complex" where
     1.9  "csqrt z = (if Im z = 0 then
    1.10              if 0 \<le> Re z then Complex (sqrt(Re z)) 0
    1.11 @@ -54,6 +55,39 @@
    1.12    ultimately show ?thesis by blast
    1.13  qed
    1.14  
    1.15 +lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
    1.16 +  by (simp add: csqrt_def)
    1.17 +
    1.18 +lemma csqrt_0 [simp]: "csqrt 0 = 0"
    1.19 +  by (simp add: csqrt_def)
    1.20 +
    1.21 +lemma csqrt_1 [simp]: "csqrt 1 = 1"
    1.22 +  by (simp add: csqrt_def)
    1.23 +
    1.24 +lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
    1.25 +proof (cases z)
    1.26 +  case (Complex x y)
    1.27 +  then show ?thesis
    1.28 +    using real_sqrt_sum_squares_ge1 [of "x" y]
    1.29 +          real_sqrt_sum_squares_ge1 [of "-x" y]
    1.30 +          real_sqrt_sum_squares_eq_cancel [of x y]
    1.31 +    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
    1.32 +    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
    1.33 +    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
    1.34 +qed
    1.35 +
    1.36 +lemma Re_csqrt: "0 \<le> Re(csqrt z)"
    1.37 +  by (metis csqrt_principal le_less)
    1.38 +
    1.39 +lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
    1.40 +  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
    1.41 +  by (cases z) (auto simp: power2_eq_iff)
    1.42 +
    1.43 +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
    1.44 +  by auto (metis csqrt power_eq_0_iff)
    1.45 +
    1.46 +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
    1.47 +  by auto (metis csqrt power2_eq_1_iff)
    1.48  
    1.49  subsection{* More lemmas about module of complex numbers *}
    1.50