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