src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 60424 c96fff9dcdbc
parent 59557 ebd8ecacfba6
child 60449 229bad93377e
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jun 10 22:28:56 2015 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Jun 10 23:34:23 2015 +0200
     1.3 @@ -1,18 +1,20 @@
     1.4  (* Author: Amine Chaieb, TU Muenchen *)
     1.5  
     1.6 -section{*Fundamental Theorem of Algebra*}
     1.7 +section \<open>Fundamental Theorem of Algebra\<close>
     1.8  
     1.9  theory Fundamental_Theorem_Algebra
    1.10  imports Polynomial Complex_Main
    1.11  begin
    1.12  
    1.13 -subsection {* More lemmas about module of complex numbers *}
    1.14 +subsection \<open>More lemmas about module of complex numbers\<close>
    1.15  
    1.16 -text{* The triangle inequality for cmod *}
    1.17 +text \<open>The triangle inequality for cmod\<close>
    1.18 +
    1.19  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
    1.20    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
    1.21  
    1.22 -subsection {* Basic lemmas about polynomials *}
    1.23 +
    1.24 +subsection \<open>Basic lemmas about polynomials\<close>
    1.25  
    1.26  lemma poly_bound_exists:
    1.27    fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
    1.28 @@ -27,9 +29,8 @@
    1.29    let ?k = " 1 + norm c + \<bar>r * m\<bar>"
    1.30    have kp: "?k > 0"
    1.31      using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
    1.32 -  {
    1.33 -    fix z :: 'a
    1.34 -    assume H: "norm z \<le> r"
    1.35 +  have "norm (poly (pCons c cs) z) \<le> ?k" if H: "norm z \<le> r" for z
    1.36 +  proof -
    1.37      from m H have th: "norm (poly cs z) \<le> m"
    1.38        by blast
    1.39      from H have rp: "r \<ge> 0"
    1.40 @@ -41,13 +42,13 @@
    1.41        by (simp add: norm_mult)
    1.42      also have "\<dots> \<le> ?k"
    1.43        by simp
    1.44 -    finally have "norm (poly (pCons c cs) z) \<le> ?k" .
    1.45 -  }
    1.46 +    finally show ?thesis .
    1.47 +  qed
    1.48    with kp show ?case by blast
    1.49  qed
    1.50  
    1.51  
    1.52 -text{* Offsetting the variable in a polynomial gives another of same degree *}
    1.53 +text \<open>Offsetting the variable in a polynomial gives another of same degree\<close>
    1.54  
    1.55  definition offset_poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
    1.56    where "offset_poly p h = fold_coeffs (\<lambda>a q. smult h q + pCons a q) p 0"
    1.57 @@ -108,7 +109,7 @@
    1.58      by (simp add: poly_offset_poly)
    1.59  qed
    1.60  
    1.61 -text{* An alternative useful formulation of completeness of the reals *}
    1.62 +text \<open>An alternative useful formulation of completeness of the reals\<close>
    1.63  lemma real_sup_exists:
    1.64    assumes ex: "\<exists>x. P x"
    1.65      and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
    1.66 @@ -120,8 +121,10 @@
    1.67      using ex bz by (subst less_cSup_iff) auto
    1.68  qed
    1.69  
    1.70 -subsection {* Fundamental theorem of algebra *}
    1.71 -lemma  unimodular_reduce_norm:
    1.72 +
    1.73 +subsection \<open>Fundamental theorem of algebra\<close>
    1.74 +
    1.75 +lemma unimodular_reduce_norm:
    1.76    assumes md: "cmod z = 1"
    1.77    shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
    1.78  proof -
    1.79 @@ -145,7 +148,7 @@
    1.80      unfolding linorder_not_le[symmetric] by blast
    1.81  qed
    1.82  
    1.83 -text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
    1.84 +text \<open>Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero\<close>
    1.85  lemma reduce_poly_simple:
    1.86    assumes b: "b \<noteq> 0"
    1.87      and n: "n \<noteq> 0"
    1.88 @@ -224,7 +227,7 @@
    1.89    ultimately show "\<exists>z. ?P z n" by blast
    1.90  qed
    1.91  
    1.92 -text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
    1.93 +text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
    1.94  
    1.95  lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
    1.96    using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
    1.97 @@ -233,7 +236,7 @@
    1.98  lemma bolzano_weierstrass_complex_disc:
    1.99    assumes r: "\<forall>n. cmod (s n) \<le> r"
   1.100    shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   1.101 -proof-
   1.102 +proof -
   1.103    from seq_monosub[of "Re \<circ> s"]
   1.104    obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
   1.105      unfolding o_def by blast
   1.106 @@ -306,7 +309,7 @@
   1.107    with hs show ?thesis by blast
   1.108  qed
   1.109  
   1.110 -text{* Polynomial is continuous. *}
   1.111 +text \<open>Polynomial is continuous.\<close>
   1.112  
   1.113  lemma poly_cont:
   1.114    fixes p :: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
   1.115 @@ -358,19 +361,18 @@
   1.116    qed
   1.117  qed
   1.118  
   1.119 -text{* Hence a polynomial attains minimum on a closed disc
   1.120 -  in the complex plane. *}
   1.121 +text \<open>Hence a polynomial attains minimum on a closed disc
   1.122 +  in the complex plane.\<close>
   1.123  lemma poly_minimum_modulus_disc: "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
   1.124  proof -
   1.125 -  {
   1.126 -    assume "\<not> r \<ge> 0"
   1.127 -    then have ?thesis
   1.128 +  show ?thesis
   1.129 +  proof (cases "r \<ge> 0")
   1.130 +    case False
   1.131 +    then show ?thesis
   1.132        by (metis norm_ge_zero order.trans)
   1.133 -  }
   1.134 -  moreover
   1.135 -  {
   1.136 -    assume rp: "r \<ge> 0"
   1.137 -    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))"
   1.138 +  next
   1.139 +    case True
   1.140 +    then have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))"
   1.141        by simp
   1.142      then have mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"
   1.143        by blast
   1.144 @@ -434,13 +436,10 @@
   1.145            by blast
   1.146          have th2: "cmod (poly p (g (f (N1 + N2))) - poly p z) < ?e/2"
   1.147            using N1[rule_format, of "N1 + N2"] th1 by simp
   1.148 -        {
   1.149 -          fix a b e2 m :: real
   1.150 -          have "a < e2 \<Longrightarrow> \<bar>b - m\<bar> < e2 \<Longrightarrow> 2 * e2 \<le> \<bar>b - m\<bar> + a \<Longrightarrow> False"
   1.151 -            by arith
   1.152 -        }
   1.153 -        note th0 = this
   1.154 -        have ath: "\<And>m x e::real. m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e"
   1.155 +        have th0: "a < e2 \<Longrightarrow> \<bar>b - m\<bar> < e2 \<Longrightarrow> 2 * e2 \<le> \<bar>b - m\<bar> + a \<Longrightarrow> False"
   1.156 +          for a b e2 m :: real
   1.157 +          by arith
   1.158 +        have ath: "m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e" for m x e :: real
   1.159            by arith
   1.160          from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   1.161          from seq_suble[OF fz(1), of "N1 + N2"]
   1.162 @@ -460,10 +459,9 @@
   1.163          with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   1.164          have "?e/2 > 1/ real (Suc (N1 + N2))"
   1.165            by (simp add: inverse_eq_divide)
   1.166 -        with ath[OF th31 th32]
   1.167 -        have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
   1.168 +        with ath[OF th31 th32] have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
   1.169            by arith
   1.170 -        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.171 +        have ath2: "\<bar>a - b\<bar> \<le> c \<Longrightarrow> \<bar>b - m\<bar> \<le> \<bar>a - m\<bar> + c" for a b c m :: real
   1.172            by arith
   1.173          have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar> \<le>
   1.174              cmod (poly p (g (f (N1 + N2))) - poly p z)"
   1.175 @@ -481,12 +479,11 @@
   1.176        with s1m[OF wr] have "cmod (poly p z) \<le> cmod (poly p w)"
   1.177          by simp
   1.178      }
   1.179 -    then have ?thesis by blast
   1.180 -  }
   1.181 -  ultimately show ?thesis by blast
   1.182 +    then show ?thesis by blast
   1.183 +  qed
   1.184  qed
   1.185  
   1.186 -text {* Nonzero polynomial in z goes to infinity as z does. *}
   1.187 +text \<open>Nonzero polynomial in z goes to infinity as z does.\<close>
   1.188  
   1.189  lemma poly_infinity:
   1.190    fixes p:: "'a::{comm_semiring_0,real_normed_div_algebra} poly"
   1.191 @@ -527,9 +524,9 @@
   1.192      case True
   1.193      with pCons.prems have c0: "c \<noteq> 0"
   1.194        by simp
   1.195 -    {
   1.196 -      fix z :: 'a
   1.197 -      assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
   1.198 +    have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.199 +      if h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z" for z :: 'a
   1.200 +    proof -
   1.201        from c0 have "norm c > 0"
   1.202          by simp
   1.203        from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
   1.204 @@ -538,14 +535,14 @@
   1.205          by arith
   1.206        from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
   1.207          by (simp add: algebra_simps)
   1.208 -      from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.209 +      from ath[OF th1 th0] show ?thesis
   1.210          using True by simp
   1.211 -    }
   1.212 +    qed
   1.213      then show ?thesis by blast
   1.214    qed
   1.215  qed
   1.216  
   1.217 -text {* Hence polynomial's modulus attains its minimum somewhere. *}
   1.218 +text \<open>Hence polynomial's modulus attains its minimum somewhere.\<close>
   1.219  lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   1.220  proof (induct p)
   1.221    case 0
   1.222 @@ -563,22 +560,18 @@
   1.223      from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
   1.224      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.225        by blast
   1.226 -    {
   1.227 -      fix z
   1.228 -      assume z: "r \<le> cmod z"
   1.229 -      from v[of 0] r[OF z] have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
   1.230 -        by simp
   1.231 -    }
   1.232 -    note v0 = this
   1.233 -    from v0 v ath[of r] show ?thesis
   1.234 +    have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)" if z: "r \<le> cmod z" for z
   1.235 +      using v[of 0] r[OF z] by simp
   1.236 +    with v ath[of r] show ?thesis
   1.237        by blast
   1.238    next
   1.239      case True
   1.240 -    with pCons.hyps show ?thesis by simp
   1.241 +    with pCons.hyps show ?thesis
   1.242 +      by simp
   1.243    qed
   1.244  qed
   1.245  
   1.246 -text{* Constant function (non-syntactic characterization). *}
   1.247 +text \<open>Constant function (non-syntactic characterization).\<close>
   1.248  definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
   1.249  
   1.250  lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
   1.251 @@ -587,8 +580,7 @@
   1.252  lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
   1.253    by (simp add: poly_monom)
   1.254  
   1.255 -text {* Decomposition of polynomial, skipping zero coefficients
   1.256 -  after the first.  *}
   1.257 +text \<open>Decomposition of polynomial, skipping zero coefficients after the first.\<close>
   1.258  
   1.259  lemma poly_decompose_lemma:
   1.260    assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
   1.261 @@ -604,7 +596,7 @@
   1.262    proof (cases "c = 0")
   1.263      case True
   1.264      from pCons.hyps pCons.prems True show ?thesis
   1.265 -      apply (auto)
   1.266 +      apply auto
   1.267        apply (rule_tac x="k+1" in exI)
   1.268        apply (rule_tac x="a" in exI, clarsimp)
   1.269        apply (rule_tac x="q" in exI)
   1.270 @@ -614,7 +606,8 @@
   1.271      case False
   1.272      show ?thesis
   1.273        apply (rule exI[where x=0])
   1.274 -      apply (rule exI[where x=c], auto simp add: False)
   1.275 +      apply (rule exI[where x=c])
   1.276 +      apply (auto simp: False)
   1.277        done
   1.278    qed
   1.279  qed
   1.280 @@ -632,12 +625,9 @@
   1.281  next
   1.282    case (pCons c cs)
   1.283    {
   1.284 -    assume C: "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   1.285 -    {
   1.286 -      fix x y
   1.287 -      from C have "poly (pCons c cs) x = poly (pCons c cs) y"
   1.288 -        by (cases "x = 0") auto
   1.289 -    }
   1.290 +    assume "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   1.291 +    then have "poly (pCons c cs) x = poly (pCons c cs) y" for x y
   1.292 +      by (cases "x = 0") auto
   1.293      with pCons.prems have False
   1.294        by (auto simp add: constant_def)
   1.295    }
   1.296 @@ -653,7 +643,7 @@
   1.297      done
   1.298  qed
   1.299  
   1.300 -text{* Fundamental theorem of algebra *}
   1.301 +text \<open>Fundamental theorem of algebra\<close>
   1.302  
   1.303  lemma fundamental_theorem_of_algebra:
   1.304    assumes nc: "\<not> constant (poly p)"
   1.305 @@ -674,26 +664,25 @@
   1.306      then show ?thesis by blast
   1.307    next
   1.308      case False
   1.309 -    note pc0 = this
   1.310      from poly_offset[of p c] obtain q where q: "psize q = psize p" "\<forall>x. poly q x = ?p (c + x)"
   1.311        by blast
   1.312 -    {
   1.313 -      assume h: "constant (poly q)"
   1.314 +    have False if h: "constant (poly q)"
   1.315 +    proof -
   1.316        from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
   1.317          by auto
   1.318 -      {
   1.319 -        fix x y
   1.320 +      have "?p x = ?p y" for x y
   1.321 +      proof -
   1.322          from th have "?p x = poly q (x - c)"
   1.323            by auto
   1.324          also have "\<dots> = poly q (y - c)"
   1.325            using h unfolding constant_def by blast
   1.326          also have "\<dots> = ?p y"
   1.327            using th by auto
   1.328 -        finally have "?p x = ?p y" .
   1.329 -      }
   1.330 -      with less(2) have False
   1.331 +        finally show ?thesis .
   1.332 +      qed
   1.333 +      with less(2) show ?thesis
   1.334          unfolding constant_def by blast
   1.335 -    }
   1.336 +    qed
   1.337      then have qnc: "\<not> constant (poly q)"
   1.338        by blast
   1.339      from q(2) have pqc0: "?p c = poly q 0"
   1.340 @@ -701,7 +690,7 @@
   1.341      from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)"
   1.342        by simp
   1.343      let ?a0 = "poly q 0"
   1.344 -    from pc0 pqc0 have a00: "?a0 \<noteq> 0"
   1.345 +    from False pqc0 have a00: "?a0 \<noteq> 0"
   1.346        by simp
   1.347      from a00 have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   1.348        by simp
   1.349 @@ -710,8 +699,8 @@
   1.350        using a00
   1.351        unfolding psize_def degree_def
   1.352        by (simp add: poly_eq_iff)
   1.353 -    {
   1.354 -      assume h: "\<And>x y. poly ?r x = poly ?r y"
   1.355 +    have False if h: "\<And>x y. poly ?r x = poly ?r y"
   1.356 +    proof -
   1.357        {
   1.358          fix x y
   1.359          from qr[rule_format, of x] have "poly q x = poly ?r x * ?a0"
   1.360 @@ -722,41 +711,35 @@
   1.361            using qr[rule_format, of y] by simp
   1.362          finally have "poly q x = poly q y" .
   1.363        }
   1.364 -      with qnc have False
   1.365 +      with qnc show ?thesis
   1.366          unfolding constant_def by blast
   1.367 -    }
   1.368 +    qed
   1.369      then have rnc: "\<not> constant (poly ?r)"
   1.370        unfolding constant_def by blast
   1.371      from qr[rule_format, of 0] a00 have r01: "poly ?r 0 = 1"
   1.372        by auto
   1.373 -    {
   1.374 -      fix w
   1.375 +    have mrmq_eq: "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" for w
   1.376 +    proof -
   1.377        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   1.378          using qr[rule_format, of w] a00 by (simp add: divide_inverse ac_simps)
   1.379        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   1.380          using a00 unfolding norm_divide by (simp add: field_simps)
   1.381 -      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .
   1.382 -    }
   1.383 -    note mrmq_eq = this
   1.384 +      finally show ?thesis .
   1.385 +    qed
   1.386      from poly_decompose[OF rnc] obtain k a s where
   1.387        kas: "a \<noteq> 0" "k \<noteq> 0" "psize s + k + 1 = psize ?r"
   1.388          "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   1.389 -    {
   1.390 -      assume "psize p = k + 1"
   1.391 +    have "\<exists>w. cmod (poly ?r w) < 1"
   1.392 +    proof (cases "psize p = k + 1")
   1.393 +      case True
   1.394        with kas(3) lgqr[symmetric] q(1) have s0: "s = 0"
   1.395          by auto
   1.396 -      {
   1.397 -        fix w
   1.398 -        have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
   1.399 -          using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
   1.400 -      }
   1.401 -      note hth = this [symmetric]
   1.402 -      from reduce_poly_simple[OF kas(1,2)] have "\<exists>w. cmod (poly ?r w) < 1"
   1.403 +      have hth[symmetric]: "cmod (poly ?r w) = cmod (1 + a * w ^ k)" for w
   1.404 +        using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)
   1.405 +      from reduce_poly_simple[OF kas(1,2)] show ?thesis
   1.406          unfolding hth by blast
   1.407 -    }
   1.408 -    moreover
   1.409 -    {
   1.410 -      assume kn: "psize p \<noteq> k + 1"
   1.411 +    next
   1.412 +      case False note kn = this
   1.413        from kn kas(3) q(1) lgqr have k1n: "k + 1 < psize p"
   1.414          by simp
   1.415        have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   1.416 @@ -827,17 +810,15 @@
   1.417          by arith
   1.418        then have "cmod (poly ?r ?w) < 1"
   1.419          unfolding kas(4)[rule_format, of ?w] r01 by simp
   1.420 -      then have "\<exists>w. cmod (poly ?r w) < 1"
   1.421 +      then show ?thesis
   1.422          by blast
   1.423 -    }
   1.424 -    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1"
   1.425 -      by blast
   1.426 -    from cr0_contr cq0 q(2) show ?thesis
   1.427 +    qed
   1.428 +    with cq0 q(2) show ?thesis
   1.429        unfolding mrmq_eq not_less[symmetric] by auto
   1.430    qed
   1.431  qed
   1.432  
   1.433 -text {* Alternative version with a syntactic notion of constant polynomial. *}
   1.434 +text \<open>Alternative version with a syntactic notion of constant polynomial.\<close>
   1.435  
   1.436  lemma fundamental_theorem_of_algebra_alt:
   1.437    assumes nc: "\<not> (\<exists>a l. a \<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
   1.438 @@ -867,17 +848,19 @@
   1.439          show ?case
   1.440          proof (cases "d = 0")
   1.441            case True
   1.442 -          then show ?thesis using pCons.prems pCons.hyps by simp
   1.443 +          then show ?thesis
   1.444 +            using pCons.prems pCons.hyps by simp
   1.445          next
   1.446            case False
   1.447            from poly_bound_exists[of 1 ds] obtain m where
   1.448              m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   1.449            have dm: "cmod d / m > 0"
   1.450              using False m(1) by (simp add: field_simps)
   1.451 -          from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
   1.452 -            x: "x > 0" "x < cmod d / m" "x < 1" by blast
   1.453 +          from real_lbound_gt_zero[OF dm zero_less_one]
   1.454 +          obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
   1.455 +            by blast
   1.456            let ?x = "complex_of_real x"
   1.457 -          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1"
   1.458 +          from x have cx: "?x \<noteq> 0" "cmod ?x \<le> 1"
   1.459              by simp_all
   1.460            from pCons.prems[rule_format, OF cx(1)]
   1.461            have cth: "cmod (?x*poly ds ?x) = cmod d"
   1.462 @@ -901,7 +884,7 @@
   1.463  qed
   1.464  
   1.465  
   1.466 -subsection{* Nullstellensatz, degrees and divisibility of polynomials *}
   1.467 +subsection \<open>Nullstellensatz, degrees and divisibility of polynomials\<close>
   1.468  
   1.469  lemma nullstellensatz_lemma:
   1.470    fixes p :: "complex poly"
   1.471 @@ -924,28 +907,28 @@
   1.472    {
   1.473      fix a
   1.474      assume a: "poly p a = 0"
   1.475 -    {
   1.476 -      assume oa: "order a p \<noteq> 0"
   1.477 +    have ?ths if oa: "order a p \<noteq> 0"
   1.478 +    proof -
   1.479        let ?op = "order a p"
   1.480        from pne have ap: "([:- a, 1:] ^ ?op) dvd p" "\<not> [:- a, 1:] ^ (Suc ?op) dvd p"
   1.481          using order by blast+
   1.482        note oop = order_degree[OF pne, unfolded dpn]
   1.483 -      {
   1.484 -        assume q0: "q = 0"
   1.485 -        then have ?ths using n0
   1.486 -          by (simp add: power_0_left)
   1.487 -      }
   1.488 -      moreover
   1.489 -      {
   1.490 -        assume q0: "q \<noteq> 0"
   1.491 +      show ?thesis
   1.492 +      proof (cases "q = 0")
   1.493 +        case True
   1.494 +        with n0 show ?thesis by (simp add: power_0_left)
   1.495 +      next
   1.496 +        case False
   1.497          from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
   1.498          obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
   1.499          from ap(1) obtain s where s: "p = [:- a, 1:] ^ ?op * s"
   1.500            by (rule dvdE)
   1.501 -        have sne: "s \<noteq> 0" using s pne by auto
   1.502 -        {
   1.503 -          assume ds0: "degree s = 0"
   1.504 -          from ds0 obtain k where kpn: "s = [:k:]"
   1.505 +        have sne: "s \<noteq> 0"
   1.506 +          using s pne by auto
   1.507 +        show ?thesis
   1.508 +        proof (cases "degree s = 0")
   1.509 +          case True
   1.510 +          then obtain k where kpn: "s = [:k:]"
   1.511              by (cases s) (auto split: if_splits)
   1.512            from sne kpn have k: "k \<noteq> 0" by simp
   1.513            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   1.514 @@ -959,14 +942,11 @@
   1.515              apply (subst power_add [symmetric])
   1.516              apply simp
   1.517              done
   1.518 -          then have ?ths
   1.519 +          then show ?thesis
   1.520              unfolding dvd_def by blast
   1.521 -        }
   1.522 -        moreover
   1.523 -        {
   1.524 -          assume ds0: "degree s \<noteq> 0"
   1.525 -          from ds0 sne dpn s oa
   1.526 -            have dsn: "degree s < n"
   1.527 +        next
   1.528 +          case False
   1.529 +          with sne dpn s oa have dsn: "degree s < n"
   1.530                apply auto
   1.531                apply (erule ssubst)
   1.532                apply (simp add: degree_mult_eq degree_linear_power)
   1.533 @@ -994,7 +974,7 @@
   1.534                  by auto
   1.535              }
   1.536              note impth = this
   1.537 -            from IH[rule_format, OF dsn, of s r] impth ds0
   1.538 +            from IH[rule_format, OF dsn, of s r] impth False
   1.539              have "s dvd (r ^ (degree s))"
   1.540                by blast
   1.541              then obtain u where u: "r ^ (degree s) = s * u" ..
   1.542 @@ -1012,13 +992,11 @@
   1.543                apply (subst u [symmetric])
   1.544                apply (simp add: ac_simps power_add [symmetric])
   1.545                done
   1.546 -            then have ?ths
   1.547 +            then show ?thesis
   1.548                unfolding dvd_def by blast
   1.549 -        }
   1.550 -        ultimately have ?ths by blast
   1.551 -      }
   1.552 -      ultimately have ?ths by blast
   1.553 -    }
   1.554 +        qed
   1.555 +      qed
   1.556 +    qed
   1.557      then have ?ths using a order_root pne by blast
   1.558    }
   1.559    moreover
   1.560 @@ -1042,34 +1020,33 @@
   1.561    "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
   1.562      p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
   1.563  proof -
   1.564 -  {
   1.565 -    assume pe: "p = 0"
   1.566 +  show ?thesis
   1.567 +  proof (cases "p = 0")
   1.568 +    case True
   1.569      then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
   1.570        by (auto simp add: poly_all_0_iff_0)
   1.571      {
   1.572        assume "p dvd (q ^ (degree p))"
   1.573        then obtain r where r: "q ^ (degree p) = p * r" ..
   1.574 -      from r pe have False by simp
   1.575 +      from r True have False by simp
   1.576      }
   1.577 -    with eq pe have ?thesis by blast
   1.578 -  }
   1.579 -  moreover
   1.580 -  {
   1.581 -    assume pe: "p \<noteq> 0"
   1.582 -    {
   1.583 -      assume dp: "degree p = 0"
   1.584 -      then obtain k where k: "p = [:k:]" "k \<noteq> 0" using pe
   1.585 +    with eq True show ?thesis by blast
   1.586 +  next
   1.587 +    case False
   1.588 +    show ?thesis
   1.589 +    proof (cases "degree p = 0")
   1.590 +      case True
   1.591 +      with \<open>p \<noteq> 0\<close> obtain k where k: "p = [:k:]" "k \<noteq> 0"
   1.592          by (cases p) (simp split: if_splits)
   1.593        then have th1: "\<forall>x. poly p x \<noteq> 0"
   1.594          by simp
   1.595 -      from k dp have "q ^ (degree p) = p * [:1/k:]"
   1.596 +      from k True have "q ^ (degree p) = p * [:1/k:]"
   1.597          by (simp add: one_poly_def)
   1.598        then have th2: "p dvd (q ^ (degree p))" ..
   1.599 -      from th1 th2 pe have ?thesis
   1.600 +      from False th1 th2 show ?thesis
   1.601          by blast
   1.602 -    }
   1.603 -    moreover
   1.604 -    {
   1.605 +    next
   1.606 +      case False
   1.607        assume dp: "degree p \<noteq> 0"
   1.608        then obtain n where n: "degree p = Suc n "
   1.609          by (cases "degree p") auto
   1.610 @@ -1086,14 +1063,12 @@
   1.611          }
   1.612        }
   1.613        with n nullstellensatz_lemma[of p q "degree p"] dp
   1.614 -      have ?thesis by auto
   1.615 -    }
   1.616 -    ultimately have ?thesis by blast
   1.617 -  }
   1.618 -  ultimately show ?thesis by blast
   1.619 +      show ?thesis by auto
   1.620 +    qed
   1.621 +  qed
   1.622  qed
   1.623  
   1.624 -text {* Useful lemma *}
   1.625 +text \<open>Useful lemma\<close>
   1.626  
   1.627  lemma constant_degree:
   1.628    fixes p :: "'a::{idom,ring_char_0} poly"
   1.629 @@ -1122,7 +1097,7 @@
   1.630    shows "degree p \<le> degree q \<or> q = 0"
   1.631    by (metis dvd_imp_degree_le pq)
   1.632  
   1.633 -text {* Arithmetic operations on multivariate polynomials. *}
   1.634 +text \<open>Arithmetic operations on multivariate polynomials.\<close>
   1.635  
   1.636  lemma mpoly_base_conv:
   1.637    fixes x :: "'a::comm_ring_1"
   1.638 @@ -1215,11 +1190,8 @@
   1.639    assumes l: "p \<noteq> 0"
   1.640    shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
   1.641  proof -
   1.642 -  {
   1.643 -    fix h t
   1.644 -    assume h: "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t"
   1.645 -    with l have False by simp
   1.646 -  }
   1.647 +  have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
   1.648 +    using l prems by simp
   1.649    then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
   1.650      by blast
   1.651    from fundamental_theorem_of_algebra_alt[OF th] show ?thesis