src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 30488 5c4c3a9e9102
parent 30242 aea5d7fa7ef5
child 31021 53642251a04f
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Mar 12 15:31:44 2009 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Mar 12 08:57:03 2009 -0700
     1.3 @@ -18,12 +18,12 @@
     1.4  proof-
     1.5    obtain x y where xy: "z = Complex x y" by (cases z)
     1.6    {assume y0: "y = 0"
     1.7 -    {assume x0: "x \<ge> 0" 
     1.8 +    {assume x0: "x \<ge> 0"
     1.9        then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
    1.10  	by (simp add: csqrt_def power2_eq_square)}
    1.11      moreover
    1.12      {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
    1.13 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0] 
    1.14 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
    1.15  	by (simp add: csqrt_def power2_eq_square) }
    1.16      ultimately have ?thesis by blast}
    1.17    moreover
    1.18 @@ -31,20 +31,20 @@
    1.19      {fix x y
    1.20        let ?z = "Complex x y"
    1.21        from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
    1.22 -      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ 
    1.23 +      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+
    1.24        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.25      note th = this
    1.26 -    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" 
    1.27 -      by (simp add: power2_eq_square) 
    1.28 +    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2"
    1.29 +      by (simp add: power2_eq_square)
    1.30      from th[of x y]
    1.31      have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
    1.32      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.33 -      unfolding power2_eq_square by simp 
    1.34 -    have "sqrt 4 = sqrt (2^2)" by simp 
    1.35 +      unfolding power2_eq_square by simp
    1.36 +    have "sqrt 4 = sqrt (2^2)" by simp
    1.37      hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
    1.38      have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
    1.39        using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
    1.40 -      unfolding power2_eq_square 
    1.41 +      unfolding power2_eq_square
    1.42        by (simp add: algebra_simps real_sqrt_divide sqrt4)
    1.43       from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
    1.44         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.45 @@ -71,7 +71,7 @@
    1.46  lemma poly_bound_exists:
    1.47    shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
    1.48  proof(induct p)
    1.49 -  case 0 thus ?case by (rule exI[where x=1], simp) 
    1.50 +  case 0 thus ?case by (rule exI[where x=1], simp)
    1.51  next
    1.52    case (pCons c cs)
    1.53    from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
    1.54 @@ -156,14 +156,14 @@
    1.55  proof-
    1.56    from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
    1.57    from ex have thx:"\<exists>x. x \<in> Collect P" by blast
    1.58 -  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y" 
    1.59 +  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
    1.60      by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
    1.61    from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
    1.62      by blast
    1.63    from Y[OF x] have xY: "x < Y" .
    1.64 -  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)  
    1.65 -  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y" 
    1.66 -    apply (clarsimp, atomize (full)) by auto 
    1.67 +  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.68 +  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
    1.69 +    apply (clarsimp, atomize (full)) by auto
    1.70    from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.71    {fix y
    1.72      {fix z assume z: "P z" "y < z"
    1.73 @@ -171,7 +171,7 @@
    1.74      moreover
    1.75      {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
    1.76        hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
    1.77 -      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def) 
    1.78 +      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    1.79        with yL(1) have False  by arith}
    1.80      ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
    1.81    thus ?thesis by blast
    1.82 @@ -190,7 +190,7 @@
    1.83      hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
    1.84      hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
    1.85        by - (rule power_mono, simp, simp)+
    1.86 -    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1" 
    1.87 +    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
    1.88        by (simp_all  add: power2_abs power_mult_distrib)
    1.89      from add_mono[OF th0] xy have False by simp }
    1.90    thus ?thesis unfolding linorder_not_le[symmetric] by blast
    1.91 @@ -216,21 +216,21 @@
    1.92    {assume o: "odd n"
    1.93      from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
    1.94      have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
    1.95 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = 
    1.96 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
    1.97      ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
    1.98 -    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2" 
    1.99 +    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
   1.100        apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
   1.101        by (simp add: power2_eq_square)
   1.102 -    finally 
   1.103 +    finally
   1.104      have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
   1.105      Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
   1.106 -    1" 
   1.107 +    1"
   1.108        apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
   1.109        using right_inverse[OF b']
   1.110        by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
   1.111      have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   1.112        apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
   1.113 -      by (simp add: real_sqrt_mult[symmetric] th0)        
   1.114 +      by (simp add: real_sqrt_mult[symmetric] th0)
   1.115      from o have "\<exists>m. n = Suc (2*m)" by presburger+
   1.116      then obtain m where m: "n = Suc (2*m)" by blast
   1.117      from unimodular_reduce_norm[OF th0] o
   1.118 @@ -246,7 +246,7 @@
   1.119      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   1.120      let ?w = "v / complex_of_real (root n (cmod b))"
   1.121      from odd_real_root_pow[OF o, of "cmod b"]
   1.122 -    have th1: "?w ^ n = v^n / complex_of_real (cmod b)" 
   1.123 +    have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
   1.124        by (simp add: power_divide complex_of_real_power)
   1.125      have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
   1.126      hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
   1.127 @@ -257,7 +257,7 @@
   1.128        using b v by (simp add: th2)
   1.129  
   1.130      from mult_less_imp_less_left[OF th4 th3]
   1.131 -    have "?P ?w n" unfolding th1 . 
   1.132 +    have "?P ?w n" unfolding th1 .
   1.133      hence "\<exists>z. ?P z n" .. }
   1.134    ultimately show "\<exists>z. ?P z n" by blast
   1.135  qed
   1.136 @@ -272,14 +272,14 @@
   1.137    assumes r: "\<forall>n. cmod (s n) \<le> r"
   1.138    shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   1.139  proof-
   1.140 -  from seq_monosub[of "Re o s"] 
   1.141 -  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))" 
   1.142 +  from seq_monosub[of "Re o s"]
   1.143 +  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
   1.144      unfolding o_def by blast
   1.145 -  from seq_monosub[of "Im o s o f"] 
   1.146 -  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast  
   1.147 +  from seq_monosub[of "Im o s o f"]
   1.148 +  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast
   1.149    let ?h = "f o g"
   1.150 -  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith 
   1.151 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>" 
   1.152 +  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith
   1.153 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>"
   1.154    proof
   1.155      fix n
   1.156      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.157 @@ -290,7 +290,7 @@
   1.158      apply (rule exI[where x= "r + 1"])
   1.159      using th rp apply simp
   1.160      using f(2) .
   1.161 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>" 
   1.162 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>"
   1.163    proof
   1.164      fix n
   1.165      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.166 @@ -303,17 +303,17 @@
   1.167      using th rp apply simp
   1.168      using g(2) .
   1.169  
   1.170 -  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x" 
   1.171 -    by blast 
   1.172 -  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r" 
   1.173 +  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
   1.174 +    by blast
   1.175 +  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
   1.176      unfolding LIMSEQ_def real_norm_def .
   1.177  
   1.178 -  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y" 
   1.179 -    by blast 
   1.180 -  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r" 
   1.181 +  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
   1.182 +    by blast
   1.183 +  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
   1.184      unfolding LIMSEQ_def real_norm_def .
   1.185    let ?w = "Complex x y"
   1.186 -  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto 
   1.187 +  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
   1.188    {fix e assume ep: "e > (0::real)"
   1.189      hence e2: "e/2 > 0" by simp
   1.190      from x[rule_format, OF e2] y[rule_format, OF e2]
   1.191 @@ -321,16 +321,16 @@
   1.192      {fix n assume nN12: "n \<ge> N1 + N2"
   1.193        hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
   1.194        from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
   1.195 -      have "cmod (s (?h n) - ?w) < e" 
   1.196 +      have "cmod (s (?h n) - ?w) < e"
   1.197  	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
   1.198      hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
   1.199 -  with hs show ?thesis  by blast  
   1.200 +  with hs show ?thesis  by blast
   1.201  qed
   1.202  
   1.203  text{* Polynomial is continuous. *}
   1.204  
   1.205  lemma poly_cont:
   1.206 -  assumes ep: "e > 0" 
   1.207 +  assumes ep: "e > 0"
   1.208    shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
   1.209  proof-
   1.210    obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
   1.211 @@ -348,35 +348,35 @@
   1.212      case 0 thus ?case  using ep by auto
   1.213    next
   1.214      case (pCons c cs)
   1.215 -    from poly_bound_exists[of 1 "cs"] 
   1.216 +    from poly_bound_exists[of 1 "cs"]
   1.217      obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
   1.218      from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
   1.219      have one0: "1 > (0::real)"  by arith
   1.220 -    from real_lbound_gt_zero[OF one0 em0] 
   1.221 +    from real_lbound_gt_zero[OF one0 em0]
   1.222      obtain d where d: "d >0" "d < 1" "d < e / m" by blast
   1.223 -    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e" 
   1.224 +    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
   1.225        by (simp_all add: field_simps real_mult_order)
   1.226 -    show ?case 
   1.227 +    show ?case
   1.228        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   1.229  	fix d w
   1.230  	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
   1.231  	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
   1.232  	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
   1.233 -	from H have th: "cmod (w-z) \<le> d" by simp 
   1.234 +	from H have th: "cmod (w-z) \<le> d" by simp
   1.235  	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
   1.236  	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
   1.237 -      qed  
   1.238 +      qed
   1.239      qed
   1.240  qed
   1.241  
   1.242 -text{* Hence a polynomial attains minimum on a closed disc 
   1.243 +text{* Hence a polynomial attains minimum on a closed disc
   1.244    in the complex plane. *}
   1.245  lemma  poly_minimum_modulus_disc:
   1.246    "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
   1.247  proof-
   1.248    {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
   1.249        apply -
   1.250 -      apply (rule exI[where x=0]) 
   1.251 +      apply (rule exI[where x=0])
   1.252        apply auto
   1.253        apply (subgoal_tac "cmod w < 0")
   1.254        apply simp
   1.255 @@ -384,35 +384,35 @@
   1.256        done }
   1.257    moreover
   1.258    {assume rp: "r \<ge> 0"
   1.259 -    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp 
   1.260 +    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp
   1.261      hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
   1.262      {fix x z
   1.263        assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
   1.264        hence "- x < 0 " by arith
   1.265        with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
   1.266      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.267 -    from real_sup_exists[OF mth1 mth2] obtain s where 
   1.268 +    from real_sup_exists[OF mth1 mth2] obtain s where
   1.269        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.270      let ?m = "-s"
   1.271      {fix y
   1.272 -      from s[rule_format, of "-y"] have 
   1.273 -    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" 
   1.274 +      from s[rule_format, of "-y"] have
   1.275 +    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y"
   1.276  	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
   1.277      note s1 = this[unfolded minus_minus]
   1.278 -    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m" 
   1.279 +    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m"
   1.280        by auto
   1.281      {fix n::nat
   1.282 -      from s1[rule_format, of "?m + 1/real (Suc n)"] 
   1.283 +      from s1[rule_format, of "?m + 1/real (Suc n)"]
   1.284        have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
   1.285  	by simp}
   1.286      hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
   1.287 -    from choice[OF th] obtain g where 
   1.288 -      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)" 
   1.289 +    from choice[OF th] obtain g where
   1.290 +      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)"
   1.291        by blast
   1.292 -    from bolzano_weierstrass_complex_disc[OF g(1)] 
   1.293 +    from bolzano_weierstrass_complex_disc[OF g(1)]
   1.294      obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   1.295 -      by blast    
   1.296 -    {fix w 
   1.297 +      by blast
   1.298 +    {fix w
   1.299        assume wr: "cmod w \<le> r"
   1.300        let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
   1.301        {assume e: "?e > 0"
   1.302 @@ -423,8 +423,8 @@
   1.303  	  have "cmod(poly p w - poly p z) < ?e / 2"
   1.304  	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
   1.305  	note th1 = this
   1.306 -	
   1.307 -	from fz(2)[rule_format, OF d(1)] obtain N1 where 
   1.308 +
   1.309 +	from fz(2)[rule_format, OF d(1)] obtain N1 where
   1.310  	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
   1.311  	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
   1.312  	  N2: "2/?e < real N2" by blast
   1.313 @@ -434,13 +434,13 @@
   1.314  	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
   1.315            ==> False" by arith}
   1.316        note th0 = this
   1.317 -      have ath: 
   1.318 +      have ath:
   1.319  	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
   1.320        from s1m[OF g(1)[rule_format]]
   1.321        have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   1.322        from seq_suble[OF fz(1), of "N1+N2"]
   1.323        have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
   1.324 -      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"  
   1.325 +      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"
   1.326  	using N2 by auto
   1.327        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.328        from g(2)[rule_format, of "f (N1 + N2)"]
   1.329 @@ -451,17 +451,17 @@
   1.330        with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   1.331        have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
   1.332        with ath[OF th31 th32]
   1.333 -      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith  
   1.334 -      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c" 
   1.335 +      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith
   1.336 +      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c"
   1.337  	by arith
   1.338        have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
   1.339 -\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)" 
   1.340 +\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)"
   1.341  	by (simp add: norm_triangle_ineq3)
   1.342        from ath2[OF th22, of ?m]
   1.343        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.344        from th0[OF th2 thc1 thc2] have False .}
   1.345        hence "?e = 0" by auto
   1.346 -      then have "cmod (poly p z) = ?m" by simp  
   1.347 +      then have "cmod (poly p z) = ?m" by simp
   1.348        with s1m[OF wr]
   1.349        have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
   1.350      hence ?thesis by blast}
   1.351 @@ -474,7 +474,7 @@
   1.352    apply (simp add: power2_eq_square[symmetric])
   1.353    done
   1.354  
   1.355 -lemma cispi: "cis pi = -1" 
   1.356 +lemma cispi: "cis pi = -1"
   1.357    unfolding cis_def
   1.358    by simp
   1.359  
   1.360 @@ -491,7 +491,7 @@
   1.361    shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
   1.362  using ex
   1.363  proof(induct p arbitrary: a d)
   1.364 -  case (pCons c cs a d) 
   1.365 +  case (pCons c cs a d)
   1.366    {assume H: "cs \<noteq> 0"
   1.367      with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
   1.368      let ?r = "1 + \<bar>r\<bar>"
   1.369 @@ -504,8 +504,8 @@
   1.370        have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
   1.371  	unfolding norm_mult by (simp add: algebra_simps)
   1.372        from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
   1.373 -      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   1.374 -	by (simp add: diff_le_eq algebra_simps) 
   1.375 +      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
   1.376 +	by (simp add: diff_le_eq algebra_simps)
   1.377        from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
   1.378      hence ?case by blast}
   1.379    moreover
   1.380 @@ -515,13 +515,13 @@
   1.381      {fix z
   1.382        assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
   1.383        from c0 have "cmod c > 0" by simp
   1.384 -      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)" 
   1.385 +      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
   1.386  	by (simp add: field_simps norm_mult)
   1.387        have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
   1.388        from complex_mod_triangle_sub[of "z*c" a ]
   1.389        have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
   1.390  	by (simp add: algebra_simps)
   1.391 -      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   1.392 +      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
   1.393          using cs0' by simp}
   1.394      then have ?case  by blast}
   1.395    ultimately show ?case by blast
   1.396 @@ -531,15 +531,15 @@
   1.397  lemma poly_minimum_modulus:
   1.398    "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   1.399  proof(induct p)
   1.400 -  case (pCons c cs) 
   1.401 +  case (pCons c cs)
   1.402    {assume cs0: "cs \<noteq> 0"
   1.403      from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
   1.404      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.405      have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
   1.406 -    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"] 
   1.407 +    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"]
   1.408      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.409      {fix z assume z: "r \<le> cmod z"
   1.410 -      from v[of 0] r[OF z] 
   1.411 +      from v[of 0] r[OF z]
   1.412        have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
   1.413  	by simp }
   1.414      note v0 = this
   1.415 @@ -558,17 +558,17 @@
   1.416    unfolding constant_def psize_def
   1.417    apply (induct p, auto)
   1.418    done
   1.419 - 
   1.420 +
   1.421  lemma poly_replicate_append:
   1.422    "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
   1.423    by (simp add: poly_monom)
   1.424  
   1.425 -text {* Decomposition of polynomial, skipping zero coefficients 
   1.426 +text {* Decomposition of polynomial, skipping zero coefficients
   1.427    after the first.  *}
   1.428  
   1.429  lemma poly_decompose_lemma:
   1.430   assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
   1.431 -  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and> 
   1.432 +  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and>
   1.433                   (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   1.434  unfolding psize_def
   1.435  using nz
   1.436 @@ -596,9 +596,9 @@
   1.437  lemma poly_decompose:
   1.438    assumes nc: "~constant(poly p)"
   1.439    shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
   1.440 -               psize q + k + 1 = psize p \<and> 
   1.441 +               psize q + k + 1 = psize p \<and>
   1.442                (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   1.443 -using nc 
   1.444 +using nc
   1.445  proof(induct p)
   1.446    case 0 thus ?case by (simp add: constant_def)
   1.447  next
   1.448 @@ -608,8 +608,8 @@
   1.449        from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)}
   1.450      with pCons.prems have False by (auto simp add: constant_def)}
   1.451    hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
   1.452 -  from poly_decompose_lemma[OF th] 
   1.453 -  show ?case 
   1.454 +  from poly_decompose_lemma[OF th]
   1.455 +  show ?case
   1.456      apply clarsimp
   1.457      apply (rule_tac x="k+1" in exI)
   1.458      apply (rule_tac x="a" in exI)
   1.459 @@ -633,7 +633,7 @@
   1.460    let ?ths = "\<exists>z. ?p z = 0"
   1.461  
   1.462    from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
   1.463 -  from poly_minimum_modulus obtain c where 
   1.464 +  from poly_minimum_modulus obtain c where
   1.465      c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
   1.466    {assume pc: "?p c = 0" hence ?ths by blast}
   1.467    moreover
   1.468 @@ -643,18 +643,18 @@
   1.469      {assume h: "constant (poly q)"
   1.470        from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
   1.471        {fix x y
   1.472 -	from th have "?p x = poly q (x - c)" by auto 
   1.473 -	also have "\<dots> = poly q (y - c)" 
   1.474 +	from th have "?p x = poly q (x - c)" by auto
   1.475 +	also have "\<dots> = poly q (y - c)"
   1.476  	  using h unfolding constant_def by blast
   1.477  	also have "\<dots> = ?p y" using th by auto
   1.478  	finally have "?p x = ?p y" .}
   1.479        with nc have False unfolding constant_def by blast }
   1.480      hence qnc: "\<not> constant (poly q)" by blast
   1.481      from q(2) have pqc0: "?p c = poly q 0" by simp
   1.482 -    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp 
   1.483 +    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp
   1.484      let ?a0 = "poly q 0"
   1.485 -    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp 
   1.486 -    from a00 
   1.487 +    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp
   1.488 +    from a00
   1.489      have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   1.490        by simp
   1.491      let ?r = "smult (inverse ?a0) q"
   1.492 @@ -663,38 +663,38 @@
   1.493        by (simp add: expand_poly_eq)
   1.494      {assume h: "\<And>x y. poly ?r x = poly ?r y"
   1.495        {fix x y
   1.496 -	from qr[rule_format, of x] 
   1.497 +	from qr[rule_format, of x]
   1.498  	have "poly q x = poly ?r x * ?a0" by auto
   1.499  	also have "\<dots> = poly ?r y * ?a0" using h by simp
   1.500  	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
   1.501 -	finally have "poly q x = poly q y" .} 
   1.502 +	finally have "poly q x = poly q y" .}
   1.503        with qnc have False unfolding constant_def by blast}
   1.504      hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
   1.505      from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
   1.506 -    {fix w 
   1.507 +    {fix w
   1.508        have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   1.509  	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
   1.510        also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   1.511  	using a00 unfolding norm_divide by (simp add: field_simps)
   1.512        finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
   1.513      note mrmq_eq = this
   1.514 -    from poly_decompose[OF rnc] obtain k a s where 
   1.515 -      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r" 
   1.516 +    from poly_decompose[OF rnc] obtain k a s where
   1.517 +      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r"
   1.518        "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   1.519      {assume "k + 1 = n"
   1.520        with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
   1.521        {fix w
   1.522 -	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" 
   1.523 +	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)"
   1.524  	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
   1.525        note hth = this [symmetric]
   1.526 -	from reduce_poly_simple[OF kas(1,2)] 
   1.527 +	from reduce_poly_simple[OF kas(1,2)]
   1.528        have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
   1.529      moreover
   1.530      {assume kn: "k+1 \<noteq> n"
   1.531        from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
   1.532 -      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))" 
   1.533 +      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))"
   1.534  	unfolding constant_def poly_pCons poly_monom
   1.535 -	using kas(1) apply simp 
   1.536 +	using kas(1) apply simp
   1.537  	by (rule exI[where x=0], rule exI[where x=1], simp)
   1.538        from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
   1.539  	by (simp add: psize_def degree_monom_eq)
   1.540 @@ -702,12 +702,12 @@
   1.541        obtain w where w: "1 + w^k * a = 0"
   1.542  	unfolding poly_pCons poly_monom
   1.543  	using kas(2) by (cases k, auto simp add: algebra_simps)
   1.544 -      from poly_bound_exists[of "cmod w" s] obtain m where 
   1.545 +      from poly_bound_exists[of "cmod w" s] obtain m where
   1.546  	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   1.547        have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
   1.548        from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
   1.549        then have wm1: "w^k * a = - 1" by simp
   1.550 -      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)" 
   1.551 +      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
   1.552  	using norm_ge_zero[of w] w0 m(1)
   1.553  	  by (simp add: inverse_eq_divide zero_less_mult_iff)
   1.554        with real_down2[OF zero_less_one] obtain t where
   1.555 @@ -717,20 +717,20 @@
   1.556        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.557        also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
   1.558  	unfolding wm1 by (simp)
   1.559 -      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.560 +      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.561  	apply -
   1.562  	apply (rule cong[OF refl[of cmod]])
   1.563  	apply assumption
   1.564  	done
   1.565 -      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"] 
   1.566 -      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.567 +      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
   1.568 +      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.569        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.570        have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
   1.571 -      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult) 
   1.572 +      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
   1.573        from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
   1.574  	by (simp add: inverse_eq_divide field_simps)
   1.575 -      with zero_less_power[OF t(1), of k] 
   1.576 -      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" 
   1.577 +      with zero_less_power[OF t(1), of k]
   1.578 +      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
   1.579  	apply - apply (rule mult_strict_left_mono) by simp_all
   1.580        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
   1.581  	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
   1.582 @@ -741,15 +741,15 @@
   1.583  	apply (rule mult_mono, simp_all add: norm_ge_zero)+
   1.584  	apply (simp add: zero_le_mult_iff zero_le_power)
   1.585  	done
   1.586 -      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp 
   1.587 -      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1" 
   1.588 +      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp
   1.589 +      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1"
   1.590  	by auto
   1.591        from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
   1.592 -      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" . 
   1.593 +      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" .
   1.594        from th11 th12
   1.595 -      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith 
   1.596 -      then have "cmod (poly ?r ?w) < 1" 
   1.597 -	unfolding kas(4)[rule_format, of ?w] r01 by simp 
   1.598 +      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith
   1.599 +      then have "cmod (poly ?r ?w) < 1"
   1.600 +	unfolding kas(4)[rule_format, of ?w] r01 by simp
   1.601        then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
   1.602      ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
   1.603      from cr0_contr cq0 q(2)
   1.604 @@ -769,18 +769,18 @@
   1.605    moreover
   1.606    {assume c0: "c\<noteq>0"
   1.607      {assume nc: "constant (poly (pCons c cs))"
   1.608 -      from nc[unfolded constant_def, rule_format, of 0] 
   1.609 -      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto 
   1.610 +      from nc[unfolded constant_def, rule_format, of 0]
   1.611 +      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto
   1.612        hence "cs = 0"
   1.613  	proof(induct cs)
   1.614  	  case (pCons d ds)
   1.615  	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
   1.616  	  moreover
   1.617  	  {assume d0: "d\<noteq>0"
   1.618 -	    from poly_bound_exists[of 1 ds] obtain m where 
   1.619 +	    from poly_bound_exists[of 1 ds] obtain m where
   1.620  	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   1.621  	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
   1.622 -	    from real_down2[OF dm zero_less_one] obtain x where 
   1.623 +	    from real_down2[OF dm zero_less_one] obtain x where
   1.624  	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
   1.625  	    let ?x = "complex_of_real x"
   1.626  	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
   1.627 @@ -792,12 +792,12 @@
   1.628  	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
   1.629  	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
   1.630  	    with cth  have ?case by blast}
   1.631 -	  ultimately show ?case by blast 
   1.632 +	  ultimately show ?case by blast
   1.633  	qed simp}
   1.634 -      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0 
   1.635 +      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0
   1.636  	by blast
   1.637        from fundamental_theorem_of_algebra[OF nc] have ?case .}
   1.638 -  ultimately show ?case by blast  
   1.639 +  ultimately show ?case by blast
   1.640  qed simp
   1.641  
   1.642  
   1.643 @@ -814,15 +814,15 @@
   1.644    assume IH: "\<forall>m<n. \<forall>p q.
   1.645                   (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
   1.646                   degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
   1.647 -    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0" 
   1.648 +    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   1.649      and dpn: "degree p = n" and n0: "n \<noteq> 0"
   1.650    from dpn n0 have pne: "p \<noteq> 0" by auto
   1.651    let ?ths = "p dvd (q ^ n)"
   1.652    {fix a assume a: "poly p a = 0"
   1.653      {assume oa: "order a p \<noteq> 0"
   1.654        let ?op = "order a p"
   1.655 -      from pne have ap: "([:- a, 1:] ^ ?op) dvd p" 
   1.656 -	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+ 
   1.657 +      from pne have ap: "([:- a, 1:] ^ ?op) dvd p"
   1.658 +	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+
   1.659        note oop = order_degree[OF pne, unfolded dpn]
   1.660        {assume q0: "q = 0"
   1.661  	hence ?ths using n0
   1.662 @@ -892,7 +892,7 @@
   1.663    {assume exa: "\<not> (\<exists>a. poly p a = 0)"
   1.664      from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
   1.665        ccs: "c\<noteq>0" "p = pCons c 0" by blast
   1.666 -    
   1.667 +
   1.668      then have pp: "\<And>x. poly p x =  c" by simp
   1.669      let ?w = "[:1/c:] * (q ^ n)"
   1.670      from ccs
   1.671 @@ -903,7 +903,7 @@
   1.672  qed
   1.673  
   1.674  lemma nullstellensatz_univariate:
   1.675 -  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> 
   1.676 +  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
   1.677      p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
   1.678  proof-
   1.679    {assume pe: "p = 0"
   1.680 @@ -933,7 +933,7 @@
   1.681  	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
   1.682  	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
   1.683  	  hence False using u h(1) by (simp only: poly_mult) simp}}
   1.684 -	with n nullstellensatz_lemma[of p q "degree p"] dp 
   1.685 +	with n nullstellensatz_lemma[of p q "degree p"] dp
   1.686  	have ?thesis by auto}
   1.687      ultimately have ?thesis by blast}
   1.688    ultimately show ?thesis by blast
   1.689 @@ -966,13 +966,13 @@
   1.690  
   1.691  (* Arithmetic operations on multivariate polynomials.                        *)
   1.692  
   1.693 -lemma mpoly_base_conv: 
   1.694 +lemma mpoly_base_conv:
   1.695    "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
   1.696  
   1.697 -lemma mpoly_norm_conv: 
   1.698 +lemma mpoly_norm_conv:
   1.699    "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
   1.700  
   1.701 -lemma mpoly_sub_conv: 
   1.702 +lemma mpoly_sub_conv:
   1.703    "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
   1.704    by (simp add: diff_def)
   1.705  
   1.706 @@ -982,9 +982,9 @@
   1.707  
   1.708  lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
   1.709  lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
   1.710 -  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast 
   1.711 +  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast
   1.712  
   1.713 -lemma poly_divides_pad_rule: 
   1.714 +lemma poly_divides_pad_rule:
   1.715    fixes p q :: "complex poly"
   1.716    assumes pq: "p dvd q"
   1.717    shows "p dvd (pCons (0::complex) q)"
   1.718 @@ -994,7 +994,7 @@
   1.719    with pq show ?thesis by (rule dvd_trans)
   1.720  qed
   1.721  
   1.722 -lemma poly_divides_pad_const_rule: 
   1.723 +lemma poly_divides_pad_const_rule:
   1.724    fixes p q :: "complex poly"
   1.725    assumes pq: "p dvd q"
   1.726    shows "p dvd (smult a q)"
   1.727 @@ -1005,12 +1005,12 @@
   1.728  qed
   1.729  
   1.730  
   1.731 -lemma poly_divides_conv0:  
   1.732 +lemma poly_divides_conv0:
   1.733    fixes p :: "complex poly"
   1.734    assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
   1.735    shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
   1.736  proof-
   1.737 -  {assume r: ?rhs 
   1.738 +  {assume r: ?rhs
   1.739      hence "q = p * 0" by simp
   1.740      hence ?lhs ..}
   1.741    moreover
   1.742 @@ -1023,10 +1023,10 @@
   1.743          by (rule dvd_imp_degree_le)
   1.744        with lgpq have ?rhs by simp }
   1.745      ultimately have ?rhs by blast }
   1.746 -  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast) 
   1.747 +  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast)
   1.748  qed
   1.749  
   1.750 -lemma poly_divides_conv1: 
   1.751 +lemma poly_divides_conv1:
   1.752    assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
   1.753    and qrp': "smult a q - p' \<equiv> r"
   1.754    shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
   1.755 @@ -1046,7 +1046,7 @@
   1.756        by (simp add: algebra_simps mult_smult_right smult_smult)
   1.757      hence ?lhs ..}
   1.758    ultimately have "?lhs = ?rhs" by blast }
   1.759 -thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast) 
   1.760 +thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
   1.761  qed
   1.762  
   1.763  lemma basic_cqe_conv1:
   1.764 @@ -1056,8 +1056,8 @@
   1.765    "(\<exists>x. poly 0 x = 0) \<equiv> True"
   1.766    "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
   1.767  
   1.768 -lemma basic_cqe_conv2: 
   1.769 -  assumes l:"p \<noteq> 0" 
   1.770 +lemma basic_cqe_conv2:
   1.771 +  assumes l:"p \<noteq> 0"
   1.772    shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
   1.773  proof-
   1.774    {fix h t
   1.775 @@ -1065,7 +1065,7 @@
   1.776      with l have False by simp}
   1.777    hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
   1.778      by blast
   1.779 -  from fundamental_theorem_of_algebra_alt[OF th] 
   1.780 +  from fundamental_theorem_of_algebra_alt[OF th]
   1.781    show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
   1.782  qed
   1.783  
   1.784 @@ -1080,7 +1080,7 @@
   1.785  
   1.786  lemma basic_cqe_conv3:
   1.787    fixes p q :: "complex poly"
   1.788 -  assumes l: "p \<noteq> 0" 
   1.789 +  assumes l: "p \<noteq> 0"
   1.790    shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
   1.791  proof-
   1.792    from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
   1.793 @@ -1108,7 +1108,7 @@
   1.794  lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
   1.795  
   1.796  lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
   1.797 -lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)" 
   1.798 +lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)"
   1.799    by (atomize (full)) simp_all
   1.800  lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
   1.801  lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")