author wenzelm Tue Apr 29 21:54:26 2014 +0200 (2014-04-29) changeset 56795 e8cce2bd23e5 parent 56794 a7c5c35b7125 child 56796 9f84219715a7
tuned proofs;
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.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.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.84  lemma bolzano_weierstrass_complex_disc:
1.85 @@ -374,12 +386,12 @@
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.261  text {* Decomposition of polynomial, skipping zero coefficients
1.262 @@ -705,8 +721,7 @@
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.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.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.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.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.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.305 -      with qnc have False unfolding constant_def by blast
1.306 +      with qnc have False
1.307 +        unfolding constant_def by blast
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.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.391          moreover
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.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.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.441          ultimately have ?ths by blast
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.451      moreover
1.453 @@ -1181,7 +1222,7 @@
1.454    ultimately show ?thesis by blast
1.455  qed
1.457 -text{* Useful lemma *}
1.458 +text {* Useful lemma *}
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.466 -(* Arithmetic operations on multivariate polynomials.                        *)
1.467 +text {* Arithmetic operations on multivariate polynomials. *}
1.469  lemma mpoly_base_conv:
1.470    fixes x :: "'a::comm_ring_1"
1.471 @@ -1232,7 +1273,7 @@
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.480 @@ -1300,8 +1341,8 @@
1.481    by simp_all
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.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)