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.98 -    apply (metis add_commute less_eq_real_def power_minus_Bit0
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