src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 56778 cb0929421ca6 parent 56776 309e1a61ee7c child 56795 e8cce2bd23e5
1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Apr 28 17:50:03 2014 +0200
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Mon Apr 28 23:43:13 2014 +0200
1.3 @@ -17,24 +17,39 @@
1.4       else Complex (sqrt((cmod z + Re z) /2)) ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
1.6  lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
1.7 -proof-
1.8 +proof -
1.9    obtain x y where xy: "z = Complex x y" by (cases z)
1.10 -  {assume y0: "y = 0"
1.11 -    {assume x0: "x \<ge> 0"
1.12 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.13 -        by (simp add: csqrt_def power2_eq_square)}
1.14 +  {
1.15 +    assume y0: "y = 0"
1.16 +    {
1.17 +      assume x0: "x \<ge> 0"
1.18 +      then have ?thesis
1.19 +        using y0 xy real_sqrt_pow2[OF x0]
1.20 +        by (simp add: csqrt_def power2_eq_square)
1.21 +    }
1.22      moreover
1.23 -    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
1.24 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.25 -        by (simp add: csqrt_def power2_eq_square) }
1.26 -    ultimately have ?thesis by blast}
1.27 +    {
1.28 +      assume "\<not> x \<ge> 0"
1.29 +      then have x0: "- x \<ge> 0" by arith
1.30 +      then have ?thesis
1.31 +        using y0 xy real_sqrt_pow2[OF x0]
1.32 +        by (simp add: csqrt_def power2_eq_square)
1.33 +    }
1.34 +    ultimately have ?thesis by blast
1.35 +  }
1.36    moreover
1.37 -  {assume y0: "y\<noteq>0"
1.38 -    {fix x y
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" by auto
1.45 -      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
1.46 -      hence "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0" by (simp_all add: power2_eq_square) }
1.47 +      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z"
1.48 +        by auto
1.49 +      then have "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0"
1.50 +        by arith+
1.51 +      then have "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0"
1.52 +        by (simp_all add: power2_eq_square)
1.53 +    }
1.54      note th = this
1.55      have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
1.56        by (simp add: power2_eq_square)
1.57 @@ -42,17 +57,25 @@
1.58      have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
1.59        "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
1.60        unfolding sq4 by simp_all
1.61 -    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
1.62 +    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) -
1.63 +        sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
1.64        unfolding power2_eq_square by simp
1.65 -    have "sqrt 4 = sqrt (2\<^sup>2)" by simp
1.66 -    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
1.67 -    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
1.68 +    have "sqrt 4 = sqrt (2\<^sup>2)"
1.69 +      by simp
1.70 +    then have sqrt4: "sqrt 4 = 2"
1.71 +      by (simp only: real_sqrt_abs)
1.72 +    have th2: "2 * (y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
1.73        using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
1.74        unfolding power2_eq_square
1.75        by (simp add: algebra_simps real_sqrt_divide sqrt4)
1.76 -     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
1.77 -       apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric])
1.78 -      using th1 th2  ..}
1.79 +    from y0 xy have ?thesis
1.80 +      apply (simp add: csqrt_def power2_eq_square)
1.81 +      apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y]
1.82 +        real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square]
1.83 +        real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square]
1.84 +        real_sqrt_mult[symmetric])
1.85 +      using th1 th2  ..
1.86 +  }
1.87    ultimately show ?thesis by blast
1.88  qed
1.90 @@ -74,14 +97,16 @@
1.91            real_sqrt_sum_squares_eq_cancel [of x y]
1.92      apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
1.93      apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
1.94 -    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
1.95 +    apply (metis add_commute less_eq_real_def power_minus_Bit0
1.96 +            real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
1.97 +    done
1.98  qed
1.100  lemma Re_csqrt: "0 \<le> Re(csqrt z)"
1.101    by (metis csqrt_principal le_less)
1.103 -lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
1.104 -  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
1.105 +lemma csqrt_square: "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> csqrt (z\<^sup>2) = z"
1.106 +  using csqrt [of "z\<^sup>2"] csqrt_principal [of "z\<^sup>2"]
1.107    by (cases z) (auto simp: power2_eq_iff)
1.109  lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
1.110 @@ -90,7 +115,8 @@
1.111  lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
1.112    by auto (metis csqrt power2_eq_1_iff)
1.114 -subsection{* More lemmas about module of complex numbers *}
1.116 +subsection {* More lemmas about module of complex numbers *}
1.118  lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
1.119    by (rule of_real_power [symmetric])
1.120 @@ -99,29 +125,37 @@
1.121  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
1.122    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
1.124 -subsection{* Basic lemmas about polynomials *}
1.126 +subsection {* Basic lemmas about polynomials *}
1.128  lemma poly_bound_exists:
1.129 -  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.130 -  shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z <= r \<longrightarrow> norm (poly p z) \<le> m)"
1.131 -proof(induct p)
1.132 -  case 0 thus ?case by (rule exI[where x=1], simp)
1.133 +  fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
1.134 +  shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z \<le> r \<longrightarrow> norm (poly p z) \<le> m)"
1.135 +proof (induct p)
1.136 +  case 0
1.137 +  then show ?case by (rule exI[where x=1]) simp
1.138  next
1.139    case (pCons c cs)
1.140    from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
1.141      by blast
1.142    let ?k = " 1 + norm c + \<bar>r * m\<bar>"
1.143    have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
1.144 -  {fix z :: 'a
1.145 +  {
1.146 +    fix z :: 'a
1.147      assume H: "norm z \<le> r"
1.148 -    from m H have th: "norm (poly cs z) \<le> m" by blast
1.149 -    from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
1.150 +    from m H have th: "norm (poly cs z) \<le> m"
1.151 +      by blast
1.152 +    from H have rp: "r \<ge> 0" using norm_ge_zero[of z]
1.153 +      by arith
1.154      have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
1.155        using norm_triangle_ineq[of c "z* poly cs z"] by simp
1.156 -    also have "\<dots> \<le> norm c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
1.157 +    also have "\<dots> \<le> norm c + r * m"
1.158 +      using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
1.159        by (simp add: norm_mult)
1.160 -    also have "\<dots> \<le> ?k" by simp
1.161 -    finally have "norm (poly (pCons c cs) z) \<le> ?k" .}
1.162 +    also have "\<dots> \<le> ?k"
1.163 +      by simp
1.164 +    finally have "norm (poly (pCons c cs) z) \<le> ?k" .
1.165 +  }
1.166    with kp show ?case by blast
1.167  qed
1.169 @@ -129,8 +163,7 @@
1.170  text{* Offsetting the variable in a polynomial gives another of same degree *}
1.172  definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
1.173 -where
1.174 -  "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
1.175 +  where "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
1.177  lemma offset_poly_0: "offset_poly 0 h = 0"
1.178    by (simp add: offset_poly_def)
1.179 @@ -141,45 +174,44 @@
1.180    by (cases "p = 0 \<and> a = 0") (auto simp add: offset_poly_def)
1.182  lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
1.183 -by (simp add: offset_poly_pCons offset_poly_0)
1.184 +  by (simp add: offset_poly_pCons offset_poly_0)
1.186  lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
1.187 -apply (induct p)
1.188 -apply (simp add: offset_poly_0)
1.189 -apply (simp add: offset_poly_pCons algebra_simps)
1.190 -done
1.191 +  apply (induct p)
1.192 +  apply (simp add: offset_poly_0)
1.193 +  apply (simp add: offset_poly_pCons algebra_simps)
1.194 +  done
1.196  lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
1.197 -by (induct p arbitrary: a, simp, force)
1.198 +  by (induct p arbitrary: a) (simp, force)
1.200  lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
1.201 -apply (safe intro!: offset_poly_0)
1.202 -apply (induct p, simp)
1.203 -apply (simp add: offset_poly_pCons)
1.204 -apply (frule offset_poly_eq_0_lemma, simp)
1.205 -done
1.206 +  apply (safe intro!: offset_poly_0)
1.207 +  apply (induct p, simp)
1.208 +  apply (simp add: offset_poly_pCons)
1.209 +  apply (frule offset_poly_eq_0_lemma, simp)
1.210 +  done
1.212  lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
1.213 -apply (induct p)
1.214 -apply (simp add: offset_poly_0)
1.215 -apply (case_tac "p = 0")
1.216 -apply (simp add: offset_poly_0 offset_poly_pCons)
1.217 -apply (simp add: offset_poly_pCons)
1.218 -apply (subst degree_add_eq_right)
1.219 -apply (rule le_less_trans [OF degree_smult_le])
1.220 -apply (simp add: offset_poly_eq_0_iff)
1.221 -apply (simp add: offset_poly_eq_0_iff)
1.222 -done
1.223 +  apply (induct p)
1.224 +  apply (simp add: offset_poly_0)
1.225 +  apply (case_tac "p = 0")
1.226 +  apply (simp add: offset_poly_0 offset_poly_pCons)
1.227 +  apply (simp add: offset_poly_pCons)
1.228 +  apply (subst degree_add_eq_right)
1.229 +  apply (rule le_less_trans [OF degree_smult_le])
1.230 +  apply (simp add: offset_poly_eq_0_iff)
1.231 +  apply (simp add: offset_poly_eq_0_iff)
1.232 +  done
1.234 -definition
1.235 -  "psize p = (if p = 0 then 0 else Suc (degree p))"
1.236 +definition "psize p = (if p = 0 then 0 else Suc (degree p))"
1.238  lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
1.239    unfolding psize_def by simp
1.241 -lemma poly_offset:
1.242 -  fixes p:: "('a::comm_ring_1) poly"
1.243 -  shows "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
1.244 +lemma poly_offset:
1.245 +  fixes p :: "'a::comm_ring_1 poly"
1.246 +  shows "\<exists>q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
1.247  proof (intro exI conjI)
1.248    show "psize (offset_poly p a) = psize p"
1.249      unfolding psize_def
1.250 @@ -189,8 +221,10 @@
1.251  qed
1.253  text{* An alternative useful formulation of completeness of the reals *}
1.254 -lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
1.255 -  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
1.256 +lemma real_sup_exists:
1.257 +  assumes ex: "\<exists>x. P x"
1.258 +    and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
1.259 +  shows "\<exists>s::real. \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
1.260  proof
1.261    from bz have "bdd_above (Collect P)"
1.262      by (force intro: less_imp_le)
1.263 @@ -202,43 +236,60 @@
1.264  lemma  unimodular_reduce_norm:
1.265    assumes md: "cmod z = 1"
1.266    shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
1.267 -proof-
1.268 -  obtain x y where z: "z = Complex x y " by (cases z, auto)
1.269 -  from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1" by (simp add: cmod_def)
1.270 -  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
1.271 -    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
1.272 +proof -
1.273 +  obtain x y where z: "z = Complex x y "
1.274 +    by (cases z) auto
1.275 +  from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1"
1.276 +    by (simp add: cmod_def)
1.277 +  {
1.278 +    assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
1.279 +    from C z xy have "2 * x \<le> 1" "2 * x \<ge> -1" "2 * y \<le> 1" "2 * y \<ge> -1"
1.280        by (simp_all add: cmod_def power2_eq_square algebra_simps)
1.281 -    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
1.282 -    hence "(abs (2 * x))\<^sup>2 <= 1\<^sup>2" "(abs (2 * y))\<^sup>2 <= 1\<^sup>2"
1.283 +    then have "abs (2 * x) \<le> 1" "abs (2 * y) \<le> 1"
1.284 +      by simp_all
1.285 +    then have "(abs (2 * x))\<^sup>2 \<le> 1\<^sup>2" "(abs (2 * y))\<^sup>2 \<le> 1\<^sup>2"
1.286        by - (rule power_mono, simp, simp)+
1.287 -    hence th0: "4*x\<^sup>2 \<le> 1" "4*y\<^sup>2 \<le> 1"
1.288 +    then have th0: "4 * x\<^sup>2 \<le> 1" "4 * y\<^sup>2 \<le> 1"
1.289        by (simp_all add: power_mult_distrib)
1.290 -    from add_mono[OF th0] xy have False by simp }
1.291 -  thus ?thesis unfolding linorder_not_le[symmetric] by blast
1.292 +    from add_mono[OF th0] xy have False by simp
1.293 +  }
1.294 +  then show ?thesis
1.295 +    unfolding linorder_not_le[symmetric] by blast
1.296  qed
1.298  text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
1.299  lemma reduce_poly_simple:
1.300 - assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
1.301 +  assumes b: "b \<noteq> 0"
1.302 +    and n: "n \<noteq> 0"
1.303    shows "\<exists>z. cmod (1 + b * z^n) < 1"
1.304 -using n
1.305 -proof(induct n rule: nat_less_induct)
1.306 +  using n
1.307 +proof (induct n rule: nat_less_induct)
1.308    fix n
1.309 -  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
1.310 +  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
1.311 +  assume n: "n \<noteq> 0"
1.312    let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
1.313 -  {assume e: "even n"
1.314 -    hence "\<exists>m. n = 2*m" by presburger
1.315 -    then obtain m where m: "n = 2*m" by blast
1.316 -    from n m have "m\<noteq>0" "m < n" by presburger+
1.317 -    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
1.318 +  {
1.319 +    assume e: "even n"
1.320 +    then have "\<exists>m. n = 2 * m"
1.321 +      by presburger
1.322 +    then obtain m where m: "n = 2 * m"
1.323 +      by blast
1.324 +    from n m have "m \<noteq> 0" "m < n"
1.325 +      by presburger+
1.326 +    with IH[rule_format, of m] obtain z where z: "?P z m"
1.327 +      by blast
1.328      from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
1.329 -    hence "\<exists>z. ?P z n" ..}
1.330 +    then have "\<exists>z. ?P z n" ..
1.331 +  }
1.332    moreover
1.333 -  {assume o: "odd n"
1.334 +  {
1.335 +    assume o: "odd n"
1.336      have th0: "cmod (complex_of_real (cmod b) / b) = 1"
1.337        using b by (simp add: norm_divide)
1.338 -    from o have "\<exists>m. n = Suc (2*m)" by presburger+
1.339 -    then obtain m where m: "n = Suc (2*m)" by blast
1.340 +    from o have "\<exists>m. n = Suc (2 * m)"
1.341 +      by presburger+
1.342 +    then obtain m where m: "n = Suc (2*m)"
1.343 +      by blast
1.344      from unimodular_reduce_norm[OF th0] o
1.345      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.346        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
1.347 @@ -251,28 +302,33 @@
1.348        apply (rule_tac x="ii" in exI)
1.349        apply (auto simp add: m power_mult)
1.350        done
1.351 -    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
1.352 +    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
1.353 +      by blast
1.354      let ?w = "v / complex_of_real (root n (cmod b))"
1.355      from odd_real_root_pow[OF o, of "cmod b"]
1.356      have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
1.357        by (simp add: power_divide complex_of_real_power)
1.358 -    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
1.359 -    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
1.360 +    have th2:"cmod (complex_of_real (cmod b) / b) = 1"
1.361 +      using b by (simp add: norm_divide)
1.362 +    then have th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0"
1.363 +      by simp
1.364      have th4: "cmod (complex_of_real (cmod b) / b) *
1.365 -   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
1.366 -   < cmod (complex_of_real (cmod b) / b) * 1"
1.367 +        cmod (1 + b * (v ^ n / complex_of_real (cmod b))) <
1.368 +        cmod (complex_of_real (cmod b) / b) * 1"
1.369        apply (simp only: norm_mult[symmetric] distrib_left)
1.370 -      using b v by (simp add: th2)
1.372 +      using b v
1.373 +      apply (simp add: th2)
1.374 +      done
1.375      from mult_less_imp_less_left[OF th4 th3]
1.376      have "?P ?w n" unfolding th1 .
1.377 -    hence "\<exists>z. ?P z n" .. }
1.378 +    then have "\<exists>z. ?P z n" ..
1.379 +  }
1.380    ultimately show "\<exists>z. ?P z n" by blast
1.381  qed
1.383  text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
1.385 -lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
1.386 +lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
1.387    using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
1.388    unfolding cmod_def by simp
1.390 @@ -280,66 +336,82 @@
1.391    assumes r: "\<forall>n. cmod (s n) \<le> r"
1.392    shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
1.393  proof-
1.394 -  from seq_monosub[of "Re o s"]
1.395 +  from seq_monosub[of "Re \<circ> s"]
1.396    obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
1.397      unfolding o_def by blast
1.398 -  from seq_monosub[of "Im o s o f"]
1.399 -  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
1.400 -  let ?h = "f o g"
1.401 -  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith
1.402 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>"
1.403 +  from seq_monosub[of "Im \<circ> s \<circ> f"]
1.404 +  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
1.405 +    unfolding o_def by blast
1.406 +  let ?h = "f \<circ> g"
1.407 +  from r[rule_format, of 0] have rp: "r \<ge> 0"
1.408 +    using norm_ge_zero[of "s 0"] by arith
1.409 +  have th: "\<forall>n. r + 1 \<ge> \<bar>Re (s n)\<bar>"
1.410    proof
1.411      fix n
1.412 -    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
1.413 +    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]
1.414 +    show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
1.415    qed
1.416 -  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
1.417 +  have conv1: "convergent (\<lambda>n. Re (s (f n)))"
1.418      apply (rule Bseq_monoseq_convergent)
1.419      apply (simp add: Bseq_def)
1.420      apply (metis gt_ex le_less_linear less_trans order.trans th)
1.421 -    using f(2) .
1.422 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
1.423 +    apply (rule f(2))
1.424 +    done
1.425 +  have th: "\<forall>n. r + 1 \<ge> \<bar>Im (s n)\<bar>"
1.426    proof
1.427      fix n
1.428 -    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
1.429 +    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]
1.430 +    show "\<bar>Im (s n)\<bar> \<le> r + 1"
1.431 +      by arith
1.432    qed
1.434    have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
1.435      apply (rule Bseq_monoseq_convergent)
1.436      apply (simp add: Bseq_def)
1.437      apply (metis gt_ex le_less_linear less_trans order.trans th)
1.438 -    using g(2) .
1.439 +    apply (rule g(2))
1.440 +    done
1.442    from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
1.443      by blast
1.444 -  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
1.445 +  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
1.446      unfolding LIMSEQ_iff real_norm_def .
1.448    from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
1.449      by blast
1.450 -  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
1.451 +  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
1.452      unfolding LIMSEQ_iff real_norm_def .
1.453    let ?w = "Complex x y"
1.454 -  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
1.455 -  {fix e assume ep: "e > (0::real)"
1.456 -    hence e2: "e/2 > 0" by simp
1.457 +  from f(1) g(1) have hs: "subseq ?h"
1.458 +    unfolding subseq_def by auto
1.459 +  {
1.460 +    fix e :: real
1.461 +    assume ep: "e > 0"
1.462 +    then have e2: "e/2 > 0" by simp
1.463      from x[rule_format, OF e2] y[rule_format, OF e2]
1.464 -    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
1.465 -    {fix n assume nN12: "n \<ge> N1 + N2"
1.466 -      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
1.467 +    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
1.468 +      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
1.469 +    {
1.470 +      fix n
1.471 +      assume nN12: "n \<ge> N1 + N2"
1.472 +      then have nN1: "g n \<ge> N1" and nN2: "n \<ge> N2"
1.473 +        using seq_suble[OF g(1), of n] by arith+
1.474        from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
1.475        have "cmod (s (?h n) - ?w) < e"
1.476 -        using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
1.477 -    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
1.478 -  with hs show ?thesis  by blast
1.479 +        using metric_bound_lemma[of "s (f (g n))" ?w] by simp
1.480 +    }
1.481 +    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast
1.482 +  }
1.483 +  with hs show ?thesis by blast
1.484  qed
1.486  text{* Polynomial is continuous. *}
1.488  lemma poly_cont:
1.489 -  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.490 +  fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
1.491    assumes ep: "e > 0"
1.492    shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
1.493 -proof-
1.494 +proof -
1.495    obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
1.496    proof
1.497      show "degree (offset_poly p z) = degree p"
1.498 @@ -347,125 +419,168 @@
1.499      show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
1.500        by (rule poly_offset_poly)
1.501    qed
1.502 -  {fix w
1.503 -    note q(2)[of "w - z", simplified]}
1.504 -  note th = this
1.505 +  have th: "\<And>w. poly q (w - z) = poly p w"
1.506 +    using q(2)[of "w - z" for w] by simp
1.507    show ?thesis unfolding th[symmetric]
1.508 -  proof(induct q)
1.509 -    case 0 thus ?case  using ep by auto
1.510 +  proof (induct q)
1.511 +    case 0
1.512 +    then show ?case
1.513 +      using ep by auto
1.514    next
1.515      case (pCons c cs)
1.516      from poly_bound_exists[of 1 "cs"]
1.517 -    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" by blast
1.518 -    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
1.519 -    have one0: "1 > (0::real)"  by arith
1.520 +    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m"
1.521 +      by blast
1.522 +    from ep m(1) have em0: "e/m > 0"
1.523 +      by (simp add: field_simps)
1.524 +    have one0: "1 > (0::real)"
1.525 +      by arith
1.526      from real_lbound_gt_zero[OF one0 em0]
1.527 -    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
1.528 -    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
1.529 +    obtain d where d: "d > 0" "d < 1" "d < e / m"
1.530 +      by blast
1.531 +    from d(1,3) m(1) have dm: "d * m > 0" "d * m < e"
1.532        by (simp_all add: field_simps)
1.533      show ?case
1.534 -      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
1.535 -        fix d w
1.536 -        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "norm (w-z) < d"
1.537 -        hence d1: "norm (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.538 -        from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
1.539 -        from H have th: "norm (w-z) \<le> d" by simp
1.540 -        from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
1.541 -        show "norm (w - z) * norm (poly cs (w - z)) < e" by simp
1.542 -      qed
1.543 +    proof (rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
1.544 +      fix d w
1.545 +      assume H: "d > 0" "d < 1" "d < e/m" "w \<noteq> z" "norm (w - z) < d"
1.546 +      then have d1: "norm (w-z) \<le> 1" "d \<ge> 0"
1.547 +        by simp_all
1.548 +      from H(3) m(1) have dme: "d*m < e"
1.549 +        by (simp add: field_simps)
1.550 +      from H have th: "norm (w - z) \<le> d"
1.551 +        by simp
1.552 +      from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
1.553 +      show "norm (w - z) * norm (poly cs (w - z)) < e"
1.554 +        by simp
1.555      qed
1.556 +  qed
1.557  qed
1.559  text{* Hence a polynomial attains minimum on a closed disc
1.560    in the complex plane. *}
1.561 -lemma  poly_minimum_modulus_disc:
1.562 -  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
1.563 -proof-
1.564 -  {assume "\<not> r \<ge> 0" hence ?thesis
1.565 -    by (metis norm_ge_zero order.trans)}
1.566 +lemma poly_minimum_modulus_disc: "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
1.567 +proof -
1.568 +  {
1.569 +    assume "\<not> r \<ge> 0"
1.570 +    then have ?thesis
1.571 +      by (metis norm_ge_zero order.trans)
1.572 +  }
1.573    moreover
1.574 -  {assume rp: "r \<ge> 0"
1.575 -    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
1.576 -    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
1.577 -    {fix x z
1.578 -      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
1.579 -      hence "- x < 0 " by arith
1.580 -      with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
1.581 -    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
1.582 +  {
1.583 +    assume rp: "r \<ge> 0"
1.584 +    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))"
1.585 +      by simp
1.586 +    then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
1.587 +      by blast
1.588 +    {
1.589 +      fix x z
1.590 +      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not> x < 1"
1.591 +      then have "- x < 0 "
1.592 +        by arith
1.593 +      with H(2) norm_ge_zero[of "poly p z"] have False
1.594 +        by simp
1.595 +    }
1.596 +    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z"
1.597 +      by blast
1.598      from real_sup_exists[OF mth1 mth2] obtain s where
1.599 -      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow>(y < s)" by blast
1.600 -    let ?m = "-s"
1.601 -    {fix y
1.602 -      from s[rule_format, of "-y"] have
1.603 -    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
1.604 -        unfolding minus_less_iff[of y ] equation_minus_iff by blast }
1.605 +      s: "\<forall>y. (\<exists>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<and> y < x) \<longleftrightarrow> y < s" by blast
1.606 +    let ?m = "- s"
1.607 +    {
1.608 +      fix y
1.609 +      from s[rule_format, of "-y"]
1.610 +      have "(\<exists>z x. cmod z \<le> r \<and> - (- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
1.611 +        unfolding minus_less_iff[of y ] equation_minus_iff by blast
1.612 +    }
1.613      note s1 = this[unfolded minus_minus]
1.614      from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
1.615        by auto
1.616 -    {fix n::nat
1.617 +    {
1.618 +      fix n :: nat
1.619        from s1[rule_format, of "?m + 1/real (Suc n)"]
1.620        have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
1.621 -        by simp}
1.622 -    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
1.623 +        by simp
1.624 +    }
1.625 +    then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
1.626      from choice[OF th] obtain g where
1.627 -      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
1.628 +        g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
1.629        by blast
1.630      from bolzano_weierstrass_complex_disc[OF g(1)]
1.631      obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
1.632        by blast
1.633 -    {fix w
1.634 +    {
1.635 +      fix w
1.636        assume wr: "cmod w \<le> r"
1.637        let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
1.638 -      {assume e: "?e > 0"
1.639 -        hence e2: "?e/2 > 0" by simp
1.640 +      {
1.641 +        assume e: "?e > 0"
1.642 +        then have e2: "?e/2 > 0" by simp
1.643          from poly_cont[OF e2, of z p] obtain d where
1.644 -          d: "d>0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2" by blast
1.645 -        {fix w assume w: "cmod (w - z) < d"
1.646 +            d: "d > 0" "\<forall>w. 0<cmod (w - z)\<and> cmod(w - z) < d \<longrightarrow> cmod(poly p w - poly p z) < ?e/2"
1.647 +          by blast
1.648 +        {
1.649 +          fix w
1.650 +          assume w: "cmod (w - z) < d"
1.651            have "cmod(poly p w - poly p z) < ?e / 2"
1.652 -            using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
1.653 +            using d(2)[rule_format, of w] w e by (cases "w = z") simp_all
1.654 +        }
1.655          note th1 = this
1.657 -        from fz(2)[rule_format, OF d(1)] obtain N1 where
1.658 -          N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
1.659 -        from reals_Archimedean2[of "2/?e"] obtain N2::nat where
1.660 -          N2: "2/?e < real N2" by blast
1.661 -        have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
1.662 +        from fz(2) d(1) obtain N1 where N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d"
1.663 +          by blast
1.664 +        from reals_Archimedean2[of "2/?e"] obtain N2 :: nat where N2: "2/?e < real N2"
1.665 +          by blast
1.666 +        have th2: "cmod (poly p (g (f (N1 + N2))) - poly p z) < ?e/2"
1.667            using N1[rule_format, of "N1 + N2"] th1 by simp
1.668 -        {fix a b e2 m :: real
1.669 -        have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
1.670 -          ==> False" by arith}
1.671 -      note th0 = this
1.672 -      have ath:
1.673 -        "\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
1.674 -      from s1m[OF g(1)[rule_format]]
1.675 -      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
1.676 -      from seq_suble[OF fz(1), of "N1+N2"]
1.677 -      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
1.678 -      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
1.679 -        using N2 by auto
1.680 -      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
1.681 -      from g(2)[rule_format, of "f (N1 + N2)"]
1.682 -      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
1.683 -      from order_less_le_trans[OF th01 th00]
1.684 -      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
1.685 -      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
1.686 -      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
1.687 -      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
1.688 -      with ath[OF th31 th32]
1.689 -      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
1.690 -      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
1.691 -        by arith
1.692 -      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
1.693 -\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
1.694 -        by (simp add: norm_triangle_ineq3)
1.695 -      from ath2[OF th22, of ?m]
1.696 -      have thc2: "2*(?e/2) \<le> \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)" by simp
1.697 -      from th0[OF th2 thc1 thc2] have False .}
1.698 -      hence "?e = 0" by auto
1.699 -      then have "cmod (poly p z) = ?m" by simp
1.700 -      with s1m[OF wr]
1.701 -      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
1.702 -    hence ?thesis by blast}
1.703 +        {
1.704 +          fix a b e2 m :: real
1.705 +          have "a < e2 \<Longrightarrow> \<bar>b - m\<bar> < e2 \<Longrightarrow> 2 * e2 \<le> \<bar>b - m\<bar> + a \<Longrightarrow> False"
1.706 +            by arith
1.707 +        }
1.708 +        note th0 = this
1.709 +        have ath: "\<And>m x e::real. m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e"
1.710 +          by arith
1.711 +        from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
1.712 +        from seq_suble[OF fz(1), of "N1+N2"]
1.713 +        have th00: "real (Suc (N1 + N2)) \<le> real (Suc (f (N1 + N2)))"
1.714 +          by simp
1.715 +        have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1 + N2)) > 0"
1.716 +          using N2 by auto
1.717 +        from frac_le[OF th000 th00]
1.718 +        have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
1.719 +          by simp
1.720 +        from g(2)[rule_format, of "f (N1 + N2)"]
1.721 +        have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
1.722 +        from order_less_le_trans[OF th01 th00]
1.723 +        have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
1.724 +        from N2 have "2/?e < real (Suc (N1 + N2))"
1.725 +          by arith
1.726 +        with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
1.727 +        have "?e/2 > 1/ real (Suc (N1 + N2))"
1.728 +          by (simp add: inverse_eq_divide)
1.729 +        with ath[OF th31 th32]
1.730 +        have thc1: "\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
1.731 +          by arith
1.732 +        have ath2: "\<And>a b c m::real. \<bar>a - b\<bar> \<le> c \<Longrightarrow> \<bar>b - m\<bar> \<le> \<bar>a - m\<bar> + c"
1.733 +          by arith
1.734 +        have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> \<le>
1.735 +            cmod (poly p (g (f (N1 + N2))) - poly p z)"
1.736 +          by (simp add: norm_triangle_ineq3)
1.737 +        from ath2[OF th22, of ?m]
1.738 +        have thc2: "2 * (?e/2) \<le>
1.739 +            \<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> + cmod (poly p (g (f (N1 + N2))) - poly p z)"
1.740 +          by simp
1.741 +        from th0[OF th2 thc1 thc2] have False .
1.742 +      }
1.743 +      then have "?e = 0"
1.744 +        by auto
1.745 +      then have "cmod (poly p z) = ?m"
1.746 +        by simp
1.747 +      with s1m[OF wr] have "cmod (poly p z) \<le> cmod (poly p w)"
1.748 +        by simp
1.749 +    }
1.750 +    then have ?thesis by blast
1.751 +  }
1.752    ultimately show ?thesis by blast
1.753  qed
1.755 @@ -476,8 +591,7 @@
1.756    done
1.758  lemma cispi: "cis pi = -1"
1.759 -  unfolding cis_def
1.760 -  by simp
1.761 +  by (simp add: cis_def)
1.763  lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
1.764    unfolding power2_eq_square
1.765 @@ -488,78 +602,99 @@
1.766  text {* Nonzero polynomial in z goes to infinity as z does. *}
1.768  lemma poly_infinity:
1.769 -  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.770 +  fixes p:: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
1.771    assumes ex: "p \<noteq> 0"
1.772    shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
1.773 -using ex
1.774 -proof(induct p arbitrary: a d)
1.775 +  using ex
1.776 +proof (induct p arbitrary: a d)
1.777    case (pCons c cs a d)
1.778 -  {assume H: "cs \<noteq> 0"
1.779 -    with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)" by blast
1.780 +  {
1.781 +    assume H: "cs \<noteq> 0"
1.782 +    with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)"
1.783 +      by blast
1.784      let ?r = "1 + \<bar>r\<bar>"
1.785 -    {fix z::'a assume h: "1 + \<bar>r\<bar> \<le> norm z"
1.786 +    {
1.787 +      fix z::'a
1.788 +      assume h: "1 + \<bar>r\<bar> \<le> norm z"
1.789        have r0: "r \<le> norm z" using h by arith
1.790 -      from r[rule_format, OF r0]
1.791 -      have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)" by arith
1.792 -      from h have z1: "norm z \<ge> 1" by arith
1.793 +      from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
1.794 +        by arith
1.795 +      from h have z1: "norm z \<ge> 1"
1.796 +        by arith
1.797        from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
1.798        have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
1.799          unfolding norm_mult by (simp add: algebra_simps)
1.800        from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
1.801        have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
1.802          by (simp add: algebra_simps)
1.803 -      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"  by arith}
1.804 -    hence ?case by blast}
1.805 +      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)" by arith
1.806 +    }
1.807 +    then have ?case by blast
1.808 +  }
1.809    moreover
1.810 -  {assume cs0: "\<not> (cs \<noteq> 0)"
1.811 -    with pCons.prems have c0: "c \<noteq> 0" by simp
1.812 -    from cs0 have cs0': "cs = 0" by simp
1.813 -    {fix z::'a
1.814 +  {
1.815 +    assume cs0: "\<not> (cs \<noteq> 0)"
1.816 +    with pCons.prems have c0: "c \<noteq> 0"
1.817 +      by simp
1.818 +    from cs0 have cs0': "cs = 0"
1.819 +      by simp
1.820 +    {
1.821 +      fix z::'a
1.822        assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
1.823 -      from c0 have "norm c > 0" by simp
1.824 +      from c0 have "norm c > 0"
1.825 +        by simp
1.826        from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
1.827          by (simp add: field_simps norm_mult)
1.828 -      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
1.829 -      from norm_diff_ineq[of "z * c" a ]
1.830 -      have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
1.831 +      have ath: "\<And>mzh mazh ma. mzh \<le> mazh + ma \<Longrightarrow> \<bar>d\<bar> + ma \<le> mzh \<Longrightarrow> d \<le> mazh"
1.832 +        by arith
1.833 +      from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
1.834          by (simp add: algebra_simps)
1.835        from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
1.836 -        using cs0' by simp}
1.837 -    then have ?case  by blast}
1.838 +        using cs0' by simp
1.839 +    }
1.840 +    then have ?case  by blast
1.841 +  }
1.842    ultimately show ?case by blast
1.843  qed simp
1.845  text {* Hence polynomial's modulus attains its minimum somewhere. *}
1.846 -lemma poly_minimum_modulus:
1.847 -  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
1.848 -proof(induct p)
1.849 +lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
1.850 +proof (induct p)
1.851 +  case 0
1.852 +  then show ?case by simp
1.853 +next
1.854    case (pCons c cs)
1.855 -  {assume cs0: "cs \<noteq> 0"
1.856 -    from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
1.857 -    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)" by blast
1.858 -    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
1.859 +  show ?case
1.860 +  proof (cases "cs = 0")
1.861 +    case False
1.862 +    from poly_infinity[OF False, of "cmod (poly (pCons c cs) 0)" c]
1.863 +    obtain r where r: "\<And>z. r \<le> cmod z \<Longrightarrow> cmod (poly (pCons c cs) 0) \<le> cmod (poly (pCons c cs) z)"
1.864 +      by blast
1.865 +    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>"
1.866 +      by arith
1.867      from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
1.868 -    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)" by blast
1.869 -    {fix z assume z: "r \<le> cmod z"
1.870 -      from v[of 0] r[OF z]
1.871 -      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
1.872 -        by simp }
1.873 +    obtain v where v: "\<And>w. cmod w \<le> \<bar>r\<bar> \<Longrightarrow> cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) w)"
1.874 +      by blast
1.875 +    {
1.876 +      fix z
1.877 +      assume z: "r \<le> cmod z"
1.878 +      from v[of 0] r[OF z] have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
1.879 +        by simp
1.880 +    }
1.881      note v0 = this
1.882 -    from v0 v ath[of r] have ?case by blast}
1.883 -  moreover
1.884 -  {assume cs0: "\<not> (cs \<noteq> 0)"
1.885 -    hence th:"cs = 0" by simp
1.886 -    from th pCons.hyps have ?case by simp}
1.887 -  ultimately show ?case by blast
1.888 -qed simp
1.889 +    from v0 v ath[of r] show ?thesis
1.890 +      by blast
1.891 +  next
1.892 +    case True
1.893 +    with pCons.hyps show ?thesis by simp
1.894 +  qed
1.895 +qed
1.897  text{* Constant function (non-syntactic characterization). *}
1.898  definition "constant f = (\<forall>x y. f x = f y)"
1.900 -lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
1.901 -  unfolding constant_def psize_def
1.902 -  apply (induct p, auto)
1.903 -  done
1.904 +lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
1.905 +  by (induct p) (auto simp: constant_def psize_def)
1.907  lemma poly_replicate_append:
1.908    "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
1.909 @@ -569,34 +704,38 @@
1.910    after the first.  *}
1.912  lemma poly_decompose_lemma:
1.913 - assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{idom}))"
1.914 -  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
1.915 -                 (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
1.916 -unfolding psize_def
1.917 -using nz
1.918 -proof(induct p)
1.919 -  case 0 thus ?case by simp
1.920 +  assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
1.921 +  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and>
1.922 +    (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
1.923 +  unfolding psize_def
1.924 +  using nz
1.925 +proof (induct p)
1.926 +  case 0
1.927 +  then show ?case by simp
1.928  next
1.929    case (pCons c cs)
1.930 -  {assume c0: "c = 0"
1.931 -    from pCons.hyps pCons.prems c0 have ?case
1.932 +  show ?case
1.933 +  proof (cases "c = 0")
1.934 +    case True
1.935 +    from pCons.hyps pCons.prems True show ?thesis
1.936        apply (auto)
1.937        apply (rule_tac x="k+1" in exI)
1.938        apply (rule_tac x="a" in exI, clarsimp)
1.939        apply (rule_tac x="q" in exI)
1.940 -      by (auto)}
1.941 -  moreover
1.942 -  {assume c0: "c\<noteq>0"
1.943 -    have ?case
1.944 +      apply auto
1.945 +      done
1.946 +  next
1.947 +    case False
1.948 +    show ?thesis
1.949        apply (rule exI[where x=0])
1.950 -      apply (rule exI[where x=c], auto simp add: c0)
1.951 -      done}
1.952 -  ultimately show ?case by blast
1.953 +      apply (rule exI[where x=c], auto simp add: False)
1.954 +      done
1.955 +  qed
1.956  qed
1.958  lemma poly_decompose:
1.959    assumes nc: "\<not> constant (poly p)"
1.960 -  shows "\<exists>k a q. a \<noteq> (0::'a::{idom}) \<and> k \<noteq> 0 \<and>
1.961 +  shows "\<exists>k a q. a \<noteq> (0::'a::idom) \<and> k \<noteq> 0 \<and>
1.962                 psize q + k + 1 = psize p \<and>
1.963                (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
1.964    using nc
1.965 @@ -613,7 +752,8 @@
1.966        from C have "poly (pCons c cs) x = poly (pCons c cs) y"
1.967          by (cases "x = 0") auto
1.969 -    with pCons.prems have False by (auto simp add: constant_def)
1.970 +    with pCons.prems have False
1.971 +      by (auto simp add: constant_def)
1.973    then have th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
1.974    from poly_decompose_lemma[OF th]
1.975 @@ -641,163 +781,227 @@
1.976    from nonconstant_length[OF less(2)] have n2: "psize p \<ge> 2" .
1.977    from poly_minimum_modulus obtain c where c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)"
1.978      by blast
1.979 -  {assume pc: "?p c = 0" hence ?ths by blast}
1.980 -  moreover
1.981 -  {assume pc0: "?p c \<noteq> 0"
1.982 -    from poly_offset[of p c] obtain q where
1.983 -      q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
1.984 -    {assume h: "constant (poly q)"
1.986 +  show ?ths
1.987 +  proof (cases "?p c = 0")
1.988 +    case True
1.989 +    then show ?thesis by blast
1.990 +  next
1.991 +    case False
1.992 +    note pc0 = this
1.993 +    from poly_offset[of p c] obtain q where q: "psize q = psize p" "\<forall>x. poly q x = ?p (c + x)"
1.994 +      by blast
1.995 +    {
1.996 +      assume h: "constant (poly q)"
1.997        from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
1.998 -      {fix x y
1.999 +      {
1.1000 +        fix x y
1.1001          from th have "?p x = poly q (x - c)" by auto
1.1002          also have "\<dots> = poly q (y - c)"
1.1003            using h unfolding constant_def by blast
1.1004          also have "\<dots> = ?p y" using th by auto
1.1005 -        finally have "?p x = ?p y" .}
1.1006 -      with less(2) have False unfolding constant_def by blast }
1.1007 -    hence qnc: "\<not> constant (poly q)" by blast
1.1008 -    from q(2) have pqc0: "?p c = poly q 0" by simp
1.1009 -    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
1.1010 +        finally have "?p x = ?p y" .
1.1011 +      }
1.1012 +      with less(2) have False
1.1013 +        unfolding constant_def by blast
1.1014 +    }
1.1015 +    then have qnc: "\<not> constant (poly q)"
1.1016 +      by blast
1.1017 +    from q(2) have pqc0: "?p c = poly q 0"
1.1018 +      by simp
1.1019 +    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)"
1.1020 +      by simp
1.1021      let ?a0 = "poly q 0"
1.1022 -    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp
1.1023 -    from a00
1.1024 -    have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
1.1025 +    from pc0 pqc0 have a00: "?a0 \<noteq> 0"
1.1026 +      by simp
1.1027 +    from a00 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
1.1028        by simp
1.1029      let ?r = "smult (inverse ?a0) q"
1.1030      have lgqr: "psize q = psize ?r"
1.1031 -      using a00 unfolding psize_def degree_def
1.1032 +      using a00
1.1033 +      unfolding psize_def degree_def
1.1034        by (simp add: poly_eq_iff)
1.1035 -    {assume h: "\<And>x y. poly ?r x = poly ?r y"
1.1036 -      {fix x y
1.1037 -        from qr[rule_format, of x]
1.1038 -        have "poly q x = poly ?r x * ?a0" by auto
1.1039 -        also have "\<dots> = poly ?r y * ?a0" using h by simp
1.1040 -        also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
1.1041 -        finally have "poly q x = poly q y" .}
1.1042 -      with qnc have False unfolding constant_def by blast}
1.1043 -    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
1.1044 -    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
1.1045 -    {fix w
1.1046 +    {
1.1047 +      assume h: "\<And>x y. poly ?r x = poly ?r y"
1.1048 +      {
1.1049 +        fix x y
1.1050 +        from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
1.1051 +          by auto
1.1052 +        also have "\<dots> = poly ?r y * ?a0"
1.1053 +          using h by simp
1.1054 +        also have "\<dots> = poly q y"
1.1055 +          using qr[rule_format, of y] by simp
1.1056 +        finally have "poly q x = poly q y" .
1.1057 +      }
1.1058 +      with qnc have False unfolding constant_def by blast
1.1059 +    }
1.1060 +    then have rnc: "\<not> constant (poly ?r)"
1.1061 +      unfolding constant_def by blast
1.1062 +    from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1"
1.1063 +      by auto
1.1064 +    {
1.1065 +      fix w
1.1066        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
1.1067          using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
1.1068        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
1.1069          using a00 unfolding norm_divide by (simp add: field_simps)
1.1070 -      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
1.1071 +      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
1.1072 +    }
1.1073      note mrmq_eq = this
1.1074      from poly_decompose[OF rnc] obtain k a s where
1.1075 -      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
1.1076 -      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
1.1077 -    {assume "psize p = k + 1"
1.1078 -      with kas(3) lgqr[symmetric] q(1) have s0:"s=0" by auto
1.1079 -      {fix w
1.1080 +      kas: "a \<noteq> 0" "k \<noteq> 0" "psize s + k + 1 = psize ?r"
1.1081 +        "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
1.1082 +    {
1.1083 +      assume "psize p = k + 1"
1.1084 +      with kas(3) lgqr[symmetric] q(1) have s0: "s = 0"
1.1085 +        by auto
1.1086 +      {
1.1087 +        fix w
1.1088          have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
1.1089 -          using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
1.1090 +          using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
1.1091 +      }
1.1092        note hth = this [symmetric]
1.1093 -        from reduce_poly_simple[OF kas(1,2)]
1.1094 -      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
1.1095 +      from reduce_poly_simple[OF kas(1,2)] have "\<exists>w. cmod (poly ?r w) < 1"
1.1096 +        unfolding hth by blast
1.1097 +    }
1.1098      moreover
1.1099 -    {assume kn: "psize p \<noteq> k+1"
1.1100 -      from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p" by simp
1.1101 +    {
1.1102 +      assume kn: "psize p \<noteq> k + 1"
1.1103 +      from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p"
1.1104 +        by simp
1.1105        have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
1.1106          unfolding constant_def poly_pCons poly_monom
1.1107          using kas(1) apply simp
1.1108 -        by (rule exI[where x=0], rule exI[where x=1], simp)
1.1109 -      from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
1.1110 +        apply (rule exI[where x=0])
1.1111 +        apply (rule exI[where x=1])
1.1112 +        apply simp
1.1113 +        done
1.1114 +      from kas(1) kas(2) have th02: "k + 1 = psize (pCons 1 (monom a (k - 1)))"
1.1115          by (simp add: psize_def degree_monom_eq)
1.1116        from less(1) [OF k1n [simplified th02] th01]
1.1117        obtain w where w: "1 + w^k * a = 0"
1.1118          unfolding poly_pCons poly_monom
1.1119 -        using kas(2) by (cases k, auto simp add: algebra_simps)
1.1120 +        using kas(2) by (cases k) (auto simp add: algebra_simps)
1.1121        from poly_bound_exists[of "cmod w" s] obtain m where
1.1122          m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
1.1123 -      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
1.1124 -      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
1.1125 -      then have wm1: "w^k * a = - 1" by simp
1.1126 +      have w0: "w \<noteq> 0" using kas(2) w
1.1127 +        by (auto simp add: power_0_left)
1.1128 +      from w have "(1 + w ^ k * a) - 1 = 0 - 1"
1.1129 +        by simp
1.1130 +      then have wm1: "w^k * a = - 1"
1.1131 +        by simp
1.1132        have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
1.1133          using norm_ge_zero[of w] w0 m(1)
1.1134 -          by (simp add: inverse_eq_divide zero_less_mult_iff)
1.1135 +        by (simp add: inverse_eq_divide zero_less_mult_iff)
1.1136        with real_lbound_gt_zero[OF zero_less_one] obtain t where
1.1137          t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
1.1138        let ?ct = "complex_of_real t"
1.1139        let ?w = "?ct * w"
1.1140 -      have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w" using kas(1) by (simp add: algebra_simps power_mult_distrib)
1.1141 +      have "1 + ?w^k * (a + ?w * poly s ?w) = 1 + ?ct^k * (w^k * a) + ?w^k * ?w * poly s ?w"
1.1142 +        using kas(1) by (simp add: algebra_simps power_mult_distrib)
1.1143        also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
1.1144 -        unfolding wm1 by (simp)
1.1145 -      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
1.1146 +        unfolding wm1 by simp
1.1147 +      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) =
1.1148 +        cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)"
1.1149          by metis
1.1150        with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
1.1151 -      have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
1.1152 -      have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
1.1153 -      have "t * cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
1.1154 -      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
1.1155 -      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
1.1156 +      have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)"
1.1157 +        unfolding norm_of_real by simp
1.1158 +      have ath: "\<And>x t::real. 0 \<le> x \<Longrightarrow> x < t \<Longrightarrow> t \<le> 1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1"
1.1159 +        by arith
1.1160 +      have "t * cmod w \<le> 1 * cmod w"
1.1161 +        apply (rule mult_mono)
1.1162 +        using t(1,2)
1.1163 +        apply auto
1.1164 +        done
1.1165 +      then have tw: "cmod ?w \<le> cmod w"
1.1166 +        using t(1) by (simp add: norm_mult)
1.1167 +      from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
1.1168          by (simp add: inverse_eq_divide field_simps)
1.1169 -      with zero_less_power[OF t(1), of k]
1.1170 -      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
1.1171 +      with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
1.1172          by (metis comm_mult_strict_left_mono)
1.1173 -      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
1.1174 +      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
1.1175 +        using w0 t(1)
1.1176          by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
1.1177        then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
1.1178          using t(1,2) m(2)[rule_format, OF tw] w0
1.1179          by auto
1.1180 -      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
1.1181 +      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k"
1.1182 +        by simp
1.1183        from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
1.1184          by auto
1.1185        from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
1.1186        have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
1.1187 -      from th11 th12
1.1188 -      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
1.1189 +      from th11 th12 have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"
1.1190 +        by arith
1.1191        then have "cmod (poly ?r ?w) < 1"
1.1192          unfolding kas(4)[rule_format, of ?w] r01 by simp
1.1193 -      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
1.1194 -    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
1.1195 -    from cr0_contr cq0 q(2)
1.1196 -    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
1.1197 -  ultimately show ?ths by blast
1.1198 +      then have "\<exists>w. cmod (poly ?r w) < 1"
1.1199 +        by blast
1.1200 +    }
1.1201 +    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1"
1.1202 +      by blast
1.1203 +    from cr0_contr cq0 q(2) show ?thesis
1.1204 +      unfolding mrmq_eq not_less[symmetric] by auto
1.1205 +  qed
1.1206  qed
1.1208  text {* Alternative version with a syntactic notion of constant polynomial. *}
1.1210  lemma fundamental_theorem_of_algebra_alt:
1.1211 -  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
1.1212 +  assumes nc: "\<not> (\<exists>a l. a \<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
1.1213    shows "\<exists>z. poly p z = (0::complex)"
1.1214 -using nc
1.1215 -proof(induct p)
1.1216 +  using nc
1.1217 +proof (induct p)
1.1218 +  case 0
1.1219 +  then show ?case by simp
1.1220 +next
1.1221    case (pCons c cs)
1.1222 -  {assume "c=0" hence ?case by auto}
1.1223 -  moreover
1.1224 -  {assume c0: "c\<noteq>0"
1.1225 -    {assume nc: "constant (poly (pCons c cs))"
1.1226 +  show ?case
1.1227 +  proof (cases "c = 0")
1.1228 +    case True
1.1229 +    then show ?thesis by auto
1.1230 +  next
1.1231 +    case False
1.1232 +    {
1.1233 +      assume nc: "constant (poly (pCons c cs))"
1.1234        from nc[unfolded constant_def, rule_format, of 0]
1.1235        have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
1.1236 -      hence "cs = 0"
1.1237 -        proof(induct cs)
1.1238 -          case (pCons d ds)
1.1239 -          {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
1.1240 -          moreover
1.1241 -          {assume d0: "d\<noteq>0"
1.1242 -            from poly_bound_exists[of 1 ds] obtain m where
1.1243 -              m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
1.1244 -            have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
1.1245 -            from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
1.1246 -              x: "x > 0" "x < cmod d / m" "x < 1" by blast
1.1247 -            let ?x = "complex_of_real x"
1.1248 -            from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
1.1249 -            from pCons.prems[rule_format, OF cx(1)]
1.1250 -            have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
1.1251 -            from m(2)[rule_format, OF cx(2)] x(1)
1.1252 -            have th0: "cmod (?x*poly ds ?x) \<le> x*m"
1.1253 -              by (simp add: norm_mult)
1.1254 -            from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
1.1255 -            with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
1.1256 -            with cth  have ?case by blast}
1.1257 -          ultimately show ?case by blast
1.1258 -        qed simp}
1.1259 -      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0
1.1260 -        by blast
1.1261 -      from fundamental_theorem_of_algebra[OF nc] have ?case .}
1.1262 -  ultimately show ?case by blast
1.1263 -qed simp
1.1264 +      then have "cs = 0"
1.1265 +      proof (induct cs)
1.1266 +        case 0
1.1267 +        then show ?case by simp
1.1268 +      next
1.1269 +        case (pCons d ds)
1.1270 +        show ?case
1.1271 +        proof (cases "d = 0")
1.1272 +          case True
1.1273 +          then show ?thesis using pCons.prems pCons.hyps by simp
1.1274 +        next
1.1275 +          case False
1.1276 +          from poly_bound_exists[of 1 ds] obtain m where
1.1277 +            m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
1.1278 +          have dm: "cmod d / m > 0" using False m(1) by (simp add: field_simps)
1.1279 +          from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
1.1280 +            x: "x > 0" "x < cmod d / m" "x < 1" by blast
1.1281 +          let ?x = "complex_of_real x"
1.1282 +          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
1.1283 +          from pCons.prems[rule_format, OF cx(1)]
1.1284 +          have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
1.1285 +          from m(2)[rule_format, OF cx(2)] x(1)
1.1286 +          have th0: "cmod (?x*poly ds ?x) \<le> x*m"
1.1287 +            by (simp add: norm_mult)
1.1288 +          from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
1.1289 +          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
1.1290 +          with cth show ?thesis by blast
1.1291 +        qed
1.1292 +      qed
1.1293 +    }
1.1294 +    then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems False
1.1295 +      by blast
1.1296 +    from fundamental_theorem_of_algebra[OF nc] show ?thesis .
1.1297 +  qed
1.1298 +qed
1.1301  subsection{* Nullstellensatz, degrees and divisibility of polynomials *}
1.1302 @@ -816,62 +1020,76 @@
1.1303                   (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
1.1304                   degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
1.1305      and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
1.1306 -    and dpn: "degree p = n" and n0: "n \<noteq> 0"
1.1307 +    and dpn: "degree p = n"
1.1308 +    and n0: "n \<noteq> 0"
1.1309    from dpn n0 have pne: "p \<noteq> 0" by auto
1.1310    let ?ths = "p dvd (q ^ n)"
1.1311 -  {fix a assume a: "poly p a = 0"
1.1312 -    {assume oa: "order a p \<noteq> 0"
1.1313 +  {
1.1314 +    fix a
1.1315 +    assume a: "poly p a = 0"
1.1316 +    {
1.1317 +      assume oa: "order a p \<noteq> 0"
1.1318        let ?op = "order a p"
1.1319 -      from pne have ap: "([:- a, 1:] ^ ?op) dvd p"
1.1320 -        "\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
1.1321 +      from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
1.1322 +        using order by blast+
1.1323        note oop = order_degree[OF pne, unfolded dpn]
1.1324 -      {assume q0: "q = 0"
1.1325 -        hence ?ths using n0
1.1326 -          by (simp add: power_0_left)}
1.1327 +      {
1.1328 +        assume q0: "q = 0"
1.1329 +        then have ?ths using n0
1.1330 +          by (simp add: power_0_left)
1.1331 +      }
1.1332        moreover
1.1333 -      {assume q0: "q \<noteq> 0"
1.1334 +      {
1.1335 +        assume q0: "q \<noteq> 0"
1.1336          from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
1.1337          obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
1.1338 -        from ap(1) obtain s where
1.1339 -          s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
1.1340 -        have sne: "s \<noteq> 0"
1.1341 -          using s pne by auto
1.1342 -        {assume ds0: "degree s = 0"
1.1343 +        from ap(1) obtain s where s: "p = [:- a, 1:] ^ ?op * s"
1.1344 +          by (rule dvdE)
1.1345 +        have sne: "s \<noteq> 0" using s pne by auto
1.1346 +        {
1.1347 +          assume ds0: "degree s = 0"
1.1348            from ds0 obtain k where kpn: "s = [:k:]"
1.1349              by (cases s) (auto split: if_splits)
1.1350            from sne kpn have k: "k \<noteq> 0" by simp
1.1351            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
1.1352            have "q ^ n = p * ?w"
1.1353              apply (subst r, subst s, subst kpn)
1.1354 -            using k oop [of a]
1.1355 +            using k oop [of a]
1.1356              apply (subst power_mult_distrib, simp)
1.1357              apply (subst power_add [symmetric], simp)
1.1358              done
1.1359 -          hence ?ths unfolding dvd_def by blast}
1.1360 +          then have ?ths unfolding dvd_def by blast
1.1361 +        }
1.1362          moreover
1.1363 -        {assume ds0: "degree s \<noteq> 0"
1.1364 +        {
1.1365 +          assume ds0: "degree s \<noteq> 0"
1.1366            from ds0 sne dpn s oa
1.1367 -            have dsn: "degree s < n" apply auto
1.1368 +            have dsn: "degree s < n"
1.1369 +              apply auto
1.1370                apply (erule ssubst)
1.1371                apply (simp add: degree_mult_eq degree_linear_power)
1.1372                done
1.1373 -            {fix x assume h: "poly s x = 0"
1.1374 -              {assume xa: "x = a"
1.1375 -                from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
1.1376 -                  u: "s = [:- a, 1:] * u" by (rule dvdE)
1.1377 +            {
1.1378 +              fix x assume h: "poly s x = 0"
1.1379 +              {
1.1380 +                assume xa: "x = a"
1.1381 +                from h[unfolded xa poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
1.1382 +                  by (rule dvdE)
1.1383                  have "p = [:- a, 1:] ^ (Suc ?op) * u"
1.1384                    by (subst s, subst u, simp only: power_Suc mult_ac)
1.1385 -                with ap(2)[unfolded dvd_def] have False by blast}
1.1386 +                with ap(2)[unfolded dvd_def] have False by blast
1.1387 +              }
1.1388                note xa = this
1.1389 -              from h have "poly p x = 0" by (subst s, simp)
1.1390 +              from h have "poly p x = 0" by (subst s) simp
1.1391                with pq0 have "poly q x = 0" by blast
1.1392                with r xa have "poly r x = 0"
1.1393 -                by auto}
1.1394 +                by auto
1.1395 +            }
1.1396              note impth = this
1.1397              from IH[rule_format, OF dsn, of s r] impth ds0
1.1398              have "s dvd (r ^ (degree s))" by blast
1.1399              then obtain u where u: "r ^ (degree s) = s * u" ..
1.1400 -            hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
1.1401 +            then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
1.1402                by (simp only: poly_mult[symmetric] poly_power[symmetric])
1.1403              let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
1.1404              from oop[of a] dsn have "q ^ n = p * ?w"
1.1405 @@ -884,19 +1102,28 @@
1.1406                apply (subst u [symmetric])
1.1407                apply (simp add: mult_ac power_add [symmetric])
1.1408                done
1.1409 -            hence ?ths unfolding dvd_def by blast}
1.1410 -      ultimately have ?ths by blast }
1.1411 -      ultimately have ?ths by blast}
1.1412 -    then have ?ths using a order_root pne by blast}
1.1413 +            then have ?ths unfolding dvd_def by blast
1.1414 +        }
1.1415 +        ultimately have ?ths by blast
1.1416 +      }
1.1417 +      ultimately have ?ths by blast
1.1418 +    }
1.1419 +    then have ?ths using a order_root pne by blast
1.1420 +  }
1.1421    moreover
1.1422 -  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
1.1423 -    from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
1.1424 -      ccs: "c\<noteq>0" "p = pCons c 0" by blast
1.1426 -    then have pp: "\<And>x. poly p x =  c" by simp
1.1427 +  {
1.1428 +    assume exa: "\<not> (\<exists>a. poly p a = 0)"
1.1429 +    from fundamental_theorem_of_algebra_alt[of p] exa
1.1430 +    obtain c where ccs: "c \<noteq> 0" "p = pCons c 0"
1.1431 +      by blast
1.1432 +    then have pp: "\<And>x. poly p x = c"
1.1433 +      by simp
1.1434      let ?w = "[:1/c:] * (q ^ n)"
1.1435 -    from ccs have "(q ^ n) = (p * ?w)" by simp
1.1436 -    hence ?ths unfolding dvd_def by blast}
1.1437 +    from ccs have "(q ^ n) = (p * ?w)"
1.1438 +      by simp
1.1439 +    then have ?ths
1.1440 +      unfolding dvd_def by blast
1.1441 +  }
1.1442    ultimately show ?ths by blast
1.1443  qed
1.1445 @@ -904,34 +1131,53 @@
1.1446    "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
1.1447      p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
1.1448  proof -
1.1449 -  {assume pe: "p = 0"
1.1450 -    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
1.1451 +  {
1.1452 +    assume pe: "p = 0"
1.1453 +    then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
1.1454        by (auto simp add: poly_all_0_iff_0)
1.1455 -    {assume "p dvd (q ^ (degree p))"
1.1456 +    {
1.1457 +      assume "p dvd (q ^ (degree p))"
1.1458        then obtain r where r: "q ^ (degree p) = p * r" ..
1.1459 -      from r pe have False by simp}
1.1460 -    with eq pe have ?thesis by blast}
1.1461 +      from r pe have False by simp
1.1462 +    }
1.1463 +    with eq pe have ?thesis by blast
1.1464 +  }
1.1465    moreover
1.1466 -  {assume pe: "p \<noteq> 0"
1.1467 -    {assume dp: "degree p = 0"
1.1468 -      then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
1.1469 +  {
1.1470 +    assume pe: "p \<noteq> 0"
1.1471 +    {
1.1472 +      assume dp: "degree p = 0"
1.1473 +      then obtain k where k: "p = [:k:]" "k \<noteq> 0" using pe
1.1474          by (cases p) (simp split: if_splits)
1.1475 -      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
1.1476 +      then have th1: "\<forall>x. poly p x \<noteq> 0"
1.1477 +        by simp
1.1478        from k dp have "q ^ (degree p) = p * [:1/k:]"
1.1479          by (simp add: one_poly_def)
1.1480 -      hence th2: "p dvd (q ^ (degree p))" ..
1.1481 -      from th1 th2 pe have ?thesis by blast}
1.1482 +      then have th2: "p dvd (q ^ (degree p))" ..
1.1483 +      from th1 th2 pe have ?thesis by blast
1.1484 +    }
1.1485      moreover
1.1486 -    {assume dp: "degree p \<noteq> 0"
1.1487 -      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
1.1488 -      {assume "p dvd (q ^ (Suc n))"
1.1489 +    {
1.1490 +      assume dp: "degree p \<noteq> 0"
1.1491 +      then obtain n where n: "degree p = Suc n "
1.1492 +        by (cases "degree p") auto
1.1493 +      {
1.1494 +        assume "p dvd (q ^ (Suc n))"
1.1495          then obtain u where u: "q ^ (Suc n) = p * u" ..
1.1496 -        {fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.1497 -          hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
1.1498 -          hence False using u h(1) by (simp only: poly_mult) simp}}
1.1499 -        with n nullstellensatz_lemma[of p q "degree p"] dp
1.1500 -        have ?thesis by auto}
1.1501 -    ultimately have ?thesis by blast}
1.1502 +        {
1.1503 +          fix x
1.1504 +          assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.1505 +          then have "poly (q ^ (Suc n)) x \<noteq> 0"
1.1506 +            by simp
1.1507 +          then have False using u h(1)
1.1508 +            by (simp only: poly_mult) simp
1.1509 +        }
1.1510 +      }
1.1511 +      with n nullstellensatz_lemma[of p q "degree p"] dp
1.1512 +      have ?thesis by auto
1.1513 +    }
1.1514 +    ultimately have ?thesis by blast
1.1515 +  }
1.1516    ultimately show ?thesis by blast
1.1517  qed
1.1519 @@ -967,39 +1213,40 @@
1.1520  (* Arithmetic operations on multivariate polynomials.                        *)
1.1522  lemma mpoly_base_conv:
1.1523 -  fixes x :: "'a::comm_ring_1"
1.1524 +  fixes x :: "'a::comm_ring_1"
1.1525    shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
1.1526    by simp_all
1.1528  lemma mpoly_norm_conv:
1.1529 -  fixes x :: "'a::comm_ring_1"
1.1530 +  fixes x :: "'a::comm_ring_1"
1.1531    shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x"
1.1532    by simp_all
1.1534  lemma mpoly_sub_conv:
1.1535 -  fixes x :: "'a::comm_ring_1"
1.1536 +  fixes x :: "'a::comm_ring_1"
1.1537    shows "poly p x - poly q x = poly p x + -1 * poly q x"
1.1538    by simp
1.1540 -lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = 0" by simp
1.1541 +lemma poly_pad_rule: "poly p x = 0 \<Longrightarrow> poly (pCons 0 p) x = 0"
1.1542 +  by simp
1.1544  lemma poly_cancel_eq_conv:
1.1545 -  fixes x :: "'a::field"
1.1546 -  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
1.1547 +  fixes x :: "'a::field"
1.1548 +  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
1.1549    by auto
1.1551  lemma poly_divides_pad_rule:
1.1552 -  fixes p:: "('a::comm_ring_1) poly"
1.1553 +  fixes p:: "('a::comm_ring_1) poly"
1.1554    assumes pq: "p dvd q"
1.1555 -shows "p dvd (pCons 0 q)"
1.1556 -proof-
1.1557 +  shows "p dvd (pCons 0 q)"
1.1558 +proof -
1.1559    have "pCons 0 q = q * [:0,1:]" by simp
1.1560    then have "q dvd (pCons 0 q)" ..
1.1561    with pq show ?thesis by (rule dvd_trans)
1.1562  qed
1.1564  lemma poly_divides_conv0:
1.1565 -  fixes p:: "'a::field poly"
1.1566 +  fixes p:: "'a::field poly"
1.1567    assumes lgpq: "degree q < degree p"
1.1568      and lq: "p \<noteq> 0"
1.1569    shows "p dvd q \<longleftrightarrow> q = 0" (is "?lhs \<longleftrightarrow> ?rhs")
1.1570 @@ -1009,22 +1256,20 @@
1.1571    then show ?lhs ..
1.1572  next
1.1573    assume l: ?lhs
1.1574 -  {
1.1575 -    assume q0: "q = 0"
1.1576 -    then have ?rhs by simp
1.1577 -  }
1.1578 -  moreover
1.1579 -  {
1.1580 +  show ?rhs
1.1581 +  proof (cases "q = 0")
1.1582 +    case True
1.1583 +    then show ?thesis by simp
1.1584 +  next
1.1585      assume q0: "q \<noteq> 0"
1.1586      from l q0 have "degree p \<le> degree q"
1.1587        by (rule dvd_imp_degree_le)
1.1588 -    with lgpq have ?rhs by simp
1.1589 -  }
1.1590 -  ultimately show ?rhs by blast
1.1591 +    with lgpq show ?thesis by simp
1.1592 +  qed
1.1593  qed
1.1595  lemma poly_divides_conv1:
1.1596 -  fixes p :: "('a::field) poly"
1.1597 +  fixes p :: "'a::field poly"
1.1598    assumes a0: "a \<noteq> 0"
1.1599      and pp': "p dvd p'"
1.1600      and qrp': "smult a q - p' = r"
1.1601 @@ -1098,7 +1343,7 @@
1.1602  qed
1.1604  lemma poly_const_conv:
1.1605 -  fixes x :: "'a::comm_ring_1"
1.1606 +  fixes x :: "'a::comm_ring_1"
1.1607    shows "poly [:c:] x = y \<longleftrightarrow> c = y"
1.1608    by simp