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.181        by (simp add: expand_poly_eq)
   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.373            by (simp add: power_0_left)}
   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.438                  by (auto simp add: uminus_add_conv_diff)}
   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.459                apply (simp add: mult_ac power_add [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