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
```