src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 32960 69916a850301 parent 32456 341c83339aeb child 34915 7894c7dab132
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -20,11 +20,11 @@
1.4    {assume y0: "y = 0"
1.5      {assume x0: "x \<ge> 0"
1.6        then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.7 -	by (simp add: csqrt_def power2_eq_square)}
1.8 +        by (simp add: csqrt_def power2_eq_square)}
1.9      moreover
1.10      {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
1.11        then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
1.12 -	by (simp add: csqrt_def power2_eq_square) }
1.13 +        by (simp add: csqrt_def power2_eq_square) }
1.14      ultimately have ?thesis by blast}
1.15    moreover
1.16    {assume y0: "y\<noteq>0"
1.17 @@ -322,7 +322,7 @@
1.18        hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
1.19        from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
1.20        have "cmod (s (?h n) - ?w) < e"
1.21 -	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
1.22 +        using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
1.23      hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
1.24    with hs show ?thesis  by blast
1.25  qed
1.26 @@ -358,13 +358,13 @@
1.27        by (simp_all add: field_simps real_mult_order)
1.28      show ?case
1.29        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
1.30 -	fix d w
1.31 -	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
1.32 -	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.33 -	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
1.34 -	from H have th: "cmod (w-z) \<le> d" by simp
1.35 -	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
1.36 -	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
1.37 +        fix d w
1.38 +        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
1.39 +        hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.40 +        from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
1.41 +        from H have th: "cmod (w-z) \<le> d" by simp
1.42 +        from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
1.43 +        show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
1.44        qed
1.45      qed
1.46  qed
1.47 @@ -397,14 +397,14 @@
1.48      {fix y
1.49        from s[rule_format, of "-y"] have
1.50      "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
1.51 -	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
1.52 +        unfolding minus_less_iff[of y ] equation_minus_iff by blast }
1.53      note s1 = this[unfolded minus_minus]
1.54      from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
1.55        by auto
1.56      {fix n::nat
1.57        from s1[rule_format, of "?m + 1/real (Suc n)"]
1.58        have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
1.59 -	by simp}
1.60 +        by simp}
1.61      hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
1.62      from choice[OF th] obtain g where
1.63        g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
1.64 @@ -416,32 +416,32 @@
1.65        assume wr: "cmod w \<le> r"
1.66        let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
1.67        {assume e: "?e > 0"
1.68 -	hence e2: "?e/2 > 0" by simp
1.69 -	from poly_cont[OF e2, of z p] obtain d where
1.70 -	  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.71 -	{fix w assume w: "cmod (w - z) < d"
1.72 -	  have "cmod(poly p w - poly p z) < ?e / 2"
1.73 -	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
1.74 -	note th1 = this
1.75 +        hence e2: "?e/2 > 0" by simp
1.76 +        from poly_cont[OF e2, of z p] obtain d where
1.77 +          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.78 +        {fix w assume w: "cmod (w - z) < d"
1.79 +          have "cmod(poly p w - poly p z) < ?e / 2"
1.80 +            using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
1.81 +        note th1 = this
1.82
1.83 -	from fz(2)[rule_format, OF d(1)] obtain N1 where
1.84 -	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
1.85 -	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
1.86 -	  N2: "2/?e < real N2" by blast
1.87 -	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
1.88 -	  using N1[rule_format, of "N1 + N2"] th1 by simp
1.89 -	{fix a b e2 m :: real
1.90 -	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
1.91 +        from fz(2)[rule_format, OF d(1)] obtain N1 where
1.92 +          N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
1.93 +        from reals_Archimedean2[of "2/?e"] obtain N2::nat where
1.94 +          N2: "2/?e < real N2" by blast
1.95 +        have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
1.96 +          using N1[rule_format, of "N1 + N2"] th1 by simp
1.97 +        {fix a b e2 m :: real
1.98 +        have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
1.99            ==> False" by arith}
1.100        note th0 = this
1.101        have ath:
1.102 -	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
1.103 +        "\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
1.104        from s1m[OF g(1)[rule_format]]
1.105        have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
1.106        from seq_suble[OF fz(1), of "N1+N2"]
1.107        have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
1.108        have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
1.109 -	using N2 by auto
1.110 +        using N2 by auto
1.111        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.112        from g(2)[rule_format, of "f (N1 + N2)"]
1.113        have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
1.114 @@ -453,10 +453,10 @@
1.115        with ath[OF th31 th32]
1.116        have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
1.117        have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
1.118 -	by arith
1.119 +        by arith
1.120        have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
1.121  \<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
1.122 -	by (simp add: norm_triangle_ineq3)
1.123 +        by (simp add: norm_triangle_ineq3)
1.124        from ath2[OF th22, of ?m]
1.125        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.126        from th0[OF th2 thc1 thc2] have False .}
1.127 @@ -502,10 +502,10 @@
1.128        from h have z1: "cmod z \<ge> 1" by arith
1.129        from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
1.130        have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
1.131 -	unfolding norm_mult by (simp add: algebra_simps)
1.132 +        unfolding norm_mult by (simp add: algebra_simps)
1.133        from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
1.134        have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
1.135 -	by (simp add: diff_le_eq algebra_simps)
1.136 +        by (simp add: diff_le_eq algebra_simps)
1.137        from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
1.138      hence ?case by blast}
1.139    moreover
1.140 @@ -516,11 +516,11 @@
1.141        assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
1.142        from c0 have "cmod c > 0" by simp
1.143        from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
1.144 -	by (simp add: field_simps norm_mult)
1.145 +        by (simp add: field_simps norm_mult)
1.146        have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
1.147        from complex_mod_triangle_sub[of "z*c" a ]
1.148        have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
1.149 -	by (simp add: algebra_simps)
1.150 +        by (simp add: algebra_simps)
1.151        from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
1.152          using cs0' by simp}
1.153      then have ?case  by blast}
1.154 @@ -541,7 +541,7 @@
1.155      {fix z assume z: "r \<le> cmod z"
1.156        from v[of 0] r[OF z]
1.157        have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
1.158 -	by simp }
1.159 +        by simp }
1.160      note v0 = this
1.161      from v0 v ath[of r] have ?case by blast}
1.162    moreover
1.163 @@ -644,11 +644,11 @@
1.164      {assume h: "constant (poly q)"
1.165        from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
1.166        {fix x y
1.167 -	from th have "?p x = poly q (x - c)" by auto
1.168 -	also have "\<dots> = poly q (y - c)"
1.169 -	  using h unfolding constant_def by blast
1.170 -	also have "\<dots> = ?p y" using th by auto
1.171 -	finally have "?p x = ?p y" .}
1.172 +        from th have "?p x = poly q (x - c)" by auto
1.173 +        also have "\<dots> = poly q (y - c)"
1.174 +          using h unfolding constant_def by blast
1.175 +        also have "\<dots> = ?p y" using th by auto
1.176 +        finally have "?p x = ?p y" .}
1.177        with nc have False unfolding constant_def by blast }
1.178      hence qnc: "\<not> constant (poly q)" by blast
1.179      from q(2) have pqc0: "?p c = poly q 0" by simp
1.180 @@ -664,19 +664,19 @@
1.182      {assume h: "\<And>x y. poly ?r x = poly ?r y"
1.183        {fix x y
1.184 -	from qr[rule_format, of x]
1.185 -	have "poly q x = poly ?r x * ?a0" by auto
1.186 -	also have "\<dots> = poly ?r y * ?a0" using h by simp
1.187 -	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
1.188 -	finally have "poly q x = poly q y" .}
1.189 +        from qr[rule_format, of x]
1.190 +        have "poly q x = poly ?r x * ?a0" by auto
1.191 +        also have "\<dots> = poly ?r y * ?a0" using h by simp
1.192 +        also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
1.193 +        finally have "poly q x = poly q y" .}
1.194        with qnc have False unfolding constant_def by blast}
1.195      hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
1.196      from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
1.197      {fix w
1.198        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
1.199 -	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
1.200 +        using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
1.201        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
1.202 -	using a00 unfolding norm_divide by (simp add: field_simps)
1.203 +        using a00 unfolding norm_divide by (simp add: field_simps)
1.204        finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
1.205      note mrmq_eq = this
1.206      from poly_decompose[OF rnc] obtain k a s where
1.207 @@ -685,72 +685,72 @@
1.208      {assume "k + 1 = n"
1.209        with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
1.210        {fix w
1.211 -	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
1.212 -	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
1.213 +        have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
1.214 +          using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
1.215        note hth = this [symmetric]
1.216 -	from reduce_poly_simple[OF kas(1,2)]
1.217 +        from reduce_poly_simple[OF kas(1,2)]
1.218        have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
1.219      moreover
1.220      {assume kn: "k+1 \<noteq> n"
1.221        from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
1.222        have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
1.223 -	unfolding constant_def poly_pCons poly_monom
1.224 -	using kas(1) apply simp
1.225 -	by (rule exI[where x=0], rule exI[where x=1], simp)
1.226 +        unfolding constant_def poly_pCons poly_monom
1.227 +        using kas(1) apply simp
1.228 +        by (rule exI[where x=0], rule exI[where x=1], simp)
1.229        from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
1.230 -	by (simp add: psize_def degree_monom_eq)
1.231 +        by (simp add: psize_def degree_monom_eq)
1.232        from H[rule_format, OF k1n th01 th02]
1.233        obtain w where w: "1 + w^k * a = 0"
1.234 -	unfolding poly_pCons poly_monom
1.235 -	using kas(2) by (cases k, auto simp add: algebra_simps)
1.236 +        unfolding poly_pCons poly_monom
1.237 +        using kas(2) by (cases k, auto simp add: algebra_simps)
1.238        from poly_bound_exists[of "cmod w" s] obtain m where
1.239 -	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
1.240 +        m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
1.241        have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
1.242        from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
1.243        then have wm1: "w^k * a = - 1" by simp
1.244        have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
1.245 -	using norm_ge_zero[of w] w0 m(1)
1.246 -	  by (simp add: inverse_eq_divide zero_less_mult_iff)
1.247 +        using norm_ge_zero[of w] w0 m(1)
1.248 +          by (simp add: inverse_eq_divide zero_less_mult_iff)
1.249        with real_down2[OF zero_less_one] obtain t where
1.250 -	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
1.251 +        t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
1.252        let ?ct = "complex_of_real t"
1.253        let ?w = "?ct * w"
1.254        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.255        also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
1.256 -	unfolding wm1 by (simp)
1.257 +        unfolding wm1 by (simp)
1.258        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.259 -	apply -
1.260 -	apply (rule cong[OF refl[of cmod]])
1.261 -	apply assumption
1.262 -	done
1.263 +        apply -
1.264 +        apply (rule cong[OF refl[of cmod]])
1.265 +        apply assumption
1.266 +        done
1.267        with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
1.268        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.269        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.270        have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
1.271        then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
1.272        from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
1.273 -	by (simp add: inverse_eq_divide field_simps)
1.274 +        by (simp add: inverse_eq_divide field_simps)
1.275        with zero_less_power[OF t(1), of k]
1.276        have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
1.277 -	apply - apply (rule mult_strict_left_mono) by simp_all
1.278 +        apply - apply (rule mult_strict_left_mono) by simp_all
1.279        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
1.280 -	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
1.281 +        by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
1.282        then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
1.283 -	using t(1,2) m(2)[rule_format, OF tw] w0
1.284 -	apply (simp only: )
1.285 -	apply auto
1.286 -	apply (rule mult_mono, simp_all add: norm_ge_zero)+
1.287 -	apply (simp add: zero_le_mult_iff zero_le_power)
1.288 -	done
1.289 +        using t(1,2) m(2)[rule_format, OF tw] w0
1.290 +        apply (simp only: )
1.291 +        apply auto
1.292 +        apply (rule mult_mono, simp_all add: norm_ge_zero)+
1.293 +        apply (simp add: zero_le_mult_iff zero_le_power)
1.294 +        done
1.295        with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
1.296        from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
1.297 -	by auto
1.298 +        by auto
1.299        from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
1.300        have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
1.301        from th11 th12
1.302        have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
1.303        then have "cmod (poly ?r ?w) < 1"
1.304 -	unfolding kas(4)[rule_format, of ?w] r01 by simp
1.305 +        unfolding kas(4)[rule_format, of ?w] r01 by simp
1.306        then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
1.307      ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
1.308      from cr0_contr cq0 q(2)
1.309 @@ -773,30 +773,30 @@
1.310        from nc[unfolded constant_def, rule_format, of 0]
1.311        have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
1.312        hence "cs = 0"
1.313 -	proof(induct cs)
1.314 -	  case (pCons d ds)
1.315 -	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
1.316 -	  moreover
1.317 -	  {assume d0: "d\<noteq>0"
1.318 -	    from poly_bound_exists[of 1 ds] obtain m where
1.319 -	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
1.320 -	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
1.321 -	    from real_down2[OF dm zero_less_one] obtain x where
1.322 -	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
1.323 -	    let ?x = "complex_of_real x"
1.324 -	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
1.325 -	    from pCons.prems[rule_format, OF cx(1)]
1.326 -	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
1.327 -	    from m(2)[rule_format, OF cx(2)] x(1)
1.328 -	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
1.329 -	      by (simp add: norm_mult)
1.330 -	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
1.331 -	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
1.332 -	    with cth  have ?case by blast}
1.333 -	  ultimately show ?case by blast
1.334 -	qed simp}
1.335 +        proof(induct cs)
1.336 +          case (pCons d ds)
1.337 +          {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
1.338 +          moreover
1.339 +          {assume d0: "d\<noteq>0"
1.340 +            from poly_bound_exists[of 1 ds] obtain m where
1.341 +              m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
1.342 +            have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
1.343 +            from real_down2[OF dm zero_less_one] obtain x where
1.344 +              x: "x > 0" "x < cmod d / m" "x < 1" by blast
1.345 +            let ?x = "complex_of_real x"
1.346 +            from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
1.347 +            from pCons.prems[rule_format, OF cx(1)]
1.348 +            have cth: "cmod (?x*poly ds ?x) = cmod d" 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  have ?case by blast}
1.355 +          ultimately show ?case by blast
1.356 +        qed simp}
1.357        then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0
1.358 -	by blast
1.359 +        by blast
1.360        from fundamental_theorem_of_algebra[OF nc] have ?case .}
1.361    ultimately show ?case by blast
1.362  qed simp
1.363 @@ -823,59 +823,59 @@
1.364      {assume oa: "order a p \<noteq> 0"
1.365        let ?op = "order a p"
1.366        from pne have ap: "([:- a, 1:] ^ ?op) dvd p"
1.367 -	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
1.368 +        "\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
1.369        note oop = order_degree[OF pne, unfolded dpn]
1.370        {assume q0: "q = 0"
1.371 -	hence ?ths using n0
1.372 +        hence ?ths using n0
1.374        moreover
1.375        {assume q0: "q \<noteq> 0"
1.376 -	from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
1.377 -	obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
1.378 -	from ap(1) obtain s where
1.379 -	  s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
1.380 -	have sne: "s \<noteq> 0"
1.381 -	  using s pne by auto
1.382 -	{assume ds0: "degree s = 0"
1.383 -	  from ds0 have "\<exists>k. s = [:k:]"
1.384 +        from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
1.385 +        obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
1.386 +        from ap(1) obtain s where
1.387 +          s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
1.388 +        have sne: "s \<noteq> 0"
1.389 +          using s pne by auto
1.390 +        {assume ds0: "degree s = 0"
1.391 +          from ds0 have "\<exists>k. s = [:k:]"
1.392              by (cases s, simp split: if_splits)
1.393 -	  then obtain k where kpn: "s = [:k:]" by blast
1.394 +          then obtain k where kpn: "s = [:k:]" by blast
1.395            from sne kpn have k: "k \<noteq> 0" by simp
1.396 -	  let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
1.397 +          let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
1.398            from k oop [of a] have "q ^ n = p * ?w"
1.399              apply -
1.400              apply (subst r, subst s, subst kpn)
1.401              apply (subst power_mult_distrib, simp)
1.402              apply (subst power_add [symmetric], simp)
1.403              done
1.404 -	  hence ?ths unfolding dvd_def by blast}
1.405 -	moreover
1.406 -	{assume ds0: "degree s \<noteq> 0"
1.407 -	  from ds0 sne dpn s oa
1.408 -	    have dsn: "degree s < n" apply auto
1.409 +          hence ?ths unfolding dvd_def by blast}
1.410 +        moreover
1.411 +        {assume ds0: "degree s \<noteq> 0"
1.412 +          from ds0 sne dpn s oa
1.413 +            have dsn: "degree s < n" apply auto
1.414                apply (erule ssubst)
1.415                apply (simp add: degree_mult_eq degree_linear_power)
1.416                done
1.417 -	    {fix x assume h: "poly s x = 0"
1.418 -	      {assume xa: "x = a"
1.419 -		from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
1.420 -		  u: "s = [:- a, 1:] * u" by (rule dvdE)
1.421 -		have "p = [:- a, 1:] ^ (Suc ?op) * u"
1.422 +            {fix x assume h: "poly s x = 0"
1.423 +              {assume xa: "x = a"
1.424 +                from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
1.425 +                  u: "s = [:- a, 1:] * u" by (rule dvdE)
1.426 +                have "p = [:- a, 1:] ^ (Suc ?op) * u"
1.427                    by (subst s, subst u, simp only: power_Suc mult_ac)
1.428 -		with ap(2)[unfolded dvd_def] have False by blast}
1.429 -	      note xa = this
1.430 -	      from h have "poly p x = 0" by (subst s, simp)
1.431 -	      with pq0 have "poly q x = 0" by blast
1.432 -	      with r xa have "poly r x = 0"
1.433 +                with ap(2)[unfolded dvd_def] have False by blast}
1.434 +              note xa = this
1.435 +              from h have "poly p x = 0" by (subst s, simp)
1.436 +              with pq0 have "poly q x = 0" by blast
1.437 +              with r xa have "poly r x = 0"
1.439 -	    note impth = this
1.440 -	    from IH[rule_format, OF dsn, of s r] impth ds0
1.441 -	    have "s dvd (r ^ (degree s))" by blast
1.442 -	    then obtain u where u: "r ^ (degree s) = s * u" ..
1.443 -	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
1.444 +            note impth = this
1.445 +            from IH[rule_format, OF dsn, of s r] impth ds0
1.446 +            have "s dvd (r ^ (degree s))" by blast
1.447 +            then obtain u where u: "r ^ (degree s) = s * u" ..
1.448 +            hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
1.449                by (simp only: poly_mult[symmetric] poly_power[symmetric])
1.450 -	    let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
1.451 -	    from oop[of a] dsn have "q ^ n = p * ?w"
1.452 +            let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
1.453 +            from oop[of a] dsn have "q ^ n = p * ?w"
1.454                apply -
1.455                apply (subst s, subst r)
1.456                apply (simp only: power_mult_distrib)
1.457 @@ -885,7 +885,7 @@
1.458                apply (subst u [symmetric])
1.460                done
1.461 -	    hence ?ths unfolding dvd_def by blast}
1.462 +            hence ?ths unfolding dvd_def by blast}
1.463        ultimately have ?ths by blast }
1.464        ultimately have ?ths by blast}
1.465      then have ?ths using a order_root pne by blast}
1.466 @@ -930,12 +930,12 @@
1.467      {assume dp: "degree p \<noteq> 0"
1.468        then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
1.469        {assume "p dvd (q ^ (Suc n))"
1.470 -	then obtain u where u: "q ^ (Suc n) = p * u" ..
1.471 -	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.472 -	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
1.473 -	  hence False using u h(1) by (simp only: poly_mult) simp}}
1.474 -	with n nullstellensatz_lemma[of p q "degree p"] dp
1.475 -	have ?thesis by auto}
1.476 +        then obtain u where u: "q ^ (Suc n) = p * u" ..
1.477 +        {fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
1.478 +          hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
1.479 +          hence False using u h(1) by (simp only: poly_mult) simp}}
1.480 +        with n nullstellensatz_lemma[of p q "degree p"] dp
1.481 +        have ?thesis by auto}
1.482      ultimately have ?thesis by blast}
1.483    ultimately show ?thesis by blast
1.484  qed
```