src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 56889 48a745e1bde7
parent 56795 e8cce2bd23e5
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue May 06 23:35:24 2014 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed May 07 12:25:35 2014 +0200
     1.3 @@ -6,126 +6,12 @@
     1.4  imports Polynomial Complex_Main
     1.5  begin
     1.6  
     1.7 -subsection {* Square root of complex numbers *}
     1.8 -
     1.9 -definition csqrt :: "complex \<Rightarrow> complex"
    1.10 -where
    1.11 -  "csqrt z =
    1.12 -    (if Im z = 0 then
    1.13 -       if 0 \<le> Re z then Complex (sqrt(Re z)) 0
    1.14 -       else Complex 0 (sqrt(- Re z))
    1.15 -     else Complex (sqrt((cmod z + Re z) /2)) ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
    1.16 -
    1.17 -lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
    1.18 -proof -
    1.19 -  obtain x y where xy: "z = Complex x y" by (cases z)
    1.20 -  {
    1.21 -    assume y0: "y = 0"
    1.22 -    {
    1.23 -      assume x0: "x \<ge> 0"
    1.24 -      then have ?thesis
    1.25 -        using y0 xy real_sqrt_pow2[OF x0]
    1.26 -        by (simp add: csqrt_def power2_eq_square)
    1.27 -    }
    1.28 -    moreover
    1.29 -    {
    1.30 -      assume "\<not> x \<ge> 0"
    1.31 -      then have x0: "- x \<ge> 0" by arith
    1.32 -      then have ?thesis
    1.33 -        using y0 xy real_sqrt_pow2[OF x0]
    1.34 -        by (simp add: csqrt_def power2_eq_square)
    1.35 -    }
    1.36 -    ultimately have ?thesis by blast
    1.37 -  }
    1.38 -  moreover
    1.39 -  {
    1.40 -    assume y0: "y \<noteq> 0"
    1.41 -    {
    1.42 -      fix x y
    1.43 -      let ?z = "Complex x y"
    1.44 -      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z"
    1.45 -        by auto
    1.46 -      then have "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0"
    1.47 -        by arith+
    1.48 -      then have "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0"
    1.49 -        by (simp_all add: power2_eq_square)
    1.50 -    }
    1.51 -    note th = this
    1.52 -    have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
    1.53 -      by (simp add: power2_eq_square)
    1.54 -    from th[of x y]
    1.55 -    have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
    1.56 -      "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
    1.57 -      unfolding sq4 by simp_all
    1.58 -    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) -
    1.59 -        sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
    1.60 -      unfolding power2_eq_square by simp
    1.61 -    have "sqrt 4 = sqrt (2\<^sup>2)"
    1.62 -      by simp
    1.63 -    then have sqrt4: "sqrt 4 = 2"
    1.64 -      by (simp only: real_sqrt_abs)
    1.65 -    have th2: "2 * (y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
    1.66 -      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
    1.67 -      unfolding power2_eq_square
    1.68 -      by (simp add: algebra_simps real_sqrt_divide sqrt4)
    1.69 -    from y0 xy have ?thesis
    1.70 -      apply (simp add: csqrt_def power2_eq_square)
    1.71 -      apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y]
    1.72 -        real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square]
    1.73 -        real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square]
    1.74 -        real_sqrt_mult[symmetric])
    1.75 -      using th1 th2  ..
    1.76 -  }
    1.77 -  ultimately show ?thesis by blast
    1.78 -qed
    1.79 -
    1.80 -lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
    1.81 -  by (simp add: csqrt_def)
    1.82 -
    1.83 -lemma csqrt_0 [simp]: "csqrt 0 = 0"
    1.84 -  by (simp add: csqrt_def)
    1.85 -
    1.86 -lemma csqrt_1 [simp]: "csqrt 1 = 1"
    1.87 -  by (simp add: csqrt_def)
    1.88 -
    1.89 -lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
    1.90 -proof (cases z)
    1.91 -  case (Complex x y)
    1.92 -  then show ?thesis
    1.93 -    using real_sqrt_sum_squares_ge1 [of "x" y]
    1.94 -          real_sqrt_sum_squares_ge1 [of "-x" y]
    1.95 -          real_sqrt_sum_squares_eq_cancel [of x y]
    1.96 -    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
    1.97 -    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
    1.98 -    apply (metis add_commute less_eq_real_def power_minus_Bit0
    1.99 -            real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
   1.100 -    done
   1.101 -qed
   1.102 -
   1.103 -lemma Re_csqrt: "0 \<le> Re(csqrt z)"
   1.104 -  by (metis csqrt_principal le_less)
   1.105 -
   1.106 -lemma csqrt_square: "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> csqrt (z\<^sup>2) = z"
   1.107 -  using csqrt [of "z\<^sup>2"] csqrt_principal [of "z\<^sup>2"]
   1.108 -  by (cases z) (auto simp: power2_eq_iff)
   1.109 -
   1.110 -lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
   1.111 -  by auto (metis csqrt power_eq_0_iff)
   1.112 -
   1.113 -lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
   1.114 -  by auto (metis csqrt power2_eq_1_iff)
   1.115 -
   1.116 -
   1.117  subsection {* More lemmas about module of complex numbers *}
   1.118  
   1.119 -lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
   1.120 -  by (rule of_real_power [symmetric])
   1.121 -
   1.122  text{* The triangle inequality for cmod *}
   1.123  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
   1.124    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
   1.125  
   1.126 -
   1.127  subsection {* Basic lemmas about polynomials *}
   1.128  
   1.129  lemma poly_bound_exists:
   1.130 @@ -281,7 +167,7 @@
   1.131      with IH[rule_format, of m] obtain z where z: "?P z m"
   1.132        by blast
   1.133      from z have "?P (csqrt z) n"
   1.134 -      by (simp add: m power_mult csqrt)
   1.135 +      by (simp add: m power_mult power2_csqrt)
   1.136      then have "\<exists>z. ?P z n" ..
   1.137    }
   1.138    moreover
   1.139 @@ -319,7 +205,7 @@
   1.140      let ?w = "v / complex_of_real (root n (cmod b))"
   1.141      from odd_real_root_pow[OF o, of "cmod b"]
   1.142      have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
   1.143 -      by (simp add: power_divide complex_of_real_power)
   1.144 +      by (simp add: power_divide of_real_power[symmetric])
   1.145      have th2:"cmod (complex_of_real (cmod b) / b) = 1"
   1.146        using b by (simp add: norm_divide)
   1.147      then have th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0"
   1.148 @@ -600,21 +486,6 @@
   1.149    ultimately show ?thesis by blast
   1.150  qed
   1.151  
   1.152 -lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a"
   1.153 -  unfolding power2_eq_square
   1.154 -  apply (simp add: rcis_mult)
   1.155 -  apply (simp add: power2_eq_square[symmetric])
   1.156 -  done
   1.157 -
   1.158 -lemma cispi: "cis pi = -1"
   1.159 -  by (simp add: cis_def)
   1.160 -
   1.161 -lemma "(rcis (sqrt (abs r)) ((pi + a) / 2))\<^sup>2 = rcis (- abs r) a"
   1.162 -  unfolding power2_eq_square
   1.163 -  apply (simp add: rcis_mult add_divide_distrib)
   1.164 -  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
   1.165 -  done
   1.166 -
   1.167  text {* Nonzero polynomial in z goes to infinity as z does. *}
   1.168  
   1.169  lemma poly_infinity: