src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 56795 e8cce2bd23e5
parent 56778 cb0929421ca6
child 56889 48a745e1bde7
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 29 21:29:36 2014 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Apr 29 21:54:26 2014 +0200
     1.3 @@ -139,15 +139,16 @@
     1.4    from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
     1.5      by blast
     1.6    let ?k = " 1 + norm c + \<bar>r * m\<bar>"
     1.7 -  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
     1.8 +  have kp: "?k > 0"
     1.9 +    using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
    1.10    {
    1.11      fix z :: 'a
    1.12      assume H: "norm z \<le> r"
    1.13      from m H have th: "norm (poly cs z) \<le> m"
    1.14        by blast
    1.15 -    from H have rp: "r \<ge> 0" using norm_ge_zero[of z]
    1.16 -      by arith
    1.17 -    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
    1.18 +    from H have rp: "r \<ge> 0"
    1.19 +      using norm_ge_zero[of z] by arith
    1.20 +    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z * poly cs z)"
    1.21        using norm_triangle_ineq[of c "z* poly cs z"] by simp
    1.22      also have "\<dots> \<le> norm c + r * m"
    1.23        using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
    1.24 @@ -187,7 +188,8 @@
    1.25  
    1.26  lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
    1.27    apply (safe intro!: offset_poly_0)
    1.28 -  apply (induct p, simp)
    1.29 +  apply (induct p)
    1.30 +  apply simp
    1.31    apply (simp add: offset_poly_pCons)
    1.32    apply (frule offset_poly_eq_0_lemma, simp)
    1.33    done
    1.34 @@ -278,7 +280,8 @@
    1.35        by presburger+
    1.36      with IH[rule_format, of m] obtain z where z: "?P z m"
    1.37        by blast
    1.38 -    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
    1.39 +    from z have "?P (csqrt z) n"
    1.40 +      by (simp add: m power_mult csqrt)
    1.41      then have "\<exists>z. ?P z n" ..
    1.42    }
    1.43    moreover
    1.44 @@ -288,16 +291,25 @@
    1.45        using b by (simp add: norm_divide)
    1.46      from o have "\<exists>m. n = Suc (2 * m)"
    1.47        by presburger+
    1.48 -    then obtain m where m: "n = Suc (2*m)"
    1.49 +    then obtain m where m: "n = Suc (2 * m)"
    1.50        by blast
    1.51      from unimodular_reduce_norm[OF th0] o
    1.52      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
    1.53 -      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
    1.54 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp)
    1.55 +      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
    1.56 +      apply (rule_tac x="1" in exI)
    1.57 +      apply simp
    1.58 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1")
    1.59 +      apply (rule_tac x="-1" in exI)
    1.60 +      apply simp
    1.61        apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
    1.62 -      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
    1.63 -      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
    1.64 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
    1.65 +      apply (cases "even m")
    1.66 +      apply (rule_tac x="ii" in exI)
    1.67 +      apply (simp add: m power_mult)
    1.68 +      apply (rule_tac x="- ii" in exI)
    1.69 +      apply (simp add: m power_mult)
    1.70 +      apply (cases "even m")
    1.71 +      apply (rule_tac x="- ii" in exI)
    1.72 +      apply (simp add: m power_mult)
    1.73        apply (auto simp add: m power_mult)
    1.74        apply (rule_tac x="ii" in exI)
    1.75        apply (auto simp add: m power_mult)
    1.76 @@ -329,7 +341,7 @@
    1.77  text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
    1.78  
    1.79  lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
    1.80 -  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
    1.81 +  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
    1.82    unfolding cmod_def by simp
    1.83  
    1.84  lemma bolzano_weierstrass_complex_disc:
    1.85 @@ -374,12 +386,12 @@
    1.86  
    1.87    from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
    1.88      by blast
    1.89 -  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
    1.90 +  then have x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Re (s (f n)) - x\<bar> < r"
    1.91      unfolding LIMSEQ_iff real_norm_def .
    1.92  
    1.93    from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
    1.94      by blast
    1.95 -  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
    1.96 +  then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
    1.97      unfolding LIMSEQ_iff real_norm_def .
    1.98    let ?w = "Complex x y"
    1.99    from f(1) g(1) have hs: "subseq ?h"
   1.100 @@ -387,10 +399,12 @@
   1.101    {
   1.102      fix e :: real
   1.103      assume ep: "e > 0"
   1.104 -    then have e2: "e/2 > 0" by simp
   1.105 +    then have e2: "e/2 > 0"
   1.106 +      by simp
   1.107      from x[rule_format, OF e2] y[rule_format, OF e2]
   1.108      obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2"
   1.109 -      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
   1.110 +      and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2"
   1.111 +      by blast
   1.112      {
   1.113        fix n
   1.114        assume nN12: "n \<ge> N1 + N2"
   1.115 @@ -400,7 +414,8 @@
   1.116        have "cmod (s (?h n) - ?w) < e"
   1.117          using metric_bound_lemma[of "s (f (g n))" ?w] by simp
   1.118      }
   1.119 -    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast
   1.120 +    then have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e"
   1.121 +      by blast
   1.122    }
   1.123    with hs show ?thesis by blast
   1.124  qed
   1.125 @@ -514,7 +529,8 @@
   1.126        let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
   1.127        {
   1.128          assume e: "?e > 0"
   1.129 -        then have e2: "?e/2 > 0" by simp
   1.130 +        then have e2: "?e/2 > 0"
   1.131 +          by simp
   1.132          from poly_cont[OF e2, of z p] obtain d where
   1.133              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.134            by blast
   1.135 @@ -541,25 +557,25 @@
   1.136          have ath: "\<And>m x e::real. m \<le> x \<Longrightarrow> x < m + e \<Longrightarrow> \<bar>x - m\<bar> < e"
   1.137            by arith
   1.138          from s1m[OF g(1)[rule_format]] have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   1.139 -        from seq_suble[OF fz(1), of "N1+N2"]
   1.140 +        from seq_suble[OF fz(1), of "N1 + N2"]
   1.141          have th00: "real (Suc (N1 + N2)) \<le> real (Suc (f (N1 + N2)))"
   1.142            by simp
   1.143          have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1 + N2)) > 0"
   1.144            using N2 by auto
   1.145          from frac_le[OF th000 th00]
   1.146 -        have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
   1.147 +        have th00: "?m + 1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))"
   1.148            by simp
   1.149          from g(2)[rule_format, of "f (N1 + N2)"]
   1.150          have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
   1.151          from order_less_le_trans[OF th01 th00]
   1.152 -        have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
   1.153 +        have th32: "cmod (poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
   1.154          from N2 have "2/?e < real (Suc (N1 + N2))"
   1.155            by arith
   1.156          with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   1.157          have "?e/2 > 1/ real (Suc (N1 + N2))"
   1.158            by (simp add: inverse_eq_divide)
   1.159          with ath[OF th31 th32]
   1.160 -        have thc1: "\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
   1.161 +        have thc1: "\<bar>cmod (poly p (g (f (N1 + N2)))) - ?m\<bar> < ?e/2"
   1.162            by arith
   1.163          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.164            by arith
   1.165 @@ -593,7 +609,7 @@
   1.166  lemma cispi: "cis pi = -1"
   1.167    by (simp add: cis_def)
   1.168  
   1.169 -lemma "(rcis (sqrt (abs r)) ((pi + a)/2))\<^sup>2 = rcis (- abs r) a"
   1.170 +lemma "(rcis (sqrt (abs r)) ((pi + a) / 2))\<^sup>2 = rcis (- abs r) a"
   1.171    unfolding power2_eq_square
   1.172    apply (simp add: rcis_mult add_divide_distrib)
   1.173    apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
   1.174 @@ -607,16 +623,21 @@
   1.175    shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
   1.176    using ex
   1.177  proof (induct p arbitrary: a d)
   1.178 +  case 0
   1.179 +  then show ?case by simp
   1.180 +next
   1.181    case (pCons c cs a d)
   1.182 -  {
   1.183 -    assume H: "cs \<noteq> 0"
   1.184 +  show ?case
   1.185 +  proof (cases "cs = 0")
   1.186 +    case False
   1.187      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.188        by blast
   1.189      let ?r = "1 + \<bar>r\<bar>"
   1.190      {
   1.191 -      fix z::'a
   1.192 +      fix z :: 'a
   1.193        assume h: "1 + \<bar>r\<bar> \<le> norm z"
   1.194 -      have r0: "r \<le> norm z" using h by arith
   1.195 +      have r0: "r \<le> norm z"
   1.196 +        using h by arith
   1.197        from r[rule_format, OF r0] have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)"
   1.198          by arith
   1.199        from h have z1: "norm z \<ge> 1"
   1.200 @@ -625,21 +646,18 @@
   1.201        have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
   1.202          unfolding norm_mult by (simp add: algebra_simps)
   1.203        from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
   1.204 -      have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.205 +      have th2: "norm (z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.206          by (simp add: algebra_simps)
   1.207 -      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)" by arith
   1.208 +      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.209 +        by arith
   1.210      }
   1.211 -    then have ?case by blast
   1.212 -  }
   1.213 -  moreover
   1.214 -  {
   1.215 -    assume cs0: "\<not> (cs \<noteq> 0)"
   1.216 +    then show ?thesis by blast
   1.217 +  next
   1.218 +    case True
   1.219      with pCons.prems have c0: "c \<noteq> 0"
   1.220        by simp
   1.221 -    from cs0 have cs0': "cs = 0"
   1.222 -      by simp
   1.223      {
   1.224 -      fix z::'a
   1.225 +      fix z :: 'a
   1.226        assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
   1.227        from c0 have "norm c > 0"
   1.228          by simp
   1.229 @@ -650,12 +668,11 @@
   1.230        from norm_diff_ineq[of "z * c" a] have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
   1.231          by (simp add: algebra_simps)
   1.232        from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
   1.233 -        using cs0' by simp
   1.234 +        using True by simp
   1.235      }
   1.236 -    then have ?case  by blast
   1.237 -  }
   1.238 -  ultimately show ?case by blast
   1.239 -qed simp
   1.240 +    then show ?thesis by blast
   1.241 +  qed
   1.242 +qed
   1.243  
   1.244  text {* Hence polynomial's modulus attains its minimum somewhere. *}
   1.245  lemma poly_minimum_modulus: "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   1.246 @@ -691,13 +708,12 @@
   1.247  qed
   1.248  
   1.249  text{* Constant function (non-syntactic characterization). *}
   1.250 -definition "constant f = (\<forall>x y. f x = f y)"
   1.251 +definition "constant f \<longleftrightarrow> (\<forall>x y. f x = f y)"
   1.252  
   1.253  lemma nonconstant_length: "\<not> constant (poly p) \<Longrightarrow> psize p \<ge> 2"
   1.254    by (induct p) (auto simp: constant_def psize_def)
   1.255  
   1.256 -lemma poly_replicate_append:
   1.257 -  "poly (monom 1 n * p) (x::'a::{comm_ring_1}) = x^n * poly p x"
   1.258 +lemma poly_replicate_append: "poly (monom 1 n * p) (x::'a::comm_ring_1) = x^n * poly p x"
   1.259    by (simp add: poly_monom)
   1.260  
   1.261  text {* Decomposition of polynomial, skipping zero coefficients
   1.262 @@ -705,8 +721,7 @@
   1.263  
   1.264  lemma poly_decompose_lemma:
   1.265    assumes nz: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly p z = (0::'a::idom))"
   1.266 -  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and>
   1.267 -    (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   1.268 +  shows "\<exists>k a q. a \<noteq> 0 \<and> Suc (psize q + k) = psize p \<and> (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   1.269    unfolding psize_def
   1.270    using nz
   1.271  proof (induct p)
   1.272 @@ -746,7 +761,7 @@
   1.273  next
   1.274    case (pCons c cs)
   1.275    {
   1.276 -    assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   1.277 +    assume C: "\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   1.278      {
   1.279        fix x y
   1.280        from C have "poly (pCons c cs) x = poly (pCons c cs) y"
   1.281 @@ -793,13 +808,16 @@
   1.282        by blast
   1.283      {
   1.284        assume h: "constant (poly q)"
   1.285 -      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
   1.286 +      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x"
   1.287 +        by auto
   1.288        {
   1.289          fix x y
   1.290 -        from th have "?p x = poly q (x - c)" by auto
   1.291 +        from th have "?p x = poly q (x - c)"
   1.292 +          by auto
   1.293          also have "\<dots> = poly q (y - c)"
   1.294            using h unfolding constant_def by blast
   1.295 -        also have "\<dots> = ?p y" using th by auto
   1.296 +        also have "\<dots> = ?p y"
   1.297 +          using th by auto
   1.298          finally have "?p x = ?p y" .
   1.299        }
   1.300        with less(2) have False
   1.301 @@ -833,7 +851,8 @@
   1.302            using qr[rule_format, of y] by simp
   1.303          finally have "poly q x = poly q y" .
   1.304        }
   1.305 -      with qnc have False unfolding constant_def by blast
   1.306 +      with qnc have False
   1.307 +        unfolding constant_def by blast
   1.308      }
   1.309      then have rnc: "\<not> constant (poly ?r)"
   1.310        unfolding constant_def by blast
   1.311 @@ -871,7 +890,8 @@
   1.312          by simp
   1.313        have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   1.314          unfolding constant_def poly_pCons poly_monom
   1.315 -        using kas(1) apply simp
   1.316 +        using kas(1)
   1.317 +        apply simp
   1.318          apply (rule exI[where x=0])
   1.319          apply (rule exI[where x=1])
   1.320          apply simp
   1.321 @@ -884,8 +904,8 @@
   1.322          using kas(2) by (cases k) (auto simp add: algebra_simps)
   1.323        from poly_bound_exists[of "cmod w" s] obtain m where
   1.324          m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   1.325 -      have w0: "w \<noteq> 0" using kas(2) w
   1.326 -        by (auto simp add: power_0_left)
   1.327 +      have w0: "w \<noteq> 0"
   1.328 +        using kas(2) w by (auto simp add: power_0_left)
   1.329        from w have "(1 + w ^ k * a) - 1 = 0 - 1"
   1.330          by simp
   1.331        then have wm1: "w^k * a = - 1"
   1.332 @@ -981,24 +1001,30 @@
   1.333            case False
   1.334            from poly_bound_exists[of 1 ds] obtain m where
   1.335              m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   1.336 -          have dm: "cmod d / m > 0" using False m(1) by (simp add: field_simps)
   1.337 +          have dm: "cmod d / m > 0"
   1.338 +            using False m(1) by (simp add: field_simps)
   1.339            from real_lbound_gt_zero[OF dm zero_less_one] obtain x where
   1.340              x: "x > 0" "x < cmod d / m" "x < 1" by blast
   1.341            let ?x = "complex_of_real x"
   1.342 -          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
   1.343 +          from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1"
   1.344 +            by simp_all
   1.345            from pCons.prems[rule_format, OF cx(1)]
   1.346 -          have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
   1.347 +          have cth: "cmod (?x*poly ds ?x) = cmod d"
   1.348 +            by (simp add: eq_diff_eq[symmetric])
   1.349            from m(2)[rule_format, OF cx(2)] x(1)
   1.350            have th0: "cmod (?x*poly ds ?x) \<le> x*m"
   1.351              by (simp add: norm_mult)
   1.352 -          from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
   1.353 -          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
   1.354 -          with cth show ?thesis by blast
   1.355 +          from x(2) m(1) have "x * m < cmod d"
   1.356 +            by (simp add: field_simps)
   1.357 +          with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d"
   1.358 +            by auto
   1.359 +          with cth show ?thesis
   1.360 +            by blast
   1.361          qed
   1.362        qed
   1.363      }
   1.364 -    then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems False
   1.365 -      by blast
   1.366 +    then have nc: "\<not> constant (poly (pCons c cs))"
   1.367 +      using pCons.prems False by blast
   1.368      from fundamental_theorem_of_algebra[OF nc] show ?thesis .
   1.369    qed
   1.370  qed
   1.371 @@ -1053,12 +1079,17 @@
   1.372            from sne kpn have k: "k \<noteq> 0" by simp
   1.373            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
   1.374            have "q ^ n = p * ?w"
   1.375 -            apply (subst r, subst s, subst kpn)
   1.376 +            apply (subst r)
   1.377 +            apply (subst s)
   1.378 +            apply (subst kpn)
   1.379              using k oop [of a]
   1.380 -            apply (subst power_mult_distrib, simp)
   1.381 -            apply (subst power_add [symmetric], simp)
   1.382 +            apply (subst power_mult_distrib)
   1.383 +            apply simp
   1.384 +            apply (subst power_add [symmetric])
   1.385 +            apply simp
   1.386              done
   1.387 -          then have ?ths unfolding dvd_def by blast
   1.388 +          then have ?ths
   1.389 +            unfolding dvd_def by blast
   1.390          }
   1.391          moreover
   1.392          {
   1.393 @@ -1076,25 +1107,33 @@
   1.394                  from h[unfolded xa poly_eq_0_iff_dvd] obtain u where u: "s = [:- a, 1:] * u"
   1.395                    by (rule dvdE)
   1.396                  have "p = [:- a, 1:] ^ (Suc ?op) * u"
   1.397 -                  by (subst s, subst u, simp only: power_Suc mult_ac)
   1.398 -                with ap(2)[unfolded dvd_def] have False by blast
   1.399 +                  apply (subst s)
   1.400 +                  apply (subst u)
   1.401 +                  apply (simp only: power_Suc mult_ac)
   1.402 +                  done
   1.403 +                with ap(2)[unfolded dvd_def] have False
   1.404 +                  by blast
   1.405                }
   1.406                note xa = this
   1.407 -              from h have "poly p x = 0" by (subst s) simp
   1.408 -              with pq0 have "poly q x = 0" by blast
   1.409 +              from h have "poly p x = 0"
   1.410 +                by (subst s) simp
   1.411 +              with pq0 have "poly q x = 0"
   1.412 +                by blast
   1.413                with r xa have "poly r x = 0"
   1.414                  by auto
   1.415              }
   1.416              note impth = this
   1.417              from IH[rule_format, OF dsn, of s r] impth ds0
   1.418 -            have "s dvd (r ^ (degree s))" by blast
   1.419 +            have "s dvd (r ^ (degree s))"
   1.420 +              by blast
   1.421              then obtain u where u: "r ^ (degree s) = s * u" ..
   1.422              then have u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
   1.423                by (simp only: poly_mult[symmetric] poly_power[symmetric])
   1.424              let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
   1.425              from oop[of a] dsn have "q ^ n = p * ?w"
   1.426                apply -
   1.427 -              apply (subst s, subst r)
   1.428 +              apply (subst s)
   1.429 +              apply (subst r)
   1.430                apply (simp only: power_mult_distrib)
   1.431                apply (subst mult_assoc [where b=s])
   1.432                apply (subst mult_assoc [where a=u])
   1.433 @@ -1102,7 +1141,8 @@
   1.434                apply (subst u [symmetric])
   1.435                apply (simp add: mult_ac power_add [symmetric])
   1.436                done
   1.437 -            then have ?ths unfolding dvd_def by blast
   1.438 +            then have ?ths
   1.439 +              unfolding dvd_def by blast
   1.440          }
   1.441          ultimately have ?ths by blast
   1.442        }
   1.443 @@ -1154,7 +1194,8 @@
   1.444        from k dp have "q ^ (degree p) = p * [:1/k:]"
   1.445          by (simp add: one_poly_def)
   1.446        then have th2: "p dvd (q ^ (degree p))" ..
   1.447 -      from th1 th2 pe have ?thesis by blast
   1.448 +      from th1 th2 pe have ?thesis
   1.449 +        by blast
   1.450      }
   1.451      moreover
   1.452      {
   1.453 @@ -1181,7 +1222,7 @@
   1.454    ultimately show ?thesis by blast
   1.455  qed
   1.456  
   1.457 -text{* Useful lemma *}
   1.458 +text {* Useful lemma *}
   1.459  
   1.460  lemma constant_degree:
   1.461    fixes p :: "'a::{idom,ring_char_0} poly"
   1.462 @@ -1210,7 +1251,7 @@
   1.463    shows "degree p \<le> degree q \<or> q = 0"
   1.464    by (metis dvd_imp_degree_le pq)
   1.465  
   1.466 -(* Arithmetic operations on multivariate polynomials.                        *)
   1.467 +text {* Arithmetic operations on multivariate polynomials. *}
   1.468  
   1.469  lemma mpoly_base_conv:
   1.470    fixes x :: "'a::comm_ring_1"
   1.471 @@ -1232,7 +1273,7 @@
   1.472  
   1.473  lemma poly_cancel_eq_conv:
   1.474    fixes x :: "'a::field"
   1.475 -  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
   1.476 +  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> y = 0 \<longleftrightarrow> a * y - b * x = 0"
   1.477    by auto
   1.478  
   1.479  lemma poly_divides_pad_rule:
   1.480 @@ -1300,8 +1341,8 @@
   1.481    by simp_all
   1.482  
   1.483  lemma basic_cqe_conv2:
   1.484 -  assumes l:"p \<noteq> 0"
   1.485 -  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex))"
   1.486 +  assumes l: "p \<noteq> 0"
   1.487 +  shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
   1.488  proof -
   1.489    {
   1.490      fix h t
   1.491 @@ -1320,7 +1361,7 @@
   1.492  lemma basic_cqe_conv3:
   1.493    fixes p q :: "complex poly"
   1.494    assumes l: "p \<noteq> 0"
   1.495 -  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> ((pCons a p) dvd (q ^ psize p))"
   1.496 +  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<longleftrightarrow> \<not> (pCons a p) dvd (q ^ psize p)"
   1.497  proof -
   1.498    from l have dp: "degree (pCons a p) = psize p"
   1.499      by (simp add: psize_def)