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.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.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.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.203  text{* Polynomial is continuous. *}
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.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.307 -	from fz(2)[rule_format, OF d(1)] obtain N1 where
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.355 -lemma cispi: "cis pi = -1"
1.356 +lemma cispi: "cis pi = -1"
1.357    unfolding cis_def
1.358    by simp
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.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.425 -text {* Decomposition of polynomial, skipping zero coefficients
1.426 +text {* Decomposition of polynomial, skipping zero coefficients
1.427    after the first.  *}
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.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.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.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.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.691  (* Arithmetic operations on multivariate polynomials.                        *)
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.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.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.706 @@ -982,9 +982,9 @@
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.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.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.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.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.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.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.784 @@ -1080,7 +1080,7 @@
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.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")