Moved FTA into Lib and cleaned it up a little.
authornipkow
Thu Feb 12 18:14:43 2009 +0100 (2009-02-12)
changeset 298794425849f5db7
parent 29878 06efd6e731c6
child 29880 3dee8ff45d3d
Moved FTA into Lib and cleaned it up a little.
src/HOL/Complex_Main.thy
src/HOL/Finite_Set.thy
src/HOL/Fundamental_Theorem_Algebra.thy
src/HOL/IsaMakefile
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Library.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Wed Feb 11 11:22:42 2009 -0800
     1.2 +++ b/src/HOL/Complex_Main.thy	Thu Feb 12 18:14:43 2009 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  imports
     1.5    Main
     1.6    Real
     1.7 -  Fundamental_Theorem_Algebra
     1.8 +  Complex
     1.9    Log
    1.10    Ln
    1.11    Taylor
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 11 11:22:42 2009 -0800
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Feb 12 18:14:43 2009 +0100
     2.3 @@ -2029,6 +2029,19 @@
     2.4    show False by simp (blast dest: Suc_neq_Zero surjD)
     2.5  qed
     2.6  
     2.7 +lemma infinite_UNIV_char_0:
     2.8 +  "\<not> finite (UNIV::'a::semiring_char_0 set)"
     2.9 +proof
    2.10 +  assume "finite (UNIV::'a set)"
    2.11 +  with subset_UNIV have "finite (range of_nat::'a set)"
    2.12 +    by (rule finite_subset)
    2.13 +  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
    2.14 +    by (simp add: inj_on_def)
    2.15 +  ultimately have "finite (UNIV::nat set)"
    2.16 +    by (rule finite_imageD)
    2.17 +  then show "False"
    2.18 +    by (simp add: infinite_UNIV_nat)
    2.19 +qed
    2.20  
    2.21  subsection{* A fold functional for non-empty sets *}
    2.22  
     3.1 --- a/src/HOL/Fundamental_Theorem_Algebra.thy	Wed Feb 11 11:22:42 2009 -0800
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1396 +0,0 @@
     3.4 -(* Author: Amine Chaieb, TU Muenchen *)
     3.5 -
     3.6 -header{*Fundamental Theorem of Algebra*}
     3.7 -
     3.8 -theory Fundamental_Theorem_Algebra
     3.9 -imports Polynomial Complex
    3.10 -begin
    3.11 -
    3.12 -subsection {* Square root of complex numbers *}
    3.13 -definition csqrt :: "complex \<Rightarrow> complex" where
    3.14 -"csqrt z = (if Im z = 0 then
    3.15 -            if 0 \<le> Re z then Complex (sqrt(Re z)) 0
    3.16 -            else Complex 0 (sqrt(- Re z))
    3.17 -           else Complex (sqrt((cmod z + Re z) /2))
    3.18 -                        ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
    3.19 -
    3.20 -lemma csqrt[algebra]: "csqrt z ^ 2 = z"
    3.21 -proof-
    3.22 -  obtain x y where xy: "z = Complex x y" by (cases z)
    3.23 -  {assume y0: "y = 0"
    3.24 -    {assume x0: "x \<ge> 0" 
    3.25 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
    3.26 -	by (simp add: csqrt_def power2_eq_square)}
    3.27 -    moreover
    3.28 -    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
    3.29 -      then have ?thesis using y0 xy real_sqrt_pow2[OF x0] 
    3.30 -	by (simp add: csqrt_def power2_eq_square) }
    3.31 -    ultimately have ?thesis by blast}
    3.32 -  moreover
    3.33 -  {assume y0: "y\<noteq>0"
    3.34 -    {fix x y
    3.35 -      let ?z = "Complex x y"
    3.36 -      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
    3.37 -      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ 
    3.38 -      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) }
    3.39 -    note th = this
    3.40 -    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" 
    3.41 -      by (simp add: power2_eq_square) 
    3.42 -    from th[of x y]
    3.43 -    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
    3.44 -    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"
    3.45 -      unfolding power2_eq_square by simp 
    3.46 -    have "sqrt 4 = sqrt (2^2)" by simp 
    3.47 -    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
    3.48 -    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
    3.49 -      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
    3.50 -      unfolding power2_eq_square 
    3.51 -      by (simp add: algebra_simps real_sqrt_divide sqrt4)
    3.52 -     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
    3.53 -       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])
    3.54 -      using th1 th2  ..}
    3.55 -  ultimately show ?thesis by blast
    3.56 -qed
    3.57 -
    3.58 -
    3.59 -subsection{* More lemmas about module of complex numbers *}
    3.60 -
    3.61 -lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
    3.62 -  by (rule of_real_power [symmetric])
    3.63 -
    3.64 -lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
    3.65 -  apply (rule exI[where x = "min d1 d2 / 2"])
    3.66 -  by (simp add: field_simps min_def)
    3.67 -
    3.68 -text{* The triangle inequality for cmod *}
    3.69 -lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
    3.70 -  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
    3.71 -
    3.72 -subsection{* Basic lemmas about complex polynomials *}
    3.73 -
    3.74 -lemma poly_bound_exists:
    3.75 -  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
    3.76 -proof(induct p)
    3.77 -  case 0 thus ?case by (rule exI[where x=1], simp) 
    3.78 -next
    3.79 -  case (pCons c cs)
    3.80 -  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
    3.81 -    by blast
    3.82 -  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
    3.83 -  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
    3.84 -  {fix z
    3.85 -    assume H: "cmod z \<le> r"
    3.86 -    from m H have th: "cmod (poly cs z) \<le> m" by blast
    3.87 -    from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
    3.88 -    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
    3.89 -      using norm_triangle_ineq[of c "z* poly cs z"] by simp
    3.90 -    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
    3.91 -    also have "\<dots> \<le> ?k" by simp
    3.92 -    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
    3.93 -  with kp show ?case by blast
    3.94 -qed
    3.95 -
    3.96 -
    3.97 -text{* Offsetting the variable in a polynomial gives another of same degree *}
    3.98 -
    3.99 -definition
   3.100 -  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
   3.101 -
   3.102 -lemma offset_poly_0: "offset_poly 0 h = 0"
   3.103 -  unfolding offset_poly_def by (simp add: poly_rec_0)
   3.104 -
   3.105 -lemma offset_poly_pCons:
   3.106 -  "offset_poly (pCons a p) h =
   3.107 -    smult h (offset_poly p h) + pCons a (offset_poly p h)"
   3.108 -  unfolding offset_poly_def by (simp add: poly_rec_pCons)
   3.109 -
   3.110 -lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
   3.111 -by (simp add: offset_poly_pCons offset_poly_0)
   3.112 -
   3.113 -lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
   3.114 -apply (induct p)
   3.115 -apply (simp add: offset_poly_0)
   3.116 -apply (simp add: offset_poly_pCons algebra_simps)
   3.117 -done
   3.118 -
   3.119 -lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
   3.120 -by (induct p arbitrary: a, simp, force)
   3.121 -
   3.122 -lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
   3.123 -apply (safe intro!: offset_poly_0)
   3.124 -apply (induct p, simp)
   3.125 -apply (simp add: offset_poly_pCons)
   3.126 -apply (frule offset_poly_eq_0_lemma, simp)
   3.127 -done
   3.128 -
   3.129 -lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
   3.130 -apply (induct p)
   3.131 -apply (simp add: offset_poly_0)
   3.132 -apply (case_tac "p = 0")
   3.133 -apply (simp add: offset_poly_0 offset_poly_pCons)
   3.134 -apply (simp add: offset_poly_pCons)
   3.135 -apply (subst degree_add_eq_right)
   3.136 -apply (rule le_less_trans [OF degree_smult_le])
   3.137 -apply (simp add: offset_poly_eq_0_iff)
   3.138 -apply (simp add: offset_poly_eq_0_iff)
   3.139 -done
   3.140 -
   3.141 -definition
   3.142 -  "psize p = (if p = 0 then 0 else Suc (degree p))"
   3.143 -
   3.144 -lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
   3.145 -  unfolding psize_def by simp
   3.146 -
   3.147 -lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
   3.148 -proof (intro exI conjI)
   3.149 -  show "psize (offset_poly p a) = psize p"
   3.150 -    unfolding psize_def
   3.151 -    by (simp add: offset_poly_eq_0_iff degree_offset_poly)
   3.152 -  show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
   3.153 -    by (simp add: poly_offset_poly)
   3.154 -qed
   3.155 -
   3.156 -text{* An alternative useful formulation of completeness of the reals *}
   3.157 -lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
   3.158 -  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
   3.159 -proof-
   3.160 -  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
   3.161 -  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
   3.162 -  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y" 
   3.163 -    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
   3.164 -  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
   3.165 -    by blast
   3.166 -  from Y[OF x] have xY: "x < Y" .
   3.167 -  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)  
   3.168 -  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y" 
   3.169 -    apply (clarsimp, atomize (full)) by auto 
   3.170 -  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
   3.171 -  {fix y
   3.172 -    {fix z assume z: "P z" "y < z"
   3.173 -      from L' z have "y < L" by auto }
   3.174 -    moreover
   3.175 -    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
   3.176 -      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
   3.177 -      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def) 
   3.178 -      with yL(1) have False  by arith}
   3.179 -    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
   3.180 -  thus ?thesis by blast
   3.181 -qed
   3.182 -
   3.183 -
   3.184 -subsection{* Some theorems about Sequences*}
   3.185 -text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
   3.186 -
   3.187 -lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   3.188 -  unfolding Ex1_def
   3.189 -  apply (rule_tac x="nat_rec e f" in exI)
   3.190 -  apply (rule conjI)+
   3.191 -apply (rule def_nat_rec_0, simp)
   3.192 -apply (rule allI, rule def_nat_rec_Suc, simp)
   3.193 -apply (rule allI, rule impI, rule ext)
   3.194 -apply (erule conjE)
   3.195 -apply (induct_tac x)
   3.196 -apply (simp add: nat_rec_0)
   3.197 -apply (erule_tac x="n" in allE)
   3.198 -apply (simp)
   3.199 -done
   3.200 -
   3.201 - text{* An equivalent formulation of monotony -- Not used here, but might be useful *}
   3.202 -lemma mono_Suc: "mono f = (\<forall>n. (f n :: 'a :: order) \<le> f (Suc n))"
   3.203 -unfolding mono_def
   3.204 -proof auto
   3.205 -  fix A B :: nat
   3.206 -  assume H: "\<forall>n. f n \<le> f (Suc n)" "A \<le> B"
   3.207 -  hence "\<exists>k. B = A + k" apply -  apply (thin_tac "\<forall>n. f n \<le> f (Suc n)") 
   3.208 -    by presburger
   3.209 -  then obtain k where k: "B = A + k" by blast
   3.210 -  {fix a k
   3.211 -    have "f a \<le> f (a + k)"
   3.212 -    proof (induct k)
   3.213 -      case 0 thus ?case by simp
   3.214 -    next
   3.215 -      case (Suc k)
   3.216 -      from Suc.hyps H(1)[rule_format, of "a + k"] show ?case by simp
   3.217 -    qed}
   3.218 -  with k show "f A \<le> f B" by blast
   3.219 -qed
   3.220 -
   3.221 -text{* for any sequence, there is a mootonic subsequence *}
   3.222 -lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
   3.223 -proof-
   3.224 -  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
   3.225 -    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
   3.226 -    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
   3.227 -    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
   3.228 -    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
   3.229 -      using H apply - 
   3.230 -      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
   3.231 -      unfolding order_le_less by blast 
   3.232 -    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
   3.233 -    {fix n
   3.234 -      have "?P (f (Suc n)) (f n)" 
   3.235 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   3.236 -	using H apply - 
   3.237 -      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
   3.238 -      unfolding order_le_less by blast 
   3.239 -    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
   3.240 -  note fSuc = this
   3.241 -    {fix p q assume pq: "p \<ge> f q"
   3.242 -      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
   3.243 -	by (cases q, simp_all) }
   3.244 -    note pqth = this
   3.245 -    {fix q
   3.246 -      have "f (Suc q) > f q" apply (induct q) 
   3.247 -	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
   3.248 -    note fss = this
   3.249 -    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
   3.250 -    {fix a b 
   3.251 -      have "f a \<le> f (a + b)"
   3.252 -      proof(induct b)
   3.253 -	case 0 thus ?case by simp
   3.254 -      next
   3.255 -	case (Suc b)
   3.256 -	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
   3.257 -      qed}
   3.258 -    note fmon0 = this
   3.259 -    have "monoseq (\<lambda>n. s (f n))" 
   3.260 -    proof-
   3.261 -      {fix n
   3.262 -	have "s (f n) \<ge> s (f (Suc n))" 
   3.263 -	proof(cases n)
   3.264 -	  case 0
   3.265 -	  assume n0: "n = 0"
   3.266 -	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
   3.267 -	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
   3.268 -	next
   3.269 -	  case (Suc m)
   3.270 -	  assume m: "n = Suc m"
   3.271 -	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
   3.272 -	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
   3.273 -	qed}
   3.274 -      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
   3.275 -    qed
   3.276 -    with th1 have ?thesis by blast}
   3.277 -  moreover
   3.278 -  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
   3.279 -    {fix p assume p: "p \<ge> Suc N" 
   3.280 -      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
   3.281 -      have "m \<noteq> p" using m(2) by auto 
   3.282 -      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
   3.283 -    note th0 = this
   3.284 -    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
   3.285 -    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
   3.286 -    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
   3.287 -      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
   3.288 -    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
   3.289 -      using N apply - 
   3.290 -      apply (erule allE[where x="Suc N"], clarsimp)
   3.291 -      apply (rule_tac x="m" in exI)
   3.292 -      apply auto
   3.293 -      apply (subgoal_tac "Suc N \<noteq> m")
   3.294 -      apply simp
   3.295 -      apply (rule ccontr, simp)
   3.296 -      done
   3.297 -    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
   3.298 -    {fix n
   3.299 -      have "f n > N \<and> ?P (f (Suc n)) (f n)"
   3.300 -	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   3.301 -      proof (induct n)
   3.302 -	case 0 thus ?case
   3.303 -	  using f0 N apply auto 
   3.304 -	  apply (erule allE[where x="f 0"], clarsimp) 
   3.305 -	  apply (rule_tac x="m" in exI, simp)
   3.306 -	  by (subgoal_tac "f 0 \<noteq> m", auto)
   3.307 -      next
   3.308 -	case (Suc n)
   3.309 -	from Suc.hyps have Nfn: "N < f n" by blast
   3.310 -	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   3.311 -	with Nfn have mN: "m > N" by arith
   3.312 -	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   3.313 -	
   3.314 -	from key have th0: "f (Suc n) > N" by simp
   3.315 -	from N[rule_format, OF th0]
   3.316 -	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   3.317 -	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   3.318 -	hence "m' > f (Suc n)" using m'(1) by simp
   3.319 -	with key m'(2) show ?case by auto
   3.320 -      qed}
   3.321 -    note fSuc = this
   3.322 -    {fix n
   3.323 -      have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto 
   3.324 -      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
   3.325 -    note thf = this
   3.326 -    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
   3.327 -    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
   3.328 -      apply -
   3.329 -      apply (rule disjI1)
   3.330 -      apply auto
   3.331 -      apply (rule order_less_imp_le)
   3.332 -      apply blast
   3.333 -      done
   3.334 -    then have ?thesis  using sqf by blast}
   3.335 -  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
   3.336 -qed
   3.337 -
   3.338 -lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
   3.339 -proof(induct n)
   3.340 -  case 0 thus ?case by simp
   3.341 -next
   3.342 -  case (Suc n)
   3.343 -  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
   3.344 -  have "n < f (Suc n)" by arith 
   3.345 -  thus ?case by arith
   3.346 -qed
   3.347 -
   3.348 -subsection {* Fundamental theorem of algebra *}
   3.349 -lemma  unimodular_reduce_norm:
   3.350 -  assumes md: "cmod z = 1"
   3.351 -  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
   3.352 -proof-
   3.353 -  obtain x y where z: "z = Complex x y " by (cases z, auto)
   3.354 -  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
   3.355 -  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
   3.356 -    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
   3.357 -      by (simp_all add: cmod_def power2_eq_square algebra_simps)
   3.358 -    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
   3.359 -    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
   3.360 -      by - (rule power_mono, simp, simp)+
   3.361 -    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1" 
   3.362 -      by (simp_all  add: power2_abs power_mult_distrib)
   3.363 -    from add_mono[OF th0] xy have False by simp }
   3.364 -  thus ?thesis unfolding linorder_not_le[symmetric] by blast
   3.365 -qed
   3.366 -
   3.367 -text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
   3.368 -lemma reduce_poly_simple:
   3.369 - assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
   3.370 -  shows "\<exists>z. cmod (1 + b * z^n) < 1"
   3.371 -using n
   3.372 -proof(induct n rule: nat_less_induct)
   3.373 -  fix n
   3.374 -  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
   3.375 -  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
   3.376 -  {assume e: "even n"
   3.377 -    hence "\<exists>m. n = 2*m" by presburger
   3.378 -    then obtain m where m: "n = 2*m" by blast
   3.379 -    from n m have "m\<noteq>0" "m < n" by presburger+
   3.380 -    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
   3.381 -    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
   3.382 -    hence "\<exists>z. ?P z n" ..}
   3.383 -  moreover
   3.384 -  {assume o: "odd n"
   3.385 -    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
   3.386 -    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
   3.387 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = 
   3.388 -    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
   3.389 -    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2" 
   3.390 -      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
   3.391 -      by (simp add: power2_eq_square)
   3.392 -    finally 
   3.393 -    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
   3.394 -    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
   3.395 -    1" 
   3.396 -      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
   3.397 -      using right_inverse[OF b']
   3.398 -      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
   3.399 -    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   3.400 -      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
   3.401 -      by (simp add: real_sqrt_mult[symmetric] th0)        
   3.402 -    from o have "\<exists>m. n = Suc (2*m)" by presburger+
   3.403 -    then obtain m where m: "n = Suc (2*m)" by blast
   3.404 -    from unimodular_reduce_norm[OF th0] o
   3.405 -    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
   3.406 -      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
   3.407 -      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
   3.408 -      apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   3.409 -      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
   3.410 -      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
   3.411 -      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
   3.412 -      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
   3.413 -      done
   3.414 -    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   3.415 -    let ?w = "v / complex_of_real (root n (cmod b))"
   3.416 -    from odd_real_root_pow[OF o, of "cmod b"]
   3.417 -    have th1: "?w ^ n = v^n / complex_of_real (cmod b)" 
   3.418 -      by (simp add: power_divide complex_of_real_power)
   3.419 -    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
   3.420 -    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
   3.421 -    have th4: "cmod (complex_of_real (cmod b) / b) *
   3.422 -   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
   3.423 -   < cmod (complex_of_real (cmod b) / b) * 1"
   3.424 -      apply (simp only: norm_mult[symmetric] right_distrib)
   3.425 -      using b v by (simp add: th2)
   3.426 -
   3.427 -    from mult_less_imp_less_left[OF th4 th3]
   3.428 -    have "?P ?w n" unfolding th1 . 
   3.429 -    hence "\<exists>z. ?P z n" .. }
   3.430 -  ultimately show "\<exists>z. ?P z n" by blast
   3.431 -qed
   3.432 -
   3.433 -
   3.434 -text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
   3.435 -
   3.436 -lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
   3.437 -  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
   3.438 -  unfolding cmod_def by simp
   3.439 -
   3.440 -lemma bolzano_weierstrass_complex_disc:
   3.441 -  assumes r: "\<forall>n. cmod (s n) \<le> r"
   3.442 -  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   3.443 -proof-
   3.444 -  from seq_monosub[of "Re o s"] 
   3.445 -  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))" 
   3.446 -    unfolding o_def by blast
   3.447 -  from seq_monosub[of "Im o s o f"] 
   3.448 -  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast  
   3.449 -  let ?h = "f o g"
   3.450 -  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith 
   3.451 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>" 
   3.452 -  proof
   3.453 -    fix n
   3.454 -    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
   3.455 -  qed
   3.456 -  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
   3.457 -    apply (rule Bseq_monoseq_convergent)
   3.458 -    apply (simp add: Bseq_def)
   3.459 -    apply (rule exI[where x= "r + 1"])
   3.460 -    using th rp apply simp
   3.461 -    using f(2) .
   3.462 -  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>" 
   3.463 -  proof
   3.464 -    fix n
   3.465 -    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
   3.466 -  qed
   3.467 -
   3.468 -  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
   3.469 -    apply (rule Bseq_monoseq_convergent)
   3.470 -    apply (simp add: Bseq_def)
   3.471 -    apply (rule exI[where x= "r + 1"])
   3.472 -    using th rp apply simp
   3.473 -    using g(2) .
   3.474 -
   3.475 -  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x" 
   3.476 -    by blast 
   3.477 -  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r" 
   3.478 -    unfolding LIMSEQ_def real_norm_def .
   3.479 -
   3.480 -  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y" 
   3.481 -    by blast 
   3.482 -  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r" 
   3.483 -    unfolding LIMSEQ_def real_norm_def .
   3.484 -  let ?w = "Complex x y"
   3.485 -  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto 
   3.486 -  {fix e assume ep: "e > (0::real)"
   3.487 -    hence e2: "e/2 > 0" by simp
   3.488 -    from x[rule_format, OF e2] y[rule_format, OF e2]
   3.489 -    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
   3.490 -    {fix n assume nN12: "n \<ge> N1 + N2"
   3.491 -      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
   3.492 -      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
   3.493 -      have "cmod (s (?h n) - ?w) < e" 
   3.494 -	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
   3.495 -    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
   3.496 -  with hs show ?thesis  by blast  
   3.497 -qed
   3.498 -
   3.499 -text{* Polynomial is continuous. *}
   3.500 -
   3.501 -lemma poly_cont:
   3.502 -  assumes ep: "e > 0" 
   3.503 -  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
   3.504 -proof-
   3.505 -  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
   3.506 -  proof
   3.507 -    show "degree (offset_poly p z) = degree p"
   3.508 -      by (rule degree_offset_poly)
   3.509 -    show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
   3.510 -      by (rule poly_offset_poly)
   3.511 -  qed
   3.512 -  {fix w
   3.513 -    note q(2)[of "w - z", simplified]}
   3.514 -  note th = this
   3.515 -  show ?thesis unfolding th[symmetric]
   3.516 -  proof(induct q)
   3.517 -    case 0 thus ?case  using ep by auto
   3.518 -  next
   3.519 -    case (pCons c cs)
   3.520 -    from poly_bound_exists[of 1 "cs"] 
   3.521 -    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
   3.522 -    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
   3.523 -    have one0: "1 > (0::real)"  by arith
   3.524 -    from real_lbound_gt_zero[OF one0 em0] 
   3.525 -    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
   3.526 -    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e" 
   3.527 -      by (simp_all add: field_simps real_mult_order)
   3.528 -    show ?case 
   3.529 -      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   3.530 -	fix d w
   3.531 -	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
   3.532 -	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
   3.533 -	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
   3.534 -	from H have th: "cmod (w-z) \<le> d" by simp 
   3.535 -	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
   3.536 -	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
   3.537 -      qed  
   3.538 -    qed
   3.539 -qed
   3.540 -
   3.541 -text{* Hence a polynomial attains minimum on a closed disc 
   3.542 -  in the complex plane. *}
   3.543 -lemma  poly_minimum_modulus_disc:
   3.544 -  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
   3.545 -proof-
   3.546 -  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
   3.547 -      apply -
   3.548 -      apply (rule exI[where x=0]) 
   3.549 -      apply auto
   3.550 -      apply (subgoal_tac "cmod w < 0")
   3.551 -      apply simp
   3.552 -      apply arith
   3.553 -      done }
   3.554 -  moreover
   3.555 -  {assume rp: "r \<ge> 0"
   3.556 -    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp 
   3.557 -    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
   3.558 -    {fix x z
   3.559 -      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
   3.560 -      hence "- x < 0 " by arith
   3.561 -      with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
   3.562 -    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
   3.563 -    from real_sup_exists[OF mth1 mth2] obtain s where 
   3.564 -      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
   3.565 -    let ?m = "-s"
   3.566 -    {fix y
   3.567 -      from s[rule_format, of "-y"] have 
   3.568 -    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" 
   3.569 -	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
   3.570 -    note s1 = this[unfolded minus_minus]
   3.571 -    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m" 
   3.572 -      by auto
   3.573 -    {fix n::nat
   3.574 -      from s1[rule_format, of "?m + 1/real (Suc n)"] 
   3.575 -      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
   3.576 -	by simp}
   3.577 -    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
   3.578 -    from choice[OF th] obtain g where 
   3.579 -      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)" 
   3.580 -      by blast
   3.581 -    from bolzano_weierstrass_complex_disc[OF g(1)] 
   3.582 -    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   3.583 -      by blast    
   3.584 -    {fix w 
   3.585 -      assume wr: "cmod w \<le> r"
   3.586 -      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
   3.587 -      {assume e: "?e > 0"
   3.588 -	hence e2: "?e/2 > 0" by simp
   3.589 -	from poly_cont[OF e2, of z p] obtain d where
   3.590 -	  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
   3.591 -	{fix w assume w: "cmod (w - z) < d"
   3.592 -	  have "cmod(poly p w - poly p z) < ?e / 2"
   3.593 -	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
   3.594 -	note th1 = this
   3.595 -	
   3.596 -	from fz(2)[rule_format, OF d(1)] obtain N1 where 
   3.597 -	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
   3.598 -	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
   3.599 -	  N2: "2/?e < real N2" by blast
   3.600 -	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
   3.601 -	  using N1[rule_format, of "N1 + N2"] th1 by simp
   3.602 -	{fix a b e2 m :: real
   3.603 -	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
   3.604 -          ==> False" by arith}
   3.605 -      note th0 = this
   3.606 -      have ath: 
   3.607 -	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
   3.608 -      from s1m[OF g(1)[rule_format]]
   3.609 -      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   3.610 -      from seq_suble[OF fz(1), of "N1+N2"]
   3.611 -      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
   3.612 -      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"  
   3.613 -	using N2 by auto
   3.614 -      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
   3.615 -      from g(2)[rule_format, of "f (N1 + N2)"]
   3.616 -      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
   3.617 -      from order_less_le_trans[OF th01 th00]
   3.618 -      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
   3.619 -      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
   3.620 -      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   3.621 -      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
   3.622 -      with ath[OF th31 th32]
   3.623 -      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith  
   3.624 -      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c" 
   3.625 -	by arith
   3.626 -      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
   3.627 -\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)" 
   3.628 -	by (simp add: norm_triangle_ineq3)
   3.629 -      from ath2[OF th22, of ?m]
   3.630 -      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
   3.631 -      from th0[OF th2 thc1 thc2] have False .}
   3.632 -      hence "?e = 0" by auto
   3.633 -      then have "cmod (poly p z) = ?m" by simp  
   3.634 -      with s1m[OF wr]
   3.635 -      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
   3.636 -    hence ?thesis by blast}
   3.637 -  ultimately show ?thesis by blast
   3.638 -qed
   3.639 -
   3.640 -lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
   3.641 -  unfolding power2_eq_square
   3.642 -  apply (simp add: rcis_mult)
   3.643 -  apply (simp add: power2_eq_square[symmetric])
   3.644 -  done
   3.645 -
   3.646 -lemma cispi: "cis pi = -1" 
   3.647 -  unfolding cis_def
   3.648 -  by simp
   3.649 -
   3.650 -lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
   3.651 -  unfolding power2_eq_square
   3.652 -  apply (simp add: rcis_mult add_divide_distrib)
   3.653 -  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
   3.654 -  done
   3.655 -
   3.656 -text {* Nonzero polynomial in z goes to infinity as z does. *}
   3.657 -
   3.658 -lemma poly_infinity:
   3.659 -  assumes ex: "p \<noteq> 0"
   3.660 -  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
   3.661 -using ex
   3.662 -proof(induct p arbitrary: a d)
   3.663 -  case (pCons c cs a d) 
   3.664 -  {assume H: "cs \<noteq> 0"
   3.665 -    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
   3.666 -    let ?r = "1 + \<bar>r\<bar>"
   3.667 -    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
   3.668 -      have r0: "r \<le> cmod z" using h by arith
   3.669 -      from r[rule_format, OF r0]
   3.670 -      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
   3.671 -      from h have z1: "cmod z \<ge> 1" by arith
   3.672 -      from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
   3.673 -      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
   3.674 -	unfolding norm_mult by (simp add: algebra_simps)
   3.675 -      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
   3.676 -      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   3.677 -	by (simp add: diff_le_eq algebra_simps) 
   3.678 -      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
   3.679 -    hence ?case by blast}
   3.680 -  moreover
   3.681 -  {assume cs0: "\<not> (cs \<noteq> 0)"
   3.682 -    with pCons.prems have c0: "c \<noteq> 0" by simp
   3.683 -    from cs0 have cs0': "cs = 0" by simp
   3.684 -    {fix z
   3.685 -      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
   3.686 -      from c0 have "cmod c > 0" by simp
   3.687 -      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)" 
   3.688 -	by (simp add: field_simps norm_mult)
   3.689 -      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
   3.690 -      from complex_mod_triangle_sub[of "z*c" a ]
   3.691 -      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
   3.692 -	by (simp add: algebra_simps)
   3.693 -      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   3.694 -        using cs0' by simp}
   3.695 -    then have ?case  by blast}
   3.696 -  ultimately show ?case by blast
   3.697 -qed simp
   3.698 -
   3.699 -text {* Hence polynomial's modulus attains its minimum somewhere. *}
   3.700 -lemma poly_minimum_modulus:
   3.701 -  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   3.702 -proof(induct p)
   3.703 -  case (pCons c cs) 
   3.704 -  {assume cs0: "cs \<noteq> 0"
   3.705 -    from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
   3.706 -    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
   3.707 -    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
   3.708 -    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"] 
   3.709 -    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
   3.710 -    {fix z assume z: "r \<le> cmod z"
   3.711 -      from v[of 0] r[OF z] 
   3.712 -      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
   3.713 -	by simp }
   3.714 -    note v0 = this
   3.715 -    from v0 v ath[of r] have ?case by blast}
   3.716 -  moreover
   3.717 -  {assume cs0: "\<not> (cs \<noteq> 0)"
   3.718 -    hence th:"cs = 0" by simp
   3.719 -    from th pCons.hyps have ?case by simp}
   3.720 -  ultimately show ?case by blast
   3.721 -qed simp
   3.722 -
   3.723 -text{* Constant function (non-syntactic characterization). *}
   3.724 -definition "constant f = (\<forall>x y. f x = f y)"
   3.725 -
   3.726 -lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
   3.727 -  unfolding constant_def psize_def
   3.728 -  apply (induct p, auto)
   3.729 -  done
   3.730 - 
   3.731 -lemma poly_replicate_append:
   3.732 -  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
   3.733 -  by (simp add: poly_monom)
   3.734 -
   3.735 -text {* Decomposition of polynomial, skipping zero coefficients 
   3.736 -  after the first.  *}
   3.737 -
   3.738 -lemma poly_decompose_lemma:
   3.739 - assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
   3.740 -  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and> 
   3.741 -                 (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   3.742 -unfolding psize_def
   3.743 -using nz
   3.744 -proof(induct p)
   3.745 -  case 0 thus ?case by simp
   3.746 -next
   3.747 -  case (pCons c cs)
   3.748 -  {assume c0: "c = 0"
   3.749 -    from pCons.hyps pCons.prems c0 have ?case apply auto
   3.750 -      apply (rule_tac x="k+1" in exI)
   3.751 -      apply (rule_tac x="a" in exI, clarsimp)
   3.752 -      apply (rule_tac x="q" in exI)
   3.753 -      by (auto simp add: power_Suc)}
   3.754 -  moreover
   3.755 -  {assume c0: "c\<noteq>0"
   3.756 -    hence ?case apply-
   3.757 -      apply (rule exI[where x=0])
   3.758 -      apply (rule exI[where x=c], clarsimp)
   3.759 -      apply (rule exI[where x=cs])
   3.760 -      apply auto
   3.761 -      done}
   3.762 -  ultimately show ?case by blast
   3.763 -qed
   3.764 -
   3.765 -lemma poly_decompose:
   3.766 -  assumes nc: "~constant(poly p)"
   3.767 -  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
   3.768 -               psize q + k + 1 = psize p \<and> 
   3.769 -              (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   3.770 -using nc 
   3.771 -proof(induct p)
   3.772 -  case 0 thus ?case by (simp add: constant_def)
   3.773 -next
   3.774 -  case (pCons c cs)
   3.775 -  {assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   3.776 -    {fix x y
   3.777 -      from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)}
   3.778 -    with pCons.prems have False by (auto simp add: constant_def)}
   3.779 -  hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
   3.780 -  from poly_decompose_lemma[OF th] 
   3.781 -  show ?case 
   3.782 -    apply clarsimp
   3.783 -    apply (rule_tac x="k+1" in exI)
   3.784 -    apply (rule_tac x="a" in exI)
   3.785 -    apply simp
   3.786 -    apply (rule_tac x="q" in exI)
   3.787 -    apply (auto simp add: power_Suc)
   3.788 -    apply (auto simp add: psize_def split: if_splits)
   3.789 -    done
   3.790 -qed
   3.791 -
   3.792 -text{* Fundamental theorem of algebral *}
   3.793 -
   3.794 -lemma fundamental_theorem_of_algebra:
   3.795 -  assumes nc: "~constant(poly p)"
   3.796 -  shows "\<exists>z::complex. poly p z = 0"
   3.797 -using nc
   3.798 -proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
   3.799 -  fix n fix p :: "complex poly"
   3.800 -  let ?p = "poly p"
   3.801 -  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
   3.802 -  let ?ths = "\<exists>z. ?p z = 0"
   3.803 -
   3.804 -  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
   3.805 -  from poly_minimum_modulus obtain c where 
   3.806 -    c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
   3.807 -  {assume pc: "?p c = 0" hence ?ths by blast}
   3.808 -  moreover
   3.809 -  {assume pc0: "?p c \<noteq> 0"
   3.810 -    from poly_offset[of p c] obtain q where
   3.811 -      q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
   3.812 -    {assume h: "constant (poly q)"
   3.813 -      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
   3.814 -      {fix x y
   3.815 -	from th have "?p x = poly q (x - c)" by auto 
   3.816 -	also have "\<dots> = poly q (y - c)" 
   3.817 -	  using h unfolding constant_def by blast
   3.818 -	also have "\<dots> = ?p y" using th by auto
   3.819 -	finally have "?p x = ?p y" .}
   3.820 -      with nc have False unfolding constant_def by blast }
   3.821 -    hence qnc: "\<not> constant (poly q)" by blast
   3.822 -    from q(2) have pqc0: "?p c = poly q 0" by simp
   3.823 -    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp 
   3.824 -    let ?a0 = "poly q 0"
   3.825 -    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp 
   3.826 -    from a00 
   3.827 -    have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   3.828 -      by simp
   3.829 -    let ?r = "smult (inverse ?a0) q"
   3.830 -    have lgqr: "psize q = psize ?r"
   3.831 -      using a00 unfolding psize_def degree_def
   3.832 -      by (simp add: expand_poly_eq)
   3.833 -    {assume h: "\<And>x y. poly ?r x = poly ?r y"
   3.834 -      {fix x y
   3.835 -	from qr[rule_format, of x] 
   3.836 -	have "poly q x = poly ?r x * ?a0" by auto
   3.837 -	also have "\<dots> = poly ?r y * ?a0" using h by simp
   3.838 -	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
   3.839 -	finally have "poly q x = poly q y" .} 
   3.840 -      with qnc have False unfolding constant_def by blast}
   3.841 -    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
   3.842 -    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
   3.843 -    {fix w 
   3.844 -      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   3.845 -	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
   3.846 -      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   3.847 -	using a00 unfolding norm_divide by (simp add: field_simps)
   3.848 -      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
   3.849 -    note mrmq_eq = this
   3.850 -    from poly_decompose[OF rnc] obtain k a s where 
   3.851 -      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r" 
   3.852 -      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   3.853 -    {assume "k + 1 = n"
   3.854 -      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
   3.855 -      {fix w
   3.856 -	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" 
   3.857 -	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
   3.858 -      note hth = this [symmetric]
   3.859 -	from reduce_poly_simple[OF kas(1,2)] 
   3.860 -      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
   3.861 -    moreover
   3.862 -    {assume kn: "k+1 \<noteq> n"
   3.863 -      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
   3.864 -      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))" 
   3.865 -	unfolding constant_def poly_pCons poly_monom
   3.866 -	using kas(1) apply simp 
   3.867 -	by (rule exI[where x=0], rule exI[where x=1], simp)
   3.868 -      from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
   3.869 -	by (simp add: psize_def degree_monom_eq)
   3.870 -      from H[rule_format, OF k1n th01 th02]
   3.871 -      obtain w where w: "1 + w^k * a = 0"
   3.872 -	unfolding poly_pCons poly_monom
   3.873 -	using kas(2) by (cases k, auto simp add: algebra_simps)
   3.874 -      from poly_bound_exists[of "cmod w" s] obtain m where 
   3.875 -	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   3.876 -      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
   3.877 -      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
   3.878 -      then have wm1: "w^k * a = - 1" by simp
   3.879 -      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)" 
   3.880 -	using norm_ge_zero[of w] w0 m(1)
   3.881 -	  by (simp add: inverse_eq_divide zero_less_mult_iff)
   3.882 -      with real_down2[OF zero_less_one] obtain t where
   3.883 -	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
   3.884 -      let ?ct = "complex_of_real t"
   3.885 -      let ?w = "?ct * w"
   3.886 -      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)
   3.887 -      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
   3.888 -	unfolding wm1 by (simp)
   3.889 -      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)" 
   3.890 -	apply -
   3.891 -	apply (rule cong[OF refl[of cmod]])
   3.892 -	apply assumption
   3.893 -	done
   3.894 -      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"] 
   3.895 -      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 
   3.896 -      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
   3.897 -      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
   3.898 -      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult) 
   3.899 -      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
   3.900 -	by (simp add: inverse_eq_divide field_simps)
   3.901 -      with zero_less_power[OF t(1), of k] 
   3.902 -      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" 
   3.903 -	apply - apply (rule mult_strict_left_mono) by simp_all
   3.904 -      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
   3.905 -	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
   3.906 -      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   3.907 -	using t(1,2) m(2)[rule_format, OF tw] w0
   3.908 -	apply (simp only: )
   3.909 -	apply auto
   3.910 -	apply (rule mult_mono, simp_all add: norm_ge_zero)+
   3.911 -	apply (simp add: zero_le_mult_iff zero_le_power)
   3.912 -	done
   3.913 -      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp 
   3.914 -      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1" 
   3.915 -	by auto
   3.916 -      from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
   3.917 -      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" . 
   3.918 -      from th11 th12
   3.919 -      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith 
   3.920 -      then have "cmod (poly ?r ?w) < 1" 
   3.921 -	unfolding kas(4)[rule_format, of ?w] r01 by simp 
   3.922 -      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
   3.923 -    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
   3.924 -    from cr0_contr cq0 q(2)
   3.925 -    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
   3.926 -  ultimately show ?ths by blast
   3.927 -qed
   3.928 -
   3.929 -text {* Alternative version with a syntactic notion of constant polynomial. *}
   3.930 -
   3.931 -lemma fundamental_theorem_of_algebra_alt:
   3.932 -  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
   3.933 -  shows "\<exists>z. poly p z = (0::complex)"
   3.934 -using nc
   3.935 -proof(induct p)
   3.936 -  case (pCons c cs)
   3.937 -  {assume "c=0" hence ?case by auto}
   3.938 -  moreover
   3.939 -  {assume c0: "c\<noteq>0"
   3.940 -    {assume nc: "constant (poly (pCons c cs))"
   3.941 -      from nc[unfolded constant_def, rule_format, of 0] 
   3.942 -      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto 
   3.943 -      hence "cs = 0"
   3.944 -	proof(induct cs)
   3.945 -	  case (pCons d ds)
   3.946 -	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
   3.947 -	  moreover
   3.948 -	  {assume d0: "d\<noteq>0"
   3.949 -	    from poly_bound_exists[of 1 ds] obtain m where 
   3.950 -	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   3.951 -	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
   3.952 -	    from real_down2[OF dm zero_less_one] obtain x where 
   3.953 -	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
   3.954 -	    let ?x = "complex_of_real x"
   3.955 -	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
   3.956 -	    from pCons.prems[rule_format, OF cx(1)]
   3.957 -	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
   3.958 -	    from m(2)[rule_format, OF cx(2)] x(1)
   3.959 -	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
   3.960 -	      by (simp add: norm_mult)
   3.961 -	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
   3.962 -	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
   3.963 -	    with cth  have ?case by blast}
   3.964 -	  ultimately show ?case by blast 
   3.965 -	qed simp}
   3.966 -      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0 
   3.967 -	by blast
   3.968 -      from fundamental_theorem_of_algebra[OF nc] have ?case .}
   3.969 -  ultimately show ?case by blast  
   3.970 -qed simp
   3.971 -
   3.972 -subsection {* Order of polynomial roots *}
   3.973 -
   3.974 -definition
   3.975 -  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
   3.976 -where
   3.977 -  [code del]:
   3.978 -  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
   3.979 -
   3.980 -lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
   3.981 -by (induct n, simp, auto intro: order_trans degree_mult_le)
   3.982 -
   3.983 -lemma coeff_linear_power:
   3.984 -  fixes a :: "'a::{comm_semiring_1,recpower}"
   3.985 -  shows "coeff ([:a, 1:] ^ n) n = 1"
   3.986 -apply (induct n, simp_all)
   3.987 -apply (subst coeff_eq_0)
   3.988 -apply (auto intro: le_less_trans degree_power_le)
   3.989 -done
   3.990 -
   3.991 -lemma degree_linear_power:
   3.992 -  fixes a :: "'a::{comm_semiring_1,recpower}"
   3.993 -  shows "degree ([:a, 1:] ^ n) = n"
   3.994 -apply (rule order_antisym)
   3.995 -apply (rule ord_le_eq_trans [OF degree_power_le], simp)
   3.996 -apply (rule le_degree, simp add: coeff_linear_power)
   3.997 -done
   3.998 -
   3.999 -lemma order_1: "[:-a, 1:] ^ order a p dvd p"
  3.1000 -apply (cases "p = 0", simp)
  3.1001 -apply (cases "order a p", simp)
  3.1002 -apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
  3.1003 -apply (drule not_less_Least, simp)
  3.1004 -apply (fold order_def, simp)
  3.1005 -done
  3.1006 -
  3.1007 -lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  3.1008 -unfolding order_def
  3.1009 -apply (rule LeastI_ex)
  3.1010 -apply (rule_tac x="degree p" in exI)
  3.1011 -apply (rule notI)
  3.1012 -apply (drule (1) dvd_imp_degree_le)
  3.1013 -apply (simp only: degree_linear_power)
  3.1014 -done
  3.1015 -
  3.1016 -lemma order:
  3.1017 -  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
  3.1018 -by (rule conjI [OF order_1 order_2])
  3.1019 -
  3.1020 -lemma order_degree:
  3.1021 -  assumes p: "p \<noteq> 0"
  3.1022 -  shows "order a p \<le> degree p"
  3.1023 -proof -
  3.1024 -  have "order a p = degree ([:-a, 1:] ^ order a p)"
  3.1025 -    by (simp only: degree_linear_power)
  3.1026 -  also have "\<dots> \<le> degree p"
  3.1027 -    using order_1 p by (rule dvd_imp_degree_le)
  3.1028 -  finally show ?thesis .
  3.1029 -qed
  3.1030 -
  3.1031 -lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  3.1032 -apply (cases "p = 0", simp_all)
  3.1033 -apply (rule iffI)
  3.1034 -apply (rule ccontr, simp)
  3.1035 -apply (frule order_2 [where a=a], simp)
  3.1036 -apply (simp add: poly_eq_0_iff_dvd)
  3.1037 -apply (simp add: poly_eq_0_iff_dvd)
  3.1038 -apply (simp only: order_def)
  3.1039 -apply (drule not_less_Least, simp)
  3.1040 -done
  3.1041 -
  3.1042 -lemma UNIV_nat_infinite:
  3.1043 -  "\<not> finite (UNIV :: nat set)" (is "\<not> finite ?U")
  3.1044 -proof
  3.1045 -  assume "finite ?U"
  3.1046 -  moreover have "Suc (Max ?U) \<in> ?U" ..
  3.1047 -  ultimately have "Suc (Max ?U) \<le> Max ?U" by (rule Max_ge)
  3.1048 -  then show "False" by simp
  3.1049 -qed
  3.1050 -
  3.1051 -lemma UNIV_char_0_infinite:
  3.1052 -  "\<not> finite (UNIV::'a::semiring_char_0 set)"
  3.1053 -proof
  3.1054 -  assume "finite (UNIV::'a set)"
  3.1055 -  with subset_UNIV have "finite (range of_nat::'a set)"
  3.1056 -    by (rule finite_subset)
  3.1057 -  moreover have "inj (of_nat::nat \<Rightarrow> 'a)"
  3.1058 -    by (simp add: inj_on_def)
  3.1059 -  ultimately have "finite (UNIV::nat set)"
  3.1060 -    by (rule finite_imageD)
  3.1061 -  then show "False"
  3.1062 -    by (simp add: UNIV_nat_infinite)
  3.1063 -qed
  3.1064 -
  3.1065 -lemma poly_zero:
  3.1066 -  fixes p :: "'a::{idom,ring_char_0} poly"
  3.1067 -  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
  3.1068 -apply (cases "p = 0", simp_all)
  3.1069 -apply (drule poly_roots_finite)
  3.1070 -apply (auto simp add: UNIV_char_0_infinite)
  3.1071 -done
  3.1072 -
  3.1073 -lemma poly_eq_iff:
  3.1074 -  fixes p q :: "'a::{idom,ring_char_0} poly"
  3.1075 -  shows "poly p = poly q \<longleftrightarrow> p = q"
  3.1076 -  using poly_zero [of "p - q"]
  3.1077 -  by (simp add: expand_fun_eq)
  3.1078 -
  3.1079 -
  3.1080 -subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
  3.1081 -
  3.1082 -lemma nullstellensatz_lemma:
  3.1083 -  fixes p :: "complex poly"
  3.1084 -  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
  3.1085 -  and "degree p = n" and "n \<noteq> 0"
  3.1086 -  shows "p dvd (q ^ n)"
  3.1087 -using prems
  3.1088 -proof(induct n arbitrary: p q rule: nat_less_induct)
  3.1089 -  fix n::nat fix p q :: "complex poly"
  3.1090 -  assume IH: "\<forall>m<n. \<forall>p q.
  3.1091 -                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
  3.1092 -                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
  3.1093 -    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0" 
  3.1094 -    and dpn: "degree p = n" and n0: "n \<noteq> 0"
  3.1095 -  from dpn n0 have pne: "p \<noteq> 0" by auto
  3.1096 -  let ?ths = "p dvd (q ^ n)"
  3.1097 -  {fix a assume a: "poly p a = 0"
  3.1098 -    {assume oa: "order a p \<noteq> 0"
  3.1099 -      let ?op = "order a p"
  3.1100 -      from pne have ap: "([:- a, 1:] ^ ?op) dvd p" 
  3.1101 -	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+ 
  3.1102 -      note oop = order_degree[OF pne, unfolded dpn]
  3.1103 -      {assume q0: "q = 0"
  3.1104 -	hence ?ths using n0
  3.1105 -          by (simp add: power_0_left)}
  3.1106 -      moreover
  3.1107 -      {assume q0: "q \<noteq> 0"
  3.1108 -	from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
  3.1109 -	obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
  3.1110 -	from ap(1) obtain s where
  3.1111 -	  s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
  3.1112 -	have sne: "s \<noteq> 0"
  3.1113 -	  using s pne by auto
  3.1114 -	{assume ds0: "degree s = 0"
  3.1115 -	  from ds0 have "\<exists>k. s = [:k:]"
  3.1116 -            by (cases s, simp split: if_splits)
  3.1117 -	  then obtain k where kpn: "s = [:k:]" by blast
  3.1118 -          from sne kpn have k: "k \<noteq> 0" by simp
  3.1119 -	  let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
  3.1120 -          from k oop [of a] have "q ^ n = p * ?w"
  3.1121 -            apply -
  3.1122 -            apply (subst r, subst s, subst kpn)
  3.1123 -            apply (subst power_mult_distrib, simp)
  3.1124 -            apply (subst power_add [symmetric], simp)
  3.1125 -            done
  3.1126 -	  hence ?ths unfolding dvd_def by blast}
  3.1127 -	moreover
  3.1128 -	{assume ds0: "degree s \<noteq> 0"
  3.1129 -	  from ds0 sne dpn s oa
  3.1130 -	    have dsn: "degree s < n" apply auto
  3.1131 -              apply (erule ssubst)
  3.1132 -              apply (simp add: degree_mult_eq degree_linear_power)
  3.1133 -              done
  3.1134 -	    {fix x assume h: "poly s x = 0"
  3.1135 -	      {assume xa: "x = a"
  3.1136 -		from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
  3.1137 -		  u: "s = [:- a, 1:] * u" by (rule dvdE)
  3.1138 -		have "p = [:- a, 1:] ^ (Suc ?op) * u"
  3.1139 -                  by (subst s, subst u, simp only: power_Suc mult_ac)
  3.1140 -		with ap(2)[unfolded dvd_def] have False by blast}
  3.1141 -	      note xa = this
  3.1142 -	      from h have "poly p x = 0" by (subst s, simp)
  3.1143 -	      with pq0 have "poly q x = 0" by blast
  3.1144 -	      with r xa have "poly r x = 0"
  3.1145 -                by (auto simp add: uminus_add_conv_diff)}
  3.1146 -	    note impth = this
  3.1147 -	    from IH[rule_format, OF dsn, of s r] impth ds0
  3.1148 -	    have "s dvd (r ^ (degree s))" by blast
  3.1149 -	    then obtain u where u: "r ^ (degree s) = s * u" ..
  3.1150 -	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
  3.1151 -              by (simp only: poly_mult[symmetric] poly_power[symmetric])
  3.1152 -	    let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
  3.1153 -	    from oop[of a] dsn have "q ^ n = p * ?w"
  3.1154 -              apply -
  3.1155 -              apply (subst s, subst r)
  3.1156 -              apply (simp only: power_mult_distrib)
  3.1157 -              apply (subst mult_assoc [where b=s])
  3.1158 -              apply (subst mult_assoc [where a=u])
  3.1159 -              apply (subst mult_assoc [where b=u, symmetric])
  3.1160 -              apply (subst u [symmetric])
  3.1161 -              apply (simp add: mult_ac power_add [symmetric])
  3.1162 -              done
  3.1163 -	    hence ?ths unfolding dvd_def by blast}
  3.1164 -      ultimately have ?ths by blast }
  3.1165 -      ultimately have ?ths by blast}
  3.1166 -    then have ?ths using a order_root pne by blast}
  3.1167 -  moreover
  3.1168 -  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
  3.1169 -    from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
  3.1170 -      ccs: "c\<noteq>0" "p = pCons c 0" by blast
  3.1171 -    
  3.1172 -    then have pp: "\<And>x. poly p x =  c" by simp
  3.1173 -    let ?w = "[:1/c:] * (q ^ n)"
  3.1174 -    from ccs
  3.1175 -    have "(q ^ n) = (p * ?w) "
  3.1176 -      by (simp add: smult_smult)
  3.1177 -    hence ?ths unfolding dvd_def by blast}
  3.1178 -  ultimately show ?ths by blast
  3.1179 -qed
  3.1180 -
  3.1181 -lemma nullstellensatz_univariate:
  3.1182 -  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> 
  3.1183 -    p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
  3.1184 -proof-
  3.1185 -  {assume pe: "p = 0"
  3.1186 -    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
  3.1187 -      apply auto
  3.1188 -      apply (rule poly_zero [THEN iffD1])
  3.1189 -      by (rule ext, simp)
  3.1190 -    {assume "p dvd (q ^ (degree p))"
  3.1191 -      then obtain r where r: "q ^ (degree p) = p * r" ..
  3.1192 -      from r pe have False by simp}
  3.1193 -    with eq pe have ?thesis by blast}
  3.1194 -  moreover
  3.1195 -  {assume pe: "p \<noteq> 0"
  3.1196 -    {assume dp: "degree p = 0"
  3.1197 -      then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
  3.1198 -        by (cases p, simp split: if_splits)
  3.1199 -      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
  3.1200 -      from k dp have "q ^ (degree p) = p * [:1/k:]"
  3.1201 -        by (simp add: one_poly_def)
  3.1202 -      hence th2: "p dvd (q ^ (degree p))" ..
  3.1203 -      from th1 th2 pe have ?thesis by blast}
  3.1204 -    moreover
  3.1205 -    {assume dp: "degree p \<noteq> 0"
  3.1206 -      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
  3.1207 -      {assume "p dvd (q ^ (Suc n))"
  3.1208 -	then obtain u where u: "q ^ (Suc n) = p * u" ..
  3.1209 -	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
  3.1210 -	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
  3.1211 -	  hence False using u h(1) by (simp only: poly_mult) simp}}
  3.1212 -	with n nullstellensatz_lemma[of p q "degree p"] dp 
  3.1213 -	have ?thesis by auto}
  3.1214 -    ultimately have ?thesis by blast}
  3.1215 -  ultimately show ?thesis by blast
  3.1216 -qed
  3.1217 -
  3.1218 -text{* Useful lemma *}
  3.1219 -
  3.1220 -lemma constant_degree:
  3.1221 -  fixes p :: "'a::{idom,ring_char_0} poly"
  3.1222 -  shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
  3.1223 -proof
  3.1224 -  assume l: ?lhs
  3.1225 -  from l[unfolded constant_def, rule_format, of _ "0"]
  3.1226 -  have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
  3.1227 -  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
  3.1228 -  then have "degree p = degree [:poly p 0:]" by simp
  3.1229 -  then show ?rhs by simp
  3.1230 -next
  3.1231 -  assume r: ?rhs
  3.1232 -  then obtain k where "p = [:k:]"
  3.1233 -    by (cases p, simp split: if_splits)
  3.1234 -  then show ?lhs unfolding constant_def by auto
  3.1235 -qed
  3.1236 -
  3.1237 -lemma divides_degree: assumes pq: "p dvd (q:: complex poly)"
  3.1238 -  shows "degree p \<le> degree q \<or> q = 0"
  3.1239 -apply (cases "q = 0", simp_all)
  3.1240 -apply (erule dvd_imp_degree_le [OF pq])
  3.1241 -done
  3.1242 -
  3.1243 -(* Arithmetic operations on multivariate polynomials.                        *)
  3.1244 -
  3.1245 -lemma mpoly_base_conv: 
  3.1246 -  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
  3.1247 -
  3.1248 -lemma mpoly_norm_conv: 
  3.1249 -  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
  3.1250 -
  3.1251 -lemma mpoly_sub_conv: 
  3.1252 -  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
  3.1253 -  by (simp add: diff_def)
  3.1254 -
  3.1255 -lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
  3.1256 -
  3.1257 -lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
  3.1258 -
  3.1259 -lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
  3.1260 -lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
  3.1261 -  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast 
  3.1262 -
  3.1263 -lemma poly_divides_pad_rule: 
  3.1264 -  fixes p q :: "complex poly"
  3.1265 -  assumes pq: "p dvd q"
  3.1266 -  shows "p dvd (pCons (0::complex) q)"
  3.1267 -proof-
  3.1268 -  have "pCons 0 q = q * [:0,1:]" by simp
  3.1269 -  then have "q dvd (pCons 0 q)" ..
  3.1270 -  with pq show ?thesis by (rule dvd_trans)
  3.1271 -qed
  3.1272 -
  3.1273 -lemma poly_divides_pad_const_rule: 
  3.1274 -  fixes p q :: "complex poly"
  3.1275 -  assumes pq: "p dvd q"
  3.1276 -  shows "p dvd (smult a q)"
  3.1277 -proof-
  3.1278 -  have "smult a q = q * [:a:]" by simp
  3.1279 -  then have "q dvd smult a q" ..
  3.1280 -  with pq show ?thesis by (rule dvd_trans)
  3.1281 -qed
  3.1282 -
  3.1283 -
  3.1284 -lemma poly_divides_conv0:  
  3.1285 -  fixes p :: "complex poly"
  3.1286 -  assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
  3.1287 -  shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
  3.1288 -proof-
  3.1289 -  {assume r: ?rhs 
  3.1290 -    hence "q = p * 0" by simp
  3.1291 -    hence ?lhs ..}
  3.1292 -  moreover
  3.1293 -  {assume l: ?lhs
  3.1294 -    {assume q0: "q = 0"
  3.1295 -      hence ?rhs by simp}
  3.1296 -    moreover
  3.1297 -    {assume q0: "q \<noteq> 0"
  3.1298 -      from l q0 have "degree p \<le> degree q"
  3.1299 -        by (rule dvd_imp_degree_le)
  3.1300 -      with lgpq have ?rhs by simp }
  3.1301 -    ultimately have ?rhs by blast }
  3.1302 -  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast) 
  3.1303 -qed
  3.1304 -
  3.1305 -lemma poly_divides_conv1: 
  3.1306 -  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
  3.1307 -  and qrp': "smult a q - p' \<equiv> r"
  3.1308 -  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
  3.1309 -proof-
  3.1310 -  {
  3.1311 -  from pp' obtain t where t: "p' = p * t" ..
  3.1312 -  {assume l: ?lhs
  3.1313 -    then obtain u where u: "q = p * u" ..
  3.1314 -     have "r = p * (smult a u - t)"
  3.1315 -       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
  3.1316 -     then have ?rhs ..}
  3.1317 -  moreover
  3.1318 -  {assume r: ?rhs
  3.1319 -    then obtain u where u: "r = p * u" ..
  3.1320 -    from u [symmetric] t qrp' [symmetric] a0
  3.1321 -    have "q = p * smult (1/a) (u + t)"
  3.1322 -      by (simp add: algebra_simps mult_smult_right smult_smult)
  3.1323 -    hence ?lhs ..}
  3.1324 -  ultimately have "?lhs = ?rhs" by blast }
  3.1325 -thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast) 
  3.1326 -qed
  3.1327 -
  3.1328 -lemma basic_cqe_conv1:
  3.1329 -  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<equiv> False"
  3.1330 -  "(\<exists>x. poly 0 x \<noteq> 0) \<equiv> False"
  3.1331 -  "(\<exists>x. poly [:c:] x \<noteq> 0) \<equiv> c\<noteq>0"
  3.1332 -  "(\<exists>x. poly 0 x = 0) \<equiv> True"
  3.1333 -  "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
  3.1334 -
  3.1335 -lemma basic_cqe_conv2: 
  3.1336 -  assumes l:"p \<noteq> 0" 
  3.1337 -  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
  3.1338 -proof-
  3.1339 -  {fix h t
  3.1340 -    assume h: "h\<noteq>0" "t=0"  "pCons a (pCons b p) = pCons h t"
  3.1341 -    with l have False by simp}
  3.1342 -  hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
  3.1343 -    by blast
  3.1344 -  from fundamental_theorem_of_algebra_alt[OF th] 
  3.1345 -  show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
  3.1346 -qed
  3.1347 -
  3.1348 -lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
  3.1349 -proof-
  3.1350 -  have "p = 0 \<longleftrightarrow> poly p = poly 0"
  3.1351 -    by (simp add: poly_zero)
  3.1352 -  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
  3.1353 -  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
  3.1354 -    by - (atomize (full), blast)
  3.1355 -qed
  3.1356 -
  3.1357 -lemma basic_cqe_conv3:
  3.1358 -  fixes p q :: "complex poly"
  3.1359 -  assumes l: "p \<noteq> 0" 
  3.1360 -  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
  3.1361 -proof-
  3.1362 -  from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
  3.1363 -  from nullstellensatz_univariate[of "pCons a p" q] l
  3.1364 -  show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
  3.1365 -    unfolding dp
  3.1366 -    by - (atomize (full), auto)
  3.1367 -qed
  3.1368 -
  3.1369 -lemma basic_cqe_conv4:
  3.1370 -  fixes p q :: "complex poly"
  3.1371 -  assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
  3.1372 -  shows "p dvd (q ^ n) \<equiv> p dvd r"
  3.1373 -proof-
  3.1374 -  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
  3.1375 -  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
  3.1376 -  thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
  3.1377 -qed
  3.1378 -
  3.1379 -lemma pmult_Cons_Cons: "(pCons (a::complex) (pCons b p) * q = (smult a q) + (pCons 0 (pCons b p * q)))"
  3.1380 -  by simp
  3.1381 -
  3.1382 -lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
  3.1383 -lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
  3.1384 -lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
  3.1385 -
  3.1386 -lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
  3.1387 -lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)" 
  3.1388 -  by (atomize (full)) simp_all
  3.1389 -lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
  3.1390 -lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
  3.1391 -proof
  3.1392 -  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
  3.1393 -next
  3.1394 -  assume "p \<and> q \<equiv> p \<and> r" "p"
  3.1395 -  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
  3.1396 -qed
  3.1397 -lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
  3.1398 -
  3.1399 -end
     4.1 --- a/src/HOL/IsaMakefile	Wed Feb 11 11:22:42 2009 -0800
     4.2 +++ b/src/HOL/IsaMakefile	Thu Feb 12 18:14:43 2009 +0100
     4.3 @@ -270,7 +270,6 @@
     4.4  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
     4.5    Complex_Main.thy \
     4.6    Complex.thy \
     4.7 -  Fundamental_Theorem_Algebra.thy \
     4.8    Deriv.thy \
     4.9    Fact.thy \
    4.10    FrechetDeriv.thy \
    4.11 @@ -317,6 +316,7 @@
    4.12    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    4.13    Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
    4.14    Library/Finite_Cartesian_Product.thy \
    4.15 +  Library/Fundamental_Theorem_Algebra.thy \
    4.16    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    4.17    Library/Multiset.thy Library/Permutation.thy	\
    4.18    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu Feb 12 18:14:43 2009 +0100
     5.3 @@ -0,0 +1,1353 @@
     5.4 +(* Author: Amine Chaieb, TU Muenchen *)
     5.5 +
     5.6 +header{*Fundamental Theorem of Algebra*}
     5.7 +
     5.8 +theory Fundamental_Theorem_Algebra
     5.9 +imports Polynomial Complex
    5.10 +begin
    5.11 +
    5.12 +subsection {* Square root of complex numbers *}
    5.13 +definition csqrt :: "complex \<Rightarrow> complex" where
    5.14 +"csqrt z = (if Im z = 0 then
    5.15 +            if 0 \<le> Re z then Complex (sqrt(Re z)) 0
    5.16 +            else Complex 0 (sqrt(- Re z))
    5.17 +           else Complex (sqrt((cmod z + Re z) /2))
    5.18 +                        ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
    5.19 +
    5.20 +lemma csqrt[algebra]: "csqrt z ^ 2 = z"
    5.21 +proof-
    5.22 +  obtain x y where xy: "z = Complex x y" by (cases z)
    5.23 +  {assume y0: "y = 0"
    5.24 +    {assume x0: "x \<ge> 0" 
    5.25 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
    5.26 +	by (simp add: csqrt_def power2_eq_square)}
    5.27 +    moreover
    5.28 +    {assume "\<not> x \<ge> 0" hence x0: "- x \<ge> 0" by arith
    5.29 +      then have ?thesis using y0 xy real_sqrt_pow2[OF x0] 
    5.30 +	by (simp add: csqrt_def power2_eq_square) }
    5.31 +    ultimately have ?thesis by blast}
    5.32 +  moreover
    5.33 +  {assume y0: "y\<noteq>0"
    5.34 +    {fix x y
    5.35 +      let ?z = "Complex x y"
    5.36 +      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z" by auto
    5.37 +      hence "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0" by arith+ 
    5.38 +      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) }
    5.39 +    note th = this
    5.40 +    have sq4: "\<And>x::real. x^2 / 4 = (x / 2) ^ 2" 
    5.41 +      by (simp add: power2_eq_square) 
    5.42 +    from th[of x y]
    5.43 +    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
    5.44 +    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"
    5.45 +      unfolding power2_eq_square by simp 
    5.46 +    have "sqrt 4 = sqrt (2^2)" by simp 
    5.47 +    hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
    5.48 +    have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
    5.49 +      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
    5.50 +      unfolding power2_eq_square 
    5.51 +      by (simp add: algebra_simps real_sqrt_divide sqrt4)
    5.52 +     from y0 xy have ?thesis  apply (simp add: csqrt_def power2_eq_square)
    5.53 +       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])
    5.54 +      using th1 th2  ..}
    5.55 +  ultimately show ?thesis by blast
    5.56 +qed
    5.57 +
    5.58 +
    5.59 +subsection{* More lemmas about module of complex numbers *}
    5.60 +
    5.61 +lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
    5.62 +  by (rule of_real_power [symmetric])
    5.63 +
    5.64 +lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
    5.65 +  apply (rule exI[where x = "min d1 d2 / 2"])
    5.66 +  by (simp add: field_simps min_def)
    5.67 +
    5.68 +text{* The triangle inequality for cmod *}
    5.69 +lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
    5.70 +  using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
    5.71 +
    5.72 +subsection{* Basic lemmas about complex polynomials *}
    5.73 +
    5.74 +lemma poly_bound_exists:
    5.75 +  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
    5.76 +proof(induct p)
    5.77 +  case 0 thus ?case by (rule exI[where x=1], simp) 
    5.78 +next
    5.79 +  case (pCons c cs)
    5.80 +  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
    5.81 +    by blast
    5.82 +  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
    5.83 +  have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
    5.84 +  {fix z
    5.85 +    assume H: "cmod z \<le> r"
    5.86 +    from m H have th: "cmod (poly cs z) \<le> m" by blast
    5.87 +    from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
    5.88 +    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
    5.89 +      using norm_triangle_ineq[of c "z* poly cs z"] by simp
    5.90 +    also have "\<dots> \<le> cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
    5.91 +    also have "\<dots> \<le> ?k" by simp
    5.92 +    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
    5.93 +  with kp show ?case by blast
    5.94 +qed
    5.95 +
    5.96 +
    5.97 +text{* Offsetting the variable in a polynomial gives another of same degree *}
    5.98 +
    5.99 +definition
   5.100 +  "offset_poly p h = poly_rec 0 (\<lambda>a p q. smult h q + pCons a q) p"
   5.101 +
   5.102 +lemma offset_poly_0: "offset_poly 0 h = 0"
   5.103 +  unfolding offset_poly_def by (simp add: poly_rec_0)
   5.104 +
   5.105 +lemma offset_poly_pCons:
   5.106 +  "offset_poly (pCons a p) h =
   5.107 +    smult h (offset_poly p h) + pCons a (offset_poly p h)"
   5.108 +  unfolding offset_poly_def by (simp add: poly_rec_pCons)
   5.109 +
   5.110 +lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
   5.111 +by (simp add: offset_poly_pCons offset_poly_0)
   5.112 +
   5.113 +lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
   5.114 +apply (induct p)
   5.115 +apply (simp add: offset_poly_0)
   5.116 +apply (simp add: offset_poly_pCons algebra_simps)
   5.117 +done
   5.118 +
   5.119 +lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \<Longrightarrow> p = 0"
   5.120 +by (induct p arbitrary: a, simp, force)
   5.121 +
   5.122 +lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \<longleftrightarrow> p = 0"
   5.123 +apply (safe intro!: offset_poly_0)
   5.124 +apply (induct p, simp)
   5.125 +apply (simp add: offset_poly_pCons)
   5.126 +apply (frule offset_poly_eq_0_lemma, simp)
   5.127 +done
   5.128 +
   5.129 +lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
   5.130 +apply (induct p)
   5.131 +apply (simp add: offset_poly_0)
   5.132 +apply (case_tac "p = 0")
   5.133 +apply (simp add: offset_poly_0 offset_poly_pCons)
   5.134 +apply (simp add: offset_poly_pCons)
   5.135 +apply (subst degree_add_eq_right)
   5.136 +apply (rule le_less_trans [OF degree_smult_le])
   5.137 +apply (simp add: offset_poly_eq_0_iff)
   5.138 +apply (simp add: offset_poly_eq_0_iff)
   5.139 +done
   5.140 +
   5.141 +definition
   5.142 +  "psize p = (if p = 0 then 0 else Suc (degree p))"
   5.143 +
   5.144 +lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
   5.145 +  unfolding psize_def by simp
   5.146 +
   5.147 +lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
   5.148 +proof (intro exI conjI)
   5.149 +  show "psize (offset_poly p a) = psize p"
   5.150 +    unfolding psize_def
   5.151 +    by (simp add: offset_poly_eq_0_iff degree_offset_poly)
   5.152 +  show "\<forall>x. poly (offset_poly p a) x = poly p (a + x)"
   5.153 +    by (simp add: poly_offset_poly)
   5.154 +qed
   5.155 +
   5.156 +text{* An alternative useful formulation of completeness of the reals *}
   5.157 +lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
   5.158 +  shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
   5.159 +proof-
   5.160 +  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
   5.161 +  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
   5.162 +  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y" 
   5.163 +    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
   5.164 +  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
   5.165 +    by blast
   5.166 +  from Y[OF x] have xY: "x < Y" .
   5.167 +  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)  
   5.168 +  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y" 
   5.169 +    apply (clarsimp, atomize (full)) by auto 
   5.170 +  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
   5.171 +  {fix y
   5.172 +    {fix z assume z: "P z" "y < z"
   5.173 +      from L' z have "y < L" by auto }
   5.174 +    moreover
   5.175 +    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
   5.176 +      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
   5.177 +      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def) 
   5.178 +      with yL(1) have False  by arith}
   5.179 +    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
   5.180 +  thus ?thesis by blast
   5.181 +qed
   5.182 +
   5.183 +
   5.184 +subsection{* Some theorems about Sequences*}
   5.185 +text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
   5.186 +
   5.187 +lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   5.188 +  unfolding Ex1_def
   5.189 +  apply (rule_tac x="nat_rec e f" in exI)
   5.190 +  apply (rule conjI)+
   5.191 +apply (rule def_nat_rec_0, simp)
   5.192 +apply (rule allI, rule def_nat_rec_Suc, simp)
   5.193 +apply (rule allI, rule impI, rule ext)
   5.194 +apply (erule conjE)
   5.195 +apply (induct_tac x)
   5.196 +apply (simp add: nat_rec_0)
   5.197 +apply (erule_tac x="n" in allE)
   5.198 +apply (simp)
   5.199 +done
   5.200 +
   5.201 +text{* for any sequence, there is a mootonic subsequence *}
   5.202 +lemma seq_monosub: "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
   5.203 +proof-
   5.204 +  {assume H: "\<forall>n. \<exists>p >n. \<forall> m\<ge>p. s m \<le> s p"
   5.205 +    let ?P = "\<lambda> p n. p > n \<and> (\<forall>m \<ge> p. s m \<le> s p)"
   5.206 +    from num_Axiom[of "SOME p. ?P p 0" "\<lambda>p n. SOME p. ?P p n"]
   5.207 +    obtain f where f: "f 0 = (SOME p. ?P p 0)" "\<forall>n. f (Suc n) = (SOME p. ?P p (f n))" by blast
   5.208 +    have "?P (f 0) 0"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p 0"]
   5.209 +      using H apply - 
   5.210 +      apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) 
   5.211 +      unfolding order_le_less by blast 
   5.212 +    hence f0: "f 0 > 0" "\<forall>m \<ge> f 0. s m \<le> s (f 0)" by blast+
   5.213 +    {fix n
   5.214 +      have "?P (f (Suc n)) (f n)" 
   5.215 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   5.216 +	using H apply - 
   5.217 +      apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) 
   5.218 +      unfolding order_le_less by blast 
   5.219 +    hence "f (Suc n) > f n" "\<forall>m \<ge> f (Suc n). s m \<le> s (f (Suc n))" by blast+}
   5.220 +  note fSuc = this
   5.221 +    {fix p q assume pq: "p \<ge> f q"
   5.222 +      have "s p \<le> s(f(q))"  using f0(2)[rule_format, of p] pq fSuc
   5.223 +	by (cases q, simp_all) }
   5.224 +    note pqth = this
   5.225 +    {fix q
   5.226 +      have "f (Suc q) > f q" apply (induct q) 
   5.227 +	using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))}
   5.228 +    note fss = this
   5.229 +    from fss have th1: "subseq f" unfolding subseq_Suc_iff ..
   5.230 +    {fix a b 
   5.231 +      have "f a \<le> f (a + b)"
   5.232 +      proof(induct b)
   5.233 +	case 0 thus ?case by simp
   5.234 +      next
   5.235 +	case (Suc b)
   5.236 +	from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp
   5.237 +      qed}
   5.238 +    note fmon0 = this
   5.239 +    have "monoseq (\<lambda>n. s (f n))" 
   5.240 +    proof-
   5.241 +      {fix n
   5.242 +	have "s (f n) \<ge> s (f (Suc n))" 
   5.243 +	proof(cases n)
   5.244 +	  case 0
   5.245 +	  assume n0: "n = 0"
   5.246 +	  from fSuc(1)[of 0] have th0: "f 0 \<le> f (Suc 0)" by simp
   5.247 +	  from f0(2)[rule_format, OF th0] show ?thesis  using n0 by simp
   5.248 +	next
   5.249 +	  case (Suc m)
   5.250 +	  assume m: "n = Suc m"
   5.251 +	  from fSuc(1)[of n] m have th0: "f (Suc m) \<le> f (Suc (Suc m))" by simp
   5.252 +	  from m fSuc(2)[rule_format, OF th0] show ?thesis by simp 
   5.253 +	qed}
   5.254 +      thus "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc by blast 
   5.255 +    qed
   5.256 +    with th1 have ?thesis by blast}
   5.257 +  moreover
   5.258 +  {fix N assume N: "\<forall>p >N. \<exists> m\<ge>p. s m > s p"
   5.259 +    {fix p assume p: "p \<ge> Suc N" 
   5.260 +      hence pN: "p > N" by arith with N obtain m where m: "m \<ge> p" "s m > s p" by blast
   5.261 +      have "m \<noteq> p" using m(2) by auto 
   5.262 +      with m have "\<exists>m>p. s p < s m" by - (rule exI[where x=m], auto)}
   5.263 +    note th0 = this
   5.264 +    let ?P = "\<lambda>m x. m > x \<and> s x < s m"
   5.265 +    from num_Axiom[of "SOME x. ?P x (Suc N)" "\<lambda>m x. SOME y. ?P y x"]
   5.266 +    obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" 
   5.267 +      "\<forall>n. f (Suc n) = (SOME m. ?P m (f n))" by blast
   5.268 +    have "?P (f 0) (Suc N)"  unfolding f(1) some_eq_ex[of "\<lambda>p. ?P p (Suc N)"]
   5.269 +      using N apply - 
   5.270 +      apply (erule allE[where x="Suc N"], clarsimp)
   5.271 +      apply (rule_tac x="m" in exI)
   5.272 +      apply auto
   5.273 +      apply (subgoal_tac "Suc N \<noteq> m")
   5.274 +      apply simp
   5.275 +      apply (rule ccontr, simp)
   5.276 +      done
   5.277 +    hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+
   5.278 +    {fix n
   5.279 +      have "f n > N \<and> ?P (f (Suc n)) (f n)"
   5.280 +	unfolding f(2)[rule_format, of n] some_eq_ex[of "\<lambda>p. ?P p (f n)"]
   5.281 +      proof (induct n)
   5.282 +	case 0 thus ?case
   5.283 +	  using f0 N apply auto 
   5.284 +	  apply (erule allE[where x="f 0"], clarsimp) 
   5.285 +	  apply (rule_tac x="m" in exI, simp)
   5.286 +	  by (subgoal_tac "f 0 \<noteq> m", auto)
   5.287 +      next
   5.288 +	case (Suc n)
   5.289 +	from Suc.hyps have Nfn: "N < f n" by blast
   5.290 +	from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast
   5.291 +	with Nfn have mN: "m > N" by arith
   5.292 +	note key = Suc.hyps[unfolded some_eq_ex[of "\<lambda>p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]]
   5.293 +	
   5.294 +	from key have th0: "f (Suc n) > N" by simp
   5.295 +	from N[rule_format, OF th0]
   5.296 +	obtain m' where m': "m' \<ge> f (Suc n)" "s (f (Suc n)) < s m'" by blast
   5.297 +	have "m' \<noteq> f (Suc (n))" apply (rule ccontr) using m'(2) by auto
   5.298 +	hence "m' > f (Suc n)" using m'(1) by simp
   5.299 +	with key m'(2) show ?case by auto
   5.300 +      qed}
   5.301 +    note fSuc = this
   5.302 +    {fix n
   5.303 +      have "f n \<ge> Suc N \<and> f(Suc n) > f n \<and> s(f n) < s(f(Suc n))" using fSuc[of n] by auto 
   5.304 +      hence "f n \<ge> Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+}
   5.305 +    note thf = this
   5.306 +    have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp
   5.307 +    have "monoseq (\<lambda>n. s (f n))"  unfolding monoseq_Suc using thf
   5.308 +      apply -
   5.309 +      apply (rule disjI1)
   5.310 +      apply auto
   5.311 +      apply (rule order_less_imp_le)
   5.312 +      apply blast
   5.313 +      done
   5.314 +    then have ?thesis  using sqf by blast}
   5.315 +  ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast
   5.316 +qed
   5.317 +
   5.318 +lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
   5.319 +proof(induct n)
   5.320 +  case 0 thus ?case by simp
   5.321 +next
   5.322 +  case (Suc n)
   5.323 +  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
   5.324 +  have "n < f (Suc n)" by arith 
   5.325 +  thus ?case by arith
   5.326 +qed
   5.327 +
   5.328 +subsection {* Fundamental theorem of algebra *}
   5.329 +lemma  unimodular_reduce_norm:
   5.330 +  assumes md: "cmod z = 1"
   5.331 +  shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
   5.332 +proof-
   5.333 +  obtain x y where z: "z = Complex x y " by (cases z, auto)
   5.334 +  from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
   5.335 +  {assume C: "cmod (z + 1) \<ge> 1" "cmod (z - 1) \<ge> 1" "cmod (z + ii) \<ge> 1" "cmod (z - ii) \<ge> 1"
   5.336 +    from C z xy have "2*x \<le> 1" "2*x \<ge> -1" "2*y \<le> 1" "2*y \<ge> -1"
   5.337 +      by (simp_all add: cmod_def power2_eq_square algebra_simps)
   5.338 +    hence "abs (2*x) \<le> 1" "abs (2*y) \<le> 1" by simp_all
   5.339 +    hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
   5.340 +      by - (rule power_mono, simp, simp)+
   5.341 +    hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1" 
   5.342 +      by (simp_all  add: power2_abs power_mult_distrib)
   5.343 +    from add_mono[OF th0] xy have False by simp }
   5.344 +  thus ?thesis unfolding linorder_not_le[symmetric] by blast
   5.345 +qed
   5.346 +
   5.347 +text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
   5.348 +lemma reduce_poly_simple:
   5.349 + assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
   5.350 +  shows "\<exists>z. cmod (1 + b * z^n) < 1"
   5.351 +using n
   5.352 +proof(induct n rule: nat_less_induct)
   5.353 +  fix n
   5.354 +  assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)" and n: "n \<noteq> 0"
   5.355 +  let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
   5.356 +  {assume e: "even n"
   5.357 +    hence "\<exists>m. n = 2*m" by presburger
   5.358 +    then obtain m where m: "n = 2*m" by blast
   5.359 +    from n m have "m\<noteq>0" "m < n" by presburger+
   5.360 +    with IH[rule_format, of m] obtain z where z: "?P z m" by blast
   5.361 +    from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
   5.362 +    hence "\<exists>z. ?P z n" ..}
   5.363 +  moreover
   5.364 +  {assume o: "odd n"
   5.365 +    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
   5.366 +    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
   5.367 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) = 
   5.368 +    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
   5.369 +    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2" 
   5.370 +      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
   5.371 +      by (simp add: power2_eq_square)
   5.372 +    finally 
   5.373 +    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
   5.374 +    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
   5.375 +    1" 
   5.376 +      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
   5.377 +      using right_inverse[OF b']
   5.378 +      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
   5.379 +    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   5.380 +      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
   5.381 +      by (simp add: real_sqrt_mult[symmetric] th0)        
   5.382 +    from o have "\<exists>m. n = Suc (2*m)" by presburger+
   5.383 +    then obtain m where m: "n = Suc (2*m)" by blast
   5.384 +    from unimodular_reduce_norm[OF th0] o
   5.385 +    have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
   5.386 +      apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
   5.387 +      apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
   5.388 +      apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
   5.389 +      apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
   5.390 +      apply (rule_tac x="- ii" in exI, simp add: m power_mult)
   5.391 +      apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
   5.392 +      apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
   5.393 +      done
   5.394 +    then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
   5.395 +    let ?w = "v / complex_of_real (root n (cmod b))"
   5.396 +    from odd_real_root_pow[OF o, of "cmod b"]
   5.397 +    have th1: "?w ^ n = v^n / complex_of_real (cmod b)" 
   5.398 +      by (simp add: power_divide complex_of_real_power)
   5.399 +    have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
   5.400 +    hence th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0" by simp
   5.401 +    have th4: "cmod (complex_of_real (cmod b) / b) *
   5.402 +   cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
   5.403 +   < cmod (complex_of_real (cmod b) / b) * 1"
   5.404 +      apply (simp only: norm_mult[symmetric] right_distrib)
   5.405 +      using b v by (simp add: th2)
   5.406 +
   5.407 +    from mult_less_imp_less_left[OF th4 th3]
   5.408 +    have "?P ?w n" unfolding th1 . 
   5.409 +    hence "\<exists>z. ?P z n" .. }
   5.410 +  ultimately show "\<exists>z. ?P z n" by blast
   5.411 +qed
   5.412 +
   5.413 +
   5.414 +text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
   5.415 +
   5.416 +lemma metric_bound_lemma: "cmod (x - y) <= \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
   5.417 +  using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
   5.418 +  unfolding cmod_def by simp
   5.419 +
   5.420 +lemma bolzano_weierstrass_complex_disc:
   5.421 +  assumes r: "\<forall>n. cmod (s n) \<le> r"
   5.422 +  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
   5.423 +proof-
   5.424 +  from seq_monosub[of "Re o s"] 
   5.425 +  obtain f g where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))" 
   5.426 +    unfolding o_def by blast
   5.427 +  from seq_monosub[of "Im o s o f"] 
   5.428 +  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s(f(g n))))" unfolding o_def by blast  
   5.429 +  let ?h = "f o g"
   5.430 +  from r[rule_format, of 0] have rp: "r \<ge> 0" using norm_ge_zero[of "s 0"] by arith 
   5.431 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Re (s n)\<bar>" 
   5.432 +  proof
   5.433 +    fix n
   5.434 +    from abs_Re_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Re (s n)\<bar> \<le> r + 1" by arith
   5.435 +  qed
   5.436 +  have conv1: "convergent (\<lambda>n. Re (s ( f n)))"
   5.437 +    apply (rule Bseq_monoseq_convergent)
   5.438 +    apply (simp add: Bseq_def)
   5.439 +    apply (rule exI[where x= "r + 1"])
   5.440 +    using th rp apply simp
   5.441 +    using f(2) .
   5.442 +  have th:"\<forall>n. r + 1 \<ge> \<bar> Im (s n)\<bar>" 
   5.443 +  proof
   5.444 +    fix n
   5.445 +    from abs_Im_le_cmod[of "s n"] r[rule_format, of n]  show "\<bar>Im (s n)\<bar> \<le> r + 1" by arith
   5.446 +  qed
   5.447 +
   5.448 +  have conv2: "convergent (\<lambda>n. Im (s (f (g n))))"
   5.449 +    apply (rule Bseq_monoseq_convergent)
   5.450 +    apply (simp add: Bseq_def)
   5.451 +    apply (rule exI[where x= "r + 1"])
   5.452 +    using th rp apply simp
   5.453 +    using g(2) .
   5.454 +
   5.455 +  from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x" 
   5.456 +    by blast 
   5.457 +  hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r" 
   5.458 +    unfolding LIMSEQ_def real_norm_def .
   5.459 +
   5.460 +  from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y" 
   5.461 +    by blast 
   5.462 +  hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r" 
   5.463 +    unfolding LIMSEQ_def real_norm_def .
   5.464 +  let ?w = "Complex x y"
   5.465 +  from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto 
   5.466 +  {fix e assume ep: "e > (0::real)"
   5.467 +    hence e2: "e/2 > 0" by simp
   5.468 +    from x[rule_format, OF e2] y[rule_format, OF e2]
   5.469 +    obtain N1 N2 where N1: "\<forall>n\<ge>N1. \<bar>Re (s (f n)) - x\<bar> < e / 2" and N2: "\<forall>n\<ge>N2. \<bar>Im (s (f (g n))) - y\<bar> < e / 2" by blast
   5.470 +    {fix n assume nN12: "n \<ge> N1 + N2"
   5.471 +      hence nN1: "g n \<ge> N1" and nN2: "n \<ge> N2" using seq_suble[OF g(1), of n] by arith+
   5.472 +      from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
   5.473 +      have "cmod (s (?h n) - ?w) < e" 
   5.474 +	using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
   5.475 +    hence "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" by blast }
   5.476 +  with hs show ?thesis  by blast  
   5.477 +qed
   5.478 +
   5.479 +text{* Polynomial is continuous. *}
   5.480 +
   5.481 +lemma poly_cont:
   5.482 +  assumes ep: "e > 0" 
   5.483 +  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
   5.484 +proof-
   5.485 +  obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
   5.486 +  proof
   5.487 +    show "degree (offset_poly p z) = degree p"
   5.488 +      by (rule degree_offset_poly)
   5.489 +    show "\<And>x. poly (offset_poly p z) x = poly p (z + x)"
   5.490 +      by (rule poly_offset_poly)
   5.491 +  qed
   5.492 +  {fix w
   5.493 +    note q(2)[of "w - z", simplified]}
   5.494 +  note th = this
   5.495 +  show ?thesis unfolding th[symmetric]
   5.496 +  proof(induct q)
   5.497 +    case 0 thus ?case  using ep by auto
   5.498 +  next
   5.499 +    case (pCons c cs)
   5.500 +    from poly_bound_exists[of 1 "cs"] 
   5.501 +    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
   5.502 +    from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
   5.503 +    have one0: "1 > (0::real)"  by arith
   5.504 +    from real_lbound_gt_zero[OF one0 em0] 
   5.505 +    obtain d where d: "d >0" "d < 1" "d < e / m" by blast
   5.506 +    from d(1,3) m(1) have dm: "d*m > 0" "d*m < e" 
   5.507 +      by (simp_all add: field_simps real_mult_order)
   5.508 +    show ?case 
   5.509 +      proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   5.510 +	fix d w
   5.511 +	assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
   5.512 +	hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
   5.513 +	from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
   5.514 +	from H have th: "cmod (w-z) \<le> d" by simp 
   5.515 +	from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
   5.516 +	show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
   5.517 +      qed  
   5.518 +    qed
   5.519 +qed
   5.520 +
   5.521 +text{* Hence a polynomial attains minimum on a closed disc 
   5.522 +  in the complex plane. *}
   5.523 +lemma  poly_minimum_modulus_disc:
   5.524 +  "\<exists>z. \<forall>w. cmod w \<le> r \<longrightarrow> cmod (poly p z) \<le> cmod (poly p w)"
   5.525 +proof-
   5.526 +  {assume "\<not> r \<ge> 0" hence ?thesis unfolding linorder_not_le
   5.527 +      apply -
   5.528 +      apply (rule exI[where x=0]) 
   5.529 +      apply auto
   5.530 +      apply (subgoal_tac "cmod w < 0")
   5.531 +      apply simp
   5.532 +      apply arith
   5.533 +      done }
   5.534 +  moreover
   5.535 +  {assume rp: "r \<ge> 0"
   5.536 +    from rp have "cmod 0 \<le> r \<and> cmod (poly p 0) = - (- cmod (poly p 0))" by simp 
   5.537 +    hence mth1: "\<exists>x z. cmod z \<le> r \<and> cmod (poly p z) = - x"  by blast
   5.538 +    {fix x z
   5.539 +      assume H: "cmod z \<le> r" "cmod (poly p z) = - x" "\<not>x < 1"
   5.540 +      hence "- x < 0 " by arith
   5.541 +      with H(2) norm_ge_zero[of "poly p z"]  have False by simp }
   5.542 +    then have mth2: "\<exists>z. \<forall>x. (\<exists>z. cmod z \<le> r \<and> cmod (poly p z) = - x) \<longrightarrow> x < z" by blast
   5.543 +    from real_sup_exists[OF mth1 mth2] obtain s where 
   5.544 +      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
   5.545 +    let ?m = "-s"
   5.546 +    {fix y
   5.547 +      from s[rule_format, of "-y"] have 
   5.548 +    "(\<exists>z x. cmod z \<le> r \<and> -(- cmod (poly p z)) < y) \<longleftrightarrow> ?m < y" 
   5.549 +	unfolding minus_less_iff[of y ] equation_minus_iff by blast }
   5.550 +    note s1 = this[unfolded minus_minus]
   5.551 +    from s1[of ?m] have s1m: "\<And>z x. cmod z \<le> r \<Longrightarrow> cmod (poly p z) \<ge> ?m" 
   5.552 +      by auto
   5.553 +    {fix n::nat
   5.554 +      from s1[rule_format, of "?m + 1/real (Suc n)"] 
   5.555 +      have "\<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)"
   5.556 +	by simp}
   5.557 +    hence th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
   5.558 +    from choice[OF th] obtain g where 
   5.559 +      g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m+1 /real(Suc n)" 
   5.560 +      by blast
   5.561 +    from bolzano_weierstrass_complex_disc[OF g(1)] 
   5.562 +    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   5.563 +      by blast    
   5.564 +    {fix w 
   5.565 +      assume wr: "cmod w \<le> r"
   5.566 +      let ?e = "\<bar>cmod (poly p z) - ?m\<bar>"
   5.567 +      {assume e: "?e > 0"
   5.568 +	hence e2: "?e/2 > 0" by simp
   5.569 +	from poly_cont[OF e2, of z p] obtain d where
   5.570 +	  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
   5.571 +	{fix w assume w: "cmod (w - z) < d"
   5.572 +	  have "cmod(poly p w - poly p z) < ?e / 2"
   5.573 +	    using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
   5.574 +	note th1 = this
   5.575 +	
   5.576 +	from fz(2)[rule_format, OF d(1)] obtain N1 where 
   5.577 +	  N1: "\<forall>n\<ge>N1. cmod (g (f n) - z) < d" by blast
   5.578 +	from reals_Archimedean2[of "2/?e"] obtain N2::nat where
   5.579 +	  N2: "2/?e < real N2" by blast
   5.580 +	have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
   5.581 +	  using N1[rule_format, of "N1 + N2"] th1 by simp
   5.582 +	{fix a b e2 m :: real
   5.583 +	have "a < e2 \<Longrightarrow> abs(b - m) < e2 \<Longrightarrow> 2 * e2 <= abs(b - m) + a
   5.584 +          ==> False" by arith}
   5.585 +      note th0 = this
   5.586 +      have ath: 
   5.587 +	"\<And>m x e. m <= x \<Longrightarrow>  x < m + e ==> abs(x - m::real) < e" by arith
   5.588 +      from s1m[OF g(1)[rule_format]]
   5.589 +      have th31: "?m \<le> cmod(poly p (g (f (N1 + N2))))" .
   5.590 +      from seq_suble[OF fz(1), of "N1+N2"]
   5.591 +      have th00: "real (Suc (N1+N2)) \<le> real (Suc (f (N1+N2)))" by simp
   5.592 +      have th000: "0 \<le> (1::real)" "(1::real) \<le> 1" "real (Suc (N1+N2)) > 0"  
   5.593 +	using N2 by auto
   5.594 +      from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \<le> ?m + 1 / real (Suc (N1 + N2))" by simp
   5.595 +      from g(2)[rule_format, of "f (N1 + N2)"]
   5.596 +      have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
   5.597 +      from order_less_le_trans[OF th01 th00]
   5.598 +      have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
   5.599 +      from N2 have "2/?e < real (Suc (N1 + N2))" by arith
   5.600 +      with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
   5.601 +      have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
   5.602 +      with ath[OF th31 th32]
   5.603 +      have thc1:"\<bar>cmod(poly p (g (f (N1 + N2)))) - ?m\<bar>< ?e/2" by arith  
   5.604 +      have ath2: "\<And>(a::real) b c m. \<bar>a - b\<bar> <= c ==> \<bar>b - m\<bar> <= \<bar>a - m\<bar> + c" 
   5.605 +	by arith
   5.606 +      have th22: "\<bar>cmod (poly p (g (f (N1 + N2)))) - cmod (poly p z)\<bar>
   5.607 +\<le> cmod (poly p (g (f (N1 + N2))) - poly p z)" 
   5.608 +	by (simp add: norm_triangle_ineq3)
   5.609 +      from ath2[OF th22, of ?m]
   5.610 +      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
   5.611 +      from th0[OF th2 thc1 thc2] have False .}
   5.612 +      hence "?e = 0" by auto
   5.613 +      then have "cmod (poly p z) = ?m" by simp  
   5.614 +      with s1m[OF wr]
   5.615 +      have "cmod (poly p z) \<le> cmod (poly p w)" by simp }
   5.616 +    hence ?thesis by blast}
   5.617 +  ultimately show ?thesis by blast
   5.618 +qed
   5.619 +
   5.620 +lemma "(rcis (sqrt (abs r)) (a/2)) ^ 2 = rcis (abs r) a"
   5.621 +  unfolding power2_eq_square
   5.622 +  apply (simp add: rcis_mult)
   5.623 +  apply (simp add: power2_eq_square[symmetric])
   5.624 +  done
   5.625 +
   5.626 +lemma cispi: "cis pi = -1" 
   5.627 +  unfolding cis_def
   5.628 +  by simp
   5.629 +
   5.630 +lemma "(rcis (sqrt (abs r)) ((pi + a)/2)) ^ 2 = rcis (- abs r) a"
   5.631 +  unfolding power2_eq_square
   5.632 +  apply (simp add: rcis_mult add_divide_distrib)
   5.633 +  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
   5.634 +  done
   5.635 +
   5.636 +text {* Nonzero polynomial in z goes to infinity as z does. *}
   5.637 +
   5.638 +lemma poly_infinity:
   5.639 +  assumes ex: "p \<noteq> 0"
   5.640 +  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
   5.641 +using ex
   5.642 +proof(induct p arbitrary: a d)
   5.643 +  case (pCons c cs a d) 
   5.644 +  {assume H: "cs \<noteq> 0"
   5.645 +    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
   5.646 +    let ?r = "1 + \<bar>r\<bar>"
   5.647 +    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
   5.648 +      have r0: "r \<le> cmod z" using h by arith
   5.649 +      from r[rule_format, OF r0]
   5.650 +      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
   5.651 +      from h have z1: "cmod z \<ge> 1" by arith
   5.652 +      from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
   5.653 +      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
   5.654 +	unfolding norm_mult by (simp add: algebra_simps)
   5.655 +      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
   5.656 +      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   5.657 +	by (simp add: diff_le_eq algebra_simps) 
   5.658 +      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
   5.659 +    hence ?case by blast}
   5.660 +  moreover
   5.661 +  {assume cs0: "\<not> (cs \<noteq> 0)"
   5.662 +    with pCons.prems have c0: "c \<noteq> 0" by simp
   5.663 +    from cs0 have cs0': "cs = 0" by simp
   5.664 +    {fix z
   5.665 +      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
   5.666 +      from c0 have "cmod c > 0" by simp
   5.667 +      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)" 
   5.668 +	by (simp add: field_simps norm_mult)
   5.669 +      have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
   5.670 +      from complex_mod_triangle_sub[of "z*c" a ]
   5.671 +      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
   5.672 +	by (simp add: algebra_simps)
   5.673 +      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)" 
   5.674 +        using cs0' by simp}
   5.675 +    then have ?case  by blast}
   5.676 +  ultimately show ?case by blast
   5.677 +qed simp
   5.678 +
   5.679 +text {* Hence polynomial's modulus attains its minimum somewhere. *}
   5.680 +lemma poly_minimum_modulus:
   5.681 +  "\<exists>z.\<forall>w. cmod (poly p z) \<le> cmod (poly p w)"
   5.682 +proof(induct p)
   5.683 +  case (pCons c cs) 
   5.684 +  {assume cs0: "cs \<noteq> 0"
   5.685 +    from poly_infinity[OF cs0, of "cmod (poly (pCons c cs) 0)" c]
   5.686 +    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
   5.687 +    have ath: "\<And>z r. r \<le> cmod z \<or> cmod z \<le> \<bar>r\<bar>" by arith
   5.688 +    from poly_minimum_modulus_disc[of "\<bar>r\<bar>" "pCons c cs"] 
   5.689 +    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
   5.690 +    {fix z assume z: "r \<le> cmod z"
   5.691 +      from v[of 0] r[OF z] 
   5.692 +      have "cmod (poly (pCons c cs) v) \<le> cmod (poly (pCons c cs) z)"
   5.693 +	by simp }
   5.694 +    note v0 = this
   5.695 +    from v0 v ath[of r] have ?case by blast}
   5.696 +  moreover
   5.697 +  {assume cs0: "\<not> (cs \<noteq> 0)"
   5.698 +    hence th:"cs = 0" by simp
   5.699 +    from th pCons.hyps have ?case by simp}
   5.700 +  ultimately show ?case by blast
   5.701 +qed simp
   5.702 +
   5.703 +text{* Constant function (non-syntactic characterization). *}
   5.704 +definition "constant f = (\<forall>x y. f x = f y)"
   5.705 +
   5.706 +lemma nonconstant_length: "\<not> (constant (poly p)) \<Longrightarrow> psize p \<ge> 2"
   5.707 +  unfolding constant_def psize_def
   5.708 +  apply (induct p, auto)
   5.709 +  done
   5.710 + 
   5.711 +lemma poly_replicate_append:
   5.712 +  "poly (monom 1 n * p) (x::'a::{recpower, comm_ring_1}) = x^n * poly p x"
   5.713 +  by (simp add: poly_monom)
   5.714 +
   5.715 +text {* Decomposition of polynomial, skipping zero coefficients 
   5.716 +  after the first.  *}
   5.717 +
   5.718 +lemma poly_decompose_lemma:
   5.719 + assumes nz: "\<not>(\<forall>z. z\<noteq>0 \<longrightarrow> poly p z = (0::'a::{recpower,idom}))"
   5.720 +  shows "\<exists>k a q. a\<noteq>0 \<and> Suc (psize q + k) = psize p \<and> 
   5.721 +                 (\<forall>z. poly p z = z^k * poly (pCons a q) z)"
   5.722 +unfolding psize_def
   5.723 +using nz
   5.724 +proof(induct p)
   5.725 +  case 0 thus ?case by simp
   5.726 +next
   5.727 +  case (pCons c cs)
   5.728 +  {assume c0: "c = 0"
   5.729 +    from pCons.hyps pCons.prems c0 have ?case apply auto
   5.730 +      apply (rule_tac x="k+1" in exI)
   5.731 +      apply (rule_tac x="a" in exI, clarsimp)
   5.732 +      apply (rule_tac x="q" in exI)
   5.733 +      by (auto simp add: power_Suc)}
   5.734 +  moreover
   5.735 +  {assume c0: "c\<noteq>0"
   5.736 +    hence ?case apply-
   5.737 +      apply (rule exI[where x=0])
   5.738 +      apply (rule exI[where x=c], clarsimp)
   5.739 +      apply (rule exI[where x=cs])
   5.740 +      apply auto
   5.741 +      done}
   5.742 +  ultimately show ?case by blast
   5.743 +qed
   5.744 +
   5.745 +lemma poly_decompose:
   5.746 +  assumes nc: "~constant(poly p)"
   5.747 +  shows "\<exists>k a q. a\<noteq>(0::'a::{recpower,idom}) \<and> k\<noteq>0 \<and>
   5.748 +               psize q + k + 1 = psize p \<and> 
   5.749 +              (\<forall>z. poly p z = poly p 0 + z^k * poly (pCons a q) z)"
   5.750 +using nc 
   5.751 +proof(induct p)
   5.752 +  case 0 thus ?case by (simp add: constant_def)
   5.753 +next
   5.754 +  case (pCons c cs)
   5.755 +  {assume C:"\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0"
   5.756 +    {fix x y
   5.757 +      from C have "poly (pCons c cs) x = poly (pCons c cs) y" by (cases "x=0", auto)}
   5.758 +    with pCons.prems have False by (auto simp add: constant_def)}
   5.759 +  hence th: "\<not> (\<forall>z. z \<noteq> 0 \<longrightarrow> poly cs z = 0)" ..
   5.760 +  from poly_decompose_lemma[OF th] 
   5.761 +  show ?case 
   5.762 +    apply clarsimp
   5.763 +    apply (rule_tac x="k+1" in exI)
   5.764 +    apply (rule_tac x="a" in exI)
   5.765 +    apply simp
   5.766 +    apply (rule_tac x="q" in exI)
   5.767 +    apply (auto simp add: power_Suc)
   5.768 +    apply (auto simp add: psize_def split: if_splits)
   5.769 +    done
   5.770 +qed
   5.771 +
   5.772 +text{* Fundamental theorem of algebral *}
   5.773 +
   5.774 +lemma fundamental_theorem_of_algebra:
   5.775 +  assumes nc: "~constant(poly p)"
   5.776 +  shows "\<exists>z::complex. poly p z = 0"
   5.777 +using nc
   5.778 +proof(induct n\<equiv> "psize p" arbitrary: p rule: nat_less_induct)
   5.779 +  fix n fix p :: "complex poly"
   5.780 +  let ?p = "poly p"
   5.781 +  assume H: "\<forall>m<n. \<forall>p. \<not> constant (poly p) \<longrightarrow> m = psize p \<longrightarrow> (\<exists>(z::complex). poly p z = 0)" and nc: "\<not> constant ?p" and n: "n = psize p"
   5.782 +  let ?ths = "\<exists>z. ?p z = 0"
   5.783 +
   5.784 +  from nonconstant_length[OF nc] have n2: "n\<ge> 2" by (simp add: n)
   5.785 +  from poly_minimum_modulus obtain c where 
   5.786 +    c: "\<forall>w. cmod (?p c) \<le> cmod (?p w)" by blast
   5.787 +  {assume pc: "?p c = 0" hence ?ths by blast}
   5.788 +  moreover
   5.789 +  {assume pc0: "?p c \<noteq> 0"
   5.790 +    from poly_offset[of p c] obtain q where
   5.791 +      q: "psize q = psize p" "\<forall>x. poly q x = ?p (c+x)" by blast
   5.792 +    {assume h: "constant (poly q)"
   5.793 +      from q(2) have th: "\<forall>x. poly q (x - c) = ?p x" by auto
   5.794 +      {fix x y
   5.795 +	from th have "?p x = poly q (x - c)" by auto 
   5.796 +	also have "\<dots> = poly q (y - c)" 
   5.797 +	  using h unfolding constant_def by blast
   5.798 +	also have "\<dots> = ?p y" using th by auto
   5.799 +	finally have "?p x = ?p y" .}
   5.800 +      with nc have False unfolding constant_def by blast }
   5.801 +    hence qnc: "\<not> constant (poly q)" by blast
   5.802 +    from q(2) have pqc0: "?p c = poly q 0" by simp
   5.803 +    from c pqc0 have cq0: "\<forall>w. cmod (poly q 0) \<le> cmod (?p w)" by simp 
   5.804 +    let ?a0 = "poly q 0"
   5.805 +    from pc0 pqc0 have a00: "?a0 \<noteq> 0" by simp 
   5.806 +    from a00 
   5.807 +    have qr: "\<forall>z. poly q z = poly (smult (inverse ?a0) q) z * ?a0"
   5.808 +      by simp
   5.809 +    let ?r = "smult (inverse ?a0) q"
   5.810 +    have lgqr: "psize q = psize ?r"
   5.811 +      using a00 unfolding psize_def degree_def
   5.812 +      by (simp add: expand_poly_eq)
   5.813 +    {assume h: "\<And>x y. poly ?r x = poly ?r y"
   5.814 +      {fix x y
   5.815 +	from qr[rule_format, of x] 
   5.816 +	have "poly q x = poly ?r x * ?a0" by auto
   5.817 +	also have "\<dots> = poly ?r y * ?a0" using h by simp
   5.818 +	also have "\<dots> = poly q y" using qr[rule_format, of y] by simp
   5.819 +	finally have "poly q x = poly q y" .} 
   5.820 +      with qnc have False unfolding constant_def by blast}
   5.821 +    hence rnc: "\<not> constant (poly ?r)" unfolding constant_def by blast
   5.822 +    from qr[rule_format, of 0] a00  have r01: "poly ?r 0 = 1" by auto
   5.823 +    {fix w 
   5.824 +      have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w / ?a0) < 1"
   5.825 +	using qr[rule_format, of w] a00 by (simp add: divide_inverse mult_ac)
   5.826 +      also have "\<dots> \<longleftrightarrow> cmod (poly q w) < cmod ?a0"
   5.827 +	using a00 unfolding norm_divide by (simp add: field_simps)
   5.828 +      finally have "cmod (poly ?r w) < 1 \<longleftrightarrow> cmod (poly q w) < cmod ?a0" .}
   5.829 +    note mrmq_eq = this
   5.830 +    from poly_decompose[OF rnc] obtain k a s where 
   5.831 +      kas: "a\<noteq>0" "k\<noteq>0" "psize s + k + 1 = psize ?r" 
   5.832 +      "\<forall>z. poly ?r z = poly ?r 0 + z^k* poly (pCons a s) z" by blast
   5.833 +    {assume "k + 1 = n"
   5.834 +      with kas(3) lgqr[symmetric] q(1) n[symmetric] have s0:"s=0" by auto
   5.835 +      {fix w
   5.836 +	have "cmod (poly ?r w) = cmod (1 + a * w ^ k)" 
   5.837 +	  using kas(4)[rule_format, of w] s0 r01 by (simp add: algebra_simps)}
   5.838 +      note hth = this [symmetric]
   5.839 +	from reduce_poly_simple[OF kas(1,2)] 
   5.840 +      have "\<exists>w. cmod (poly ?r w) < 1" unfolding hth by blast}
   5.841 +    moreover
   5.842 +    {assume kn: "k+1 \<noteq> n"
   5.843 +      from kn kas(3) q(1) n[symmetric] lgqr have k1n: "k + 1 < n" by simp
   5.844 +      have th01: "\<not> constant (poly (pCons 1 (monom a (k - 1))))" 
   5.845 +	unfolding constant_def poly_pCons poly_monom
   5.846 +	using kas(1) apply simp 
   5.847 +	by (rule exI[where x=0], rule exI[where x=1], simp)
   5.848 +      from kas(1) kas(2) have th02: "k+1 = psize (pCons 1 (monom a (k - 1)))"
   5.849 +	by (simp add: psize_def degree_monom_eq)
   5.850 +      from H[rule_format, OF k1n th01 th02]
   5.851 +      obtain w where w: "1 + w^k * a = 0"
   5.852 +	unfolding poly_pCons poly_monom
   5.853 +	using kas(2) by (cases k, auto simp add: algebra_simps)
   5.854 +      from poly_bound_exists[of "cmod w" s] obtain m where 
   5.855 +	m: "m > 0" "\<forall>z. cmod z \<le> cmod w \<longrightarrow> cmod (poly s z) \<le> m" by blast
   5.856 +      have w0: "w\<noteq>0" using kas(2) w by (auto simp add: power_0_left)
   5.857 +      from w have "(1 + w ^ k * a) - 1 = 0 - 1" by simp
   5.858 +      then have wm1: "w^k * a = - 1" by simp
   5.859 +      have inv0: "0 < inverse (cmod w ^ (k + 1) * m)" 
   5.860 +	using norm_ge_zero[of w] w0 m(1)
   5.861 +	  by (simp add: inverse_eq_divide zero_less_mult_iff)
   5.862 +      with real_down2[OF zero_less_one] obtain t where
   5.863 +	t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
   5.864 +      let ?ct = "complex_of_real t"
   5.865 +      let ?w = "?ct * w"
   5.866 +      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)
   5.867 +      also have "\<dots> = complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w"
   5.868 +	unfolding wm1 by (simp)
   5.869 +      finally have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) = cmod (complex_of_real (1 - t^k) + ?w^k * ?w * poly s ?w)" 
   5.870 +	apply -
   5.871 +	apply (rule cong[OF refl[of cmod]])
   5.872 +	apply assumption
   5.873 +	done
   5.874 +      with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"] 
   5.875 +      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 
   5.876 +      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
   5.877 +      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
   5.878 +      then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult) 
   5.879 +      from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
   5.880 +	by (simp add: inverse_eq_divide field_simps)
   5.881 +      with zero_less_power[OF t(1), of k] 
   5.882 +      have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1" 
   5.883 +	apply - apply (rule mult_strict_left_mono) by simp_all
   5.884 +      have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
   5.885 +	by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
   5.886 +      then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
   5.887 +	using t(1,2) m(2)[rule_format, OF tw] w0
   5.888 +	apply (simp only: )
   5.889 +	apply auto
   5.890 +	apply (rule mult_mono, simp_all add: norm_ge_zero)+
   5.891 +	apply (simp add: zero_le_mult_iff zero_le_power)
   5.892 +	done
   5.893 +      with th30 have th120: "cmod (?w^k * ?w * poly s ?w) < t^k" by simp 
   5.894 +      from power_strict_mono[OF t(2), of k] t(1) kas(2) have th121: "t^k \<le> 1" 
   5.895 +	by auto
   5.896 +      from ath[OF norm_ge_zero[of "?w^k * ?w * poly s ?w"] th120 th121]
   5.897 +      have th12: "\<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w) < 1" . 
   5.898 +      from th11 th12
   5.899 +      have "cmod (1 + ?w^k * (a + ?w * poly s ?w)) < 1"  by arith 
   5.900 +      then have "cmod (poly ?r ?w) < 1" 
   5.901 +	unfolding kas(4)[rule_format, of ?w] r01 by simp 
   5.902 +      then have "\<exists>w. cmod (poly ?r w) < 1" by blast}
   5.903 +    ultimately have cr0_contr: "\<exists>w. cmod (poly ?r w) < 1" by blast
   5.904 +    from cr0_contr cq0 q(2)
   5.905 +    have ?ths unfolding mrmq_eq not_less[symmetric] by auto}
   5.906 +  ultimately show ?ths by blast
   5.907 +qed
   5.908 +
   5.909 +text {* Alternative version with a syntactic notion of constant polynomial. *}
   5.910 +
   5.911 +lemma fundamental_theorem_of_algebra_alt:
   5.912 +  assumes nc: "~(\<exists>a l. a\<noteq> 0 \<and> l = 0 \<and> p = pCons a l)"
   5.913 +  shows "\<exists>z. poly p z = (0::complex)"
   5.914 +using nc
   5.915 +proof(induct p)
   5.916 +  case (pCons c cs)
   5.917 +  {assume "c=0" hence ?case by auto}
   5.918 +  moreover
   5.919 +  {assume c0: "c\<noteq>0"
   5.920 +    {assume nc: "constant (poly (pCons c cs))"
   5.921 +      from nc[unfolded constant_def, rule_format, of 0] 
   5.922 +      have "\<forall>w. w \<noteq> 0 \<longrightarrow> poly cs w = 0" by auto 
   5.923 +      hence "cs = 0"
   5.924 +	proof(induct cs)
   5.925 +	  case (pCons d ds)
   5.926 +	  {assume "d=0" hence ?case using pCons.prems pCons.hyps by simp}
   5.927 +	  moreover
   5.928 +	  {assume d0: "d\<noteq>0"
   5.929 +	    from poly_bound_exists[of 1 ds] obtain m where 
   5.930 +	      m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   5.931 +	    have dm: "cmod d / m > 0" using d0 m(1) by (simp add: field_simps)
   5.932 +	    from real_down2[OF dm zero_less_one] obtain x where 
   5.933 +	      x: "x > 0" "x < cmod d / m" "x < 1" by blast
   5.934 +	    let ?x = "complex_of_real x"
   5.935 +	    from x have cx: "?x \<noteq> 0"  "cmod ?x \<le> 1" by simp_all
   5.936 +	    from pCons.prems[rule_format, OF cx(1)]
   5.937 +	    have cth: "cmod (?x*poly ds ?x) = cmod d" by (simp add: eq_diff_eq[symmetric])
   5.938 +	    from m(2)[rule_format, OF cx(2)] x(1)
   5.939 +	    have th0: "cmod (?x*poly ds ?x) \<le> x*m"
   5.940 +	      by (simp add: norm_mult)
   5.941 +	    from x(2) m(1) have "x*m < cmod d" by (simp add: field_simps)
   5.942 +	    with th0 have "cmod (?x*poly ds ?x) \<noteq> cmod d" by auto
   5.943 +	    with cth  have ?case by blast}
   5.944 +	  ultimately show ?case by blast 
   5.945 +	qed simp}
   5.946 +      then have nc: "\<not> constant (poly (pCons c cs))" using pCons.prems c0 
   5.947 +	by blast
   5.948 +      from fundamental_theorem_of_algebra[OF nc] have ?case .}
   5.949 +  ultimately show ?case by blast  
   5.950 +qed simp
   5.951 +
   5.952 +subsection {* Order of polynomial roots *}
   5.953 +
   5.954 +definition
   5.955 +  order :: "'a::{idom,recpower} \<Rightarrow> 'a poly \<Rightarrow> nat"
   5.956 +where
   5.957 +  [code del]:
   5.958 +  "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)"
   5.959 +
   5.960 +lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
   5.961 +by (induct n, simp, auto intro: order_trans degree_mult_le)
   5.962 +
   5.963 +lemma coeff_linear_power:
   5.964 +  fixes a :: "'a::{comm_semiring_1,recpower}"
   5.965 +  shows "coeff ([:a, 1:] ^ n) n = 1"
   5.966 +apply (induct n, simp_all)
   5.967 +apply (subst coeff_eq_0)
   5.968 +apply (auto intro: le_less_trans degree_power_le)
   5.969 +done
   5.970 +
   5.971 +lemma degree_linear_power:
   5.972 +  fixes a :: "'a::{comm_semiring_1,recpower}"
   5.973 +  shows "degree ([:a, 1:] ^ n) = n"
   5.974 +apply (rule order_antisym)
   5.975 +apply (rule ord_le_eq_trans [OF degree_power_le], simp)
   5.976 +apply (rule le_degree, simp add: coeff_linear_power)
   5.977 +done
   5.978 +
   5.979 +lemma order_1: "[:-a, 1:] ^ order a p dvd p"
   5.980 +apply (cases "p = 0", simp)
   5.981 +apply (cases "order a p", simp)
   5.982 +apply (subgoal_tac "nat < (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)")
   5.983 +apply (drule not_less_Least, simp)
   5.984 +apply (fold order_def, simp)
   5.985 +done
   5.986 +
   5.987 +lemma order_2: "p \<noteq> 0 \<Longrightarrow> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
   5.988 +unfolding order_def
   5.989 +apply (rule LeastI_ex)
   5.990 +apply (rule_tac x="degree p" in exI)
   5.991 +apply (rule notI)
   5.992 +apply (drule (1) dvd_imp_degree_le)
   5.993 +apply (simp only: degree_linear_power)
   5.994 +done
   5.995 +
   5.996 +lemma order:
   5.997 +  "p \<noteq> 0 \<Longrightarrow> [:-a, 1:] ^ order a p dvd p \<and> \<not> [:-a, 1:] ^ Suc (order a p) dvd p"
   5.998 +by (rule conjI [OF order_1 order_2])
   5.999 +
  5.1000 +lemma order_degree:
  5.1001 +  assumes p: "p \<noteq> 0"
  5.1002 +  shows "order a p \<le> degree p"
  5.1003 +proof -
  5.1004 +  have "order a p = degree ([:-a, 1:] ^ order a p)"
  5.1005 +    by (simp only: degree_linear_power)
  5.1006 +  also have "\<dots> \<le> degree p"
  5.1007 +    using order_1 p by (rule dvd_imp_degree_le)
  5.1008 +  finally show ?thesis .
  5.1009 +qed
  5.1010 +
  5.1011 +lemma order_root: "poly p a = 0 \<longleftrightarrow> p = 0 \<or> order a p \<noteq> 0"
  5.1012 +apply (cases "p = 0", simp_all)
  5.1013 +apply (rule iffI)
  5.1014 +apply (rule ccontr, simp)
  5.1015 +apply (frule order_2 [where a=a], simp)
  5.1016 +apply (simp add: poly_eq_0_iff_dvd)
  5.1017 +apply (simp add: poly_eq_0_iff_dvd)
  5.1018 +apply (simp only: order_def)
  5.1019 +apply (drule not_less_Least, simp)
  5.1020 +done
  5.1021 +
  5.1022 +lemma poly_zero:
  5.1023 +  fixes p :: "'a::{idom,ring_char_0} poly"
  5.1024 +  shows "poly p = poly 0 \<longleftrightarrow> p = 0"
  5.1025 +apply (cases "p = 0", simp_all)
  5.1026 +apply (drule poly_roots_finite)
  5.1027 +apply (auto simp add: infinite_UNIV_char_0)
  5.1028 +done
  5.1029 +
  5.1030 +lemma poly_eq_iff:
  5.1031 +  fixes p q :: "'a::{idom,ring_char_0} poly"
  5.1032 +  shows "poly p = poly q \<longleftrightarrow> p = q"
  5.1033 +  using poly_zero [of "p - q"]
  5.1034 +  by (simp add: expand_fun_eq)
  5.1035 +
  5.1036 +
  5.1037 +subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
  5.1038 +
  5.1039 +lemma nullstellensatz_lemma:
  5.1040 +  fixes p :: "complex poly"
  5.1041 +  assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
  5.1042 +  and "degree p = n" and "n \<noteq> 0"
  5.1043 +  shows "p dvd (q ^ n)"
  5.1044 +using prems
  5.1045 +proof(induct n arbitrary: p q rule: nat_less_induct)
  5.1046 +  fix n::nat fix p q :: "complex poly"
  5.1047 +  assume IH: "\<forall>m<n. \<forall>p q.
  5.1048 +                 (\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longrightarrow>
  5.1049 +                 degree p = m \<longrightarrow> m \<noteq> 0 \<longrightarrow> p dvd (q ^ m)"
  5.1050 +    and pq0: "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0" 
  5.1051 +    and dpn: "degree p = n" and n0: "n \<noteq> 0"
  5.1052 +  from dpn n0 have pne: "p \<noteq> 0" by auto
  5.1053 +  let ?ths = "p dvd (q ^ n)"
  5.1054 +  {fix a assume a: "poly p a = 0"
  5.1055 +    {assume oa: "order a p \<noteq> 0"
  5.1056 +      let ?op = "order a p"
  5.1057 +      from pne have ap: "([:- a, 1:] ^ ?op) dvd p" 
  5.1058 +	"\<not> [:- a, 1:] ^ (Suc ?op) dvd p" using order by blast+ 
  5.1059 +      note oop = order_degree[OF pne, unfolded dpn]
  5.1060 +      {assume q0: "q = 0"
  5.1061 +	hence ?ths using n0
  5.1062 +          by (simp add: power_0_left)}
  5.1063 +      moreover
  5.1064 +      {assume q0: "q \<noteq> 0"
  5.1065 +	from pq0[rule_format, OF a, unfolded poly_eq_0_iff_dvd]
  5.1066 +	obtain r where r: "q = [:- a, 1:] * r" by (rule dvdE)
  5.1067 +	from ap(1) obtain s where
  5.1068 +	  s: "p = [:- a, 1:] ^ ?op * s" by (rule dvdE)
  5.1069 +	have sne: "s \<noteq> 0"
  5.1070 +	  using s pne by auto
  5.1071 +	{assume ds0: "degree s = 0"
  5.1072 +	  from ds0 have "\<exists>k. s = [:k:]"
  5.1073 +            by (cases s, simp split: if_splits)
  5.1074 +	  then obtain k where kpn: "s = [:k:]" by blast
  5.1075 +          from sne kpn have k: "k \<noteq> 0" by simp
  5.1076 +	  let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
  5.1077 +          from k oop [of a] have "q ^ n = p * ?w"
  5.1078 +            apply -
  5.1079 +            apply (subst r, subst s, subst kpn)
  5.1080 +            apply (subst power_mult_distrib, simp)
  5.1081 +            apply (subst power_add [symmetric], simp)
  5.1082 +            done
  5.1083 +	  hence ?ths unfolding dvd_def by blast}
  5.1084 +	moreover
  5.1085 +	{assume ds0: "degree s \<noteq> 0"
  5.1086 +	  from ds0 sne dpn s oa
  5.1087 +	    have dsn: "degree s < n" apply auto
  5.1088 +              apply (erule ssubst)
  5.1089 +              apply (simp add: degree_mult_eq degree_linear_power)
  5.1090 +              done
  5.1091 +	    {fix x assume h: "poly s x = 0"
  5.1092 +	      {assume xa: "x = a"
  5.1093 +		from h[unfolded xa poly_eq_0_iff_dvd] obtain u where
  5.1094 +		  u: "s = [:- a, 1:] * u" by (rule dvdE)
  5.1095 +		have "p = [:- a, 1:] ^ (Suc ?op) * u"
  5.1096 +                  by (subst s, subst u, simp only: power_Suc mult_ac)
  5.1097 +		with ap(2)[unfolded dvd_def] have False by blast}
  5.1098 +	      note xa = this
  5.1099 +	      from h have "poly p x = 0" by (subst s, simp)
  5.1100 +	      with pq0 have "poly q x = 0" by blast
  5.1101 +	      with r xa have "poly r x = 0"
  5.1102 +                by (auto simp add: uminus_add_conv_diff)}
  5.1103 +	    note impth = this
  5.1104 +	    from IH[rule_format, OF dsn, of s r] impth ds0
  5.1105 +	    have "s dvd (r ^ (degree s))" by blast
  5.1106 +	    then obtain u where u: "r ^ (degree s) = s * u" ..
  5.1107 +	    hence u': "\<And>x. poly s x * poly u x = poly r x ^ degree s"
  5.1108 +              by (simp only: poly_mult[symmetric] poly_power[symmetric])
  5.1109 +	    let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))"
  5.1110 +	    from oop[of a] dsn have "q ^ n = p * ?w"
  5.1111 +              apply -
  5.1112 +              apply (subst s, subst r)
  5.1113 +              apply (simp only: power_mult_distrib)
  5.1114 +              apply (subst mult_assoc [where b=s])
  5.1115 +              apply (subst mult_assoc [where a=u])
  5.1116 +              apply (subst mult_assoc [where b=u, symmetric])
  5.1117 +              apply (subst u [symmetric])
  5.1118 +              apply (simp add: mult_ac power_add [symmetric])
  5.1119 +              done
  5.1120 +	    hence ?ths unfolding dvd_def by blast}
  5.1121 +      ultimately have ?ths by blast }
  5.1122 +      ultimately have ?ths by blast}
  5.1123 +    then have ?ths using a order_root pne by blast}
  5.1124 +  moreover
  5.1125 +  {assume exa: "\<not> (\<exists>a. poly p a = 0)"
  5.1126 +    from fundamental_theorem_of_algebra_alt[of p] exa obtain c where
  5.1127 +      ccs: "c\<noteq>0" "p = pCons c 0" by blast
  5.1128 +    
  5.1129 +    then have pp: "\<And>x. poly p x =  c" by simp
  5.1130 +    let ?w = "[:1/c:] * (q ^ n)"
  5.1131 +    from ccs
  5.1132 +    have "(q ^ n) = (p * ?w) "
  5.1133 +      by (simp add: smult_smult)
  5.1134 +    hence ?ths unfolding dvd_def by blast}
  5.1135 +  ultimately show ?ths by blast
  5.1136 +qed
  5.1137 +
  5.1138 +lemma nullstellensatz_univariate:
  5.1139 +  "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> 
  5.1140 +    p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
  5.1141 +proof-
  5.1142 +  {assume pe: "p = 0"
  5.1143 +    hence eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
  5.1144 +      apply auto
  5.1145 +      apply (rule poly_zero [THEN iffD1])
  5.1146 +      by (rule ext, simp)
  5.1147 +    {assume "p dvd (q ^ (degree p))"
  5.1148 +      then obtain r where r: "q ^ (degree p) = p * r" ..
  5.1149 +      from r pe have False by simp}
  5.1150 +    with eq pe have ?thesis by blast}
  5.1151 +  moreover
  5.1152 +  {assume pe: "p \<noteq> 0"
  5.1153 +    {assume dp: "degree p = 0"
  5.1154 +      then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
  5.1155 +        by (cases p, simp split: if_splits)
  5.1156 +      hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
  5.1157 +      from k dp have "q ^ (degree p) = p * [:1/k:]"
  5.1158 +        by (simp add: one_poly_def)
  5.1159 +      hence th2: "p dvd (q ^ (degree p))" ..
  5.1160 +      from th1 th2 pe have ?thesis by blast}
  5.1161 +    moreover
  5.1162 +    {assume dp: "degree p \<noteq> 0"
  5.1163 +      then obtain n where n: "degree p = Suc n " by (cases "degree p", auto)
  5.1164 +      {assume "p dvd (q ^ (Suc n))"
  5.1165 +	then obtain u where u: "q ^ (Suc n) = p * u" ..
  5.1166 +	{fix x assume h: "poly p x = 0" "poly q x \<noteq> 0"
  5.1167 +	  hence "poly (q ^ (Suc n)) x \<noteq> 0" by simp
  5.1168 +	  hence False using u h(1) by (simp only: poly_mult) simp}}
  5.1169 +	with n nullstellensatz_lemma[of p q "degree p"] dp 
  5.1170 +	have ?thesis by auto}
  5.1171 +    ultimately have ?thesis by blast}
  5.1172 +  ultimately show ?thesis by blast
  5.1173 +qed
  5.1174 +
  5.1175 +text{* Useful lemma *}
  5.1176 +
  5.1177 +lemma constant_degree:
  5.1178 +  fixes p :: "'a::{idom,ring_char_0} poly"
  5.1179 +  shows "constant (poly p) \<longleftrightarrow> degree p = 0" (is "?lhs = ?rhs")
  5.1180 +proof
  5.1181 +  assume l: ?lhs
  5.1182 +  from l[unfolded constant_def, rule_format, of _ "0"]
  5.1183 +  have th: "poly p = poly [:poly p 0:]" apply - by (rule ext, simp)
  5.1184 +  then have "p = [:poly p 0:]" by (simp add: poly_eq_iff)
  5.1185 +  then have "degree p = degree [:poly p 0:]" by simp
  5.1186 +  then show ?rhs by simp
  5.1187 +next
  5.1188 +  assume r: ?rhs
  5.1189 +  then obtain k where "p = [:k:]"
  5.1190 +    by (cases p, simp split: if_splits)
  5.1191 +  then show ?lhs unfolding constant_def by auto
  5.1192 +qed
  5.1193 +
  5.1194 +lemma divides_degree: assumes pq: "p dvd (q:: complex poly)"
  5.1195 +  shows "degree p \<le> degree q \<or> q = 0"
  5.1196 +apply (cases "q = 0", simp_all)
  5.1197 +apply (erule dvd_imp_degree_le [OF pq])
  5.1198 +done
  5.1199 +
  5.1200 +(* Arithmetic operations on multivariate polynomials.                        *)
  5.1201 +
  5.1202 +lemma mpoly_base_conv: 
  5.1203 +  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
  5.1204 +
  5.1205 +lemma mpoly_norm_conv: 
  5.1206 +  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
  5.1207 +
  5.1208 +lemma mpoly_sub_conv: 
  5.1209 +  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
  5.1210 +  by (simp add: diff_def)
  5.1211 +
  5.1212 +lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
  5.1213 +
  5.1214 +lemma poly_cancel_eq_conv: "p = (0::complex) \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (q = 0) \<equiv> (a * q - b * p = 0)" apply (atomize (full)) by auto
  5.1215 +
  5.1216 +lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
  5.1217 +lemma  resolve_eq_then: "(P \<Longrightarrow> (Q \<equiv> Q1)) \<Longrightarrow> (\<not>P \<Longrightarrow> (Q \<equiv> Q2))
  5.1218 +  \<Longrightarrow> Q \<equiv> P \<and> Q1 \<or> \<not>P\<and> Q2" apply (atomize (full)) by blast 
  5.1219 +
  5.1220 +lemma poly_divides_pad_rule: 
  5.1221 +  fixes p q :: "complex poly"
  5.1222 +  assumes pq: "p dvd q"
  5.1223 +  shows "p dvd (pCons (0::complex) q)"
  5.1224 +proof-
  5.1225 +  have "pCons 0 q = q * [:0,1:]" by simp
  5.1226 +  then have "q dvd (pCons 0 q)" ..
  5.1227 +  with pq show ?thesis by (rule dvd_trans)
  5.1228 +qed
  5.1229 +
  5.1230 +lemma poly_divides_pad_const_rule: 
  5.1231 +  fixes p q :: "complex poly"
  5.1232 +  assumes pq: "p dvd q"
  5.1233 +  shows "p dvd (smult a q)"
  5.1234 +proof-
  5.1235 +  have "smult a q = q * [:a:]" by simp
  5.1236 +  then have "q dvd smult a q" ..
  5.1237 +  with pq show ?thesis by (rule dvd_trans)
  5.1238 +qed
  5.1239 +
  5.1240 +
  5.1241 +lemma poly_divides_conv0:  
  5.1242 +  fixes p :: "complex poly"
  5.1243 +  assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
  5.1244 +  shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
  5.1245 +proof-
  5.1246 +  {assume r: ?rhs 
  5.1247 +    hence "q = p * 0" by simp
  5.1248 +    hence ?lhs ..}
  5.1249 +  moreover
  5.1250 +  {assume l: ?lhs
  5.1251 +    {assume q0: "q = 0"
  5.1252 +      hence ?rhs by simp}
  5.1253 +    moreover
  5.1254 +    {assume q0: "q \<noteq> 0"
  5.1255 +      from l q0 have "degree p \<le> degree q"
  5.1256 +        by (rule dvd_imp_degree_le)
  5.1257 +      with lgpq have ?rhs by simp }
  5.1258 +    ultimately have ?rhs by blast }
  5.1259 +  ultimately show "?lhs \<equiv> ?rhs" by - (atomize (full), blast) 
  5.1260 +qed
  5.1261 +
  5.1262 +lemma poly_divides_conv1: 
  5.1263 +  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
  5.1264 +  and qrp': "smult a q - p' \<equiv> r"
  5.1265 +  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
  5.1266 +proof-
  5.1267 +  {
  5.1268 +  from pp' obtain t where t: "p' = p * t" ..
  5.1269 +  {assume l: ?lhs
  5.1270 +    then obtain u where u: "q = p * u" ..
  5.1271 +     have "r = p * (smult a u - t)"
  5.1272 +       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
  5.1273 +     then have ?rhs ..}
  5.1274 +  moreover
  5.1275 +  {assume r: ?rhs
  5.1276 +    then obtain u where u: "r = p * u" ..
  5.1277 +    from u [symmetric] t qrp' [symmetric] a0
  5.1278 +    have "q = p * smult (1/a) (u + t)"
  5.1279 +      by (simp add: algebra_simps mult_smult_right smult_smult)
  5.1280 +    hence ?lhs ..}
  5.1281 +  ultimately have "?lhs = ?rhs" by blast }
  5.1282 +thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast) 
  5.1283 +qed
  5.1284 +
  5.1285 +lemma basic_cqe_conv1:
  5.1286 +  "(\<exists>x. poly p x = 0 \<and> poly 0 x \<noteq> 0) \<equiv> False"
  5.1287 +  "(\<exists>x. poly 0 x \<noteq> 0) \<equiv> False"
  5.1288 +  "(\<exists>x. poly [:c:] x \<noteq> 0) \<equiv> c\<noteq>0"
  5.1289 +  "(\<exists>x. poly 0 x = 0) \<equiv> True"
  5.1290 +  "(\<exists>x. poly [:c:] x = 0) \<equiv> c = 0" by simp_all
  5.1291 +
  5.1292 +lemma basic_cqe_conv2: 
  5.1293 +  assumes l:"p \<noteq> 0" 
  5.1294 +  shows "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True"
  5.1295 +proof-
  5.1296 +  {fix h t
  5.1297 +    assume h: "h\<noteq>0" "t=0"  "pCons a (pCons b p) = pCons h t"
  5.1298 +    with l have False by simp}
  5.1299 +  hence th: "\<not> (\<exists> h t. h\<noteq>0 \<and> t=0 \<and> pCons a (pCons b p) = pCons h t)"
  5.1300 +    by blast
  5.1301 +  from fundamental_theorem_of_algebra_alt[OF th] 
  5.1302 +  show "(\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)) \<equiv> True" by auto
  5.1303 +qed
  5.1304 +
  5.1305 +lemma  basic_cqe_conv_2b: "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> (p \<noteq> 0)"
  5.1306 +proof-
  5.1307 +  have "p = 0 \<longleftrightarrow> poly p = poly 0"
  5.1308 +    by (simp add: poly_zero)
  5.1309 +  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
  5.1310 +  finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
  5.1311 +    by - (atomize (full), blast)
  5.1312 +qed
  5.1313 +
  5.1314 +lemma basic_cqe_conv3:
  5.1315 +  fixes p q :: "complex poly"
  5.1316 +  assumes l: "p \<noteq> 0" 
  5.1317 +  shows "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
  5.1318 +proof-
  5.1319 +  from l have dp:"degree (pCons a p) = psize p" by (simp add: psize_def)
  5.1320 +  from nullstellensatz_univariate[of "pCons a p" q] l
  5.1321 +  show "(\<exists>x. poly (pCons a p) x = 0 \<and> poly q x \<noteq> 0) \<equiv> \<not> ((pCons a p) dvd (q ^ (psize p)))"
  5.1322 +    unfolding dp
  5.1323 +    by - (atomize (full), auto)
  5.1324 +qed
  5.1325 +
  5.1326 +lemma basic_cqe_conv4:
  5.1327 +  fixes p q :: "complex poly"
  5.1328 +  assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
  5.1329 +  shows "p dvd (q ^ n) \<equiv> p dvd r"
  5.1330 +proof-
  5.1331 +  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
  5.1332 +  then have "(q ^ n) = r" by (simp add: poly_eq_iff)
  5.1333 +  thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
  5.1334 +qed
  5.1335 +
  5.1336 +lemma pmult_Cons_Cons: "(pCons (a::complex) (pCons b p) * q = (smult a q) + (pCons 0 (pCons b p * q)))"
  5.1337 +  by simp
  5.1338 +
  5.1339 +lemma elim_neg_conv: "- z \<equiv> (-1) * (z::complex)" by simp
  5.1340 +lemma eqT_intr: "PROP P \<Longrightarrow> (True \<Longrightarrow> PROP P )" "PROP P \<Longrightarrow> True" by blast+
  5.1341 +lemma negate_negate_rule: "Trueprop P \<equiv> \<not> P \<equiv> False" by (atomize (full), auto)
  5.1342 +
  5.1343 +lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
  5.1344 +lemma resolve_eq_ne: "(P \<equiv> True) \<equiv> (\<not>P \<equiv> False)" "(P \<equiv> False) \<equiv> (\<not>P \<equiv> True)" 
  5.1345 +  by (atomize (full)) simp_all
  5.1346 +lemma cqe_conv1: "poly 0 x = 0 \<longleftrightarrow> True"  by simp
  5.1347 +lemma cqe_conv2: "(p \<Longrightarrow> (q \<equiv> r)) \<equiv> ((p \<and> q) \<equiv> (p \<and> r))"  (is "?l \<equiv> ?r")
  5.1348 +proof
  5.1349 +  assume "p \<Longrightarrow> q \<equiv> r" thus "p \<and> q \<equiv> p \<and> r" apply - apply (atomize (full)) by blast
  5.1350 +next
  5.1351 +  assume "p \<and> q \<equiv> p \<and> r" "p"
  5.1352 +  thus "q \<equiv> r" apply - apply (atomize (full)) apply blast done
  5.1353 +qed
  5.1354 +lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
  5.1355 +
  5.1356 +end
     6.1 --- a/src/HOL/Library/Library.thy	Wed Feb 11 11:22:42 2009 -0800
     6.2 +++ b/src/HOL/Library/Library.thy	Thu Feb 12 18:14:43 2009 +0100
     6.3 @@ -23,6 +23,7 @@
     6.4    Float
     6.5    Formal_Power_Series
     6.6    FuncSet
     6.7 +  Fundamental_Theorem_Algebra
     6.8    Infinite_Set
     6.9    ListVector
    6.10    Mapping
     7.1 --- a/src/HOL/Library/Univ_Poly.thy	Wed Feb 11 11:22:42 2009 -0800
     7.2 +++ b/src/HOL/Library/Univ_Poly.thy	Thu Feb 12 18:14:43 2009 +0100
     7.3 @@ -344,26 +344,6 @@
     7.4  apply (erule_tac x="x" in allE, clarsimp)
     7.5  by (case_tac "n=length p", auto simp add: order_le_less)
     7.6  
     7.7 -lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
     7.8 -  unfolding finite_conv_nat_seg_image
     7.9 -proof(auto simp add: expand_set_eq image_iff)
    7.10 -  fix n::nat and f:: "nat \<Rightarrow> nat"
    7.11 -  let ?N = "{i. i < n}"
    7.12 -  let ?fN = "f ` ?N"
    7.13 -  let ?y = "Max ?fN + 1"
    7.14 -  from nat_seg_image_imp_finite[of "?fN" "f" n] 
    7.15 -  have thfN: "finite ?fN" by simp
    7.16 -  {assume "n =0" hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto}
    7.17 -  moreover
    7.18 -  {assume nz: "n \<noteq> 0"
    7.19 -    hence thne: "?fN \<noteq> {}" by (auto simp add: neq0_conv)
    7.20 -    have "\<forall>x\<in> ?fN. Max ?fN \<ge> x" using nz Max_ge_iff[OF thfN thne] by auto
    7.21 -    hence "\<forall>x\<in> ?fN. ?y > x" by auto
    7.22 -    hence "?y \<notin> ?fN" by auto
    7.23 -    hence "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by auto }
    7.24 -  ultimately show "\<exists>x. \<forall>xa<n. x \<noteq> f xa" by blast
    7.25 -qed
    7.26 -
    7.27  lemma (in ring_char_0) UNIV_ring_char_0_infinte: 
    7.28    "\<not> (finite (UNIV:: 'a set))" 
    7.29  proof
    7.30 @@ -374,7 +354,7 @@
    7.31      then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)
    7.32      show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)
    7.33    qed
    7.34 -  with UNIV_nat_infinite show False ..
    7.35 +  with infinite_UNIV_nat show False ..
    7.36  qed
    7.37  
    7.38  lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) = 
     8.1 --- a/src/HOL/Nat.thy	Wed Feb 11 11:22:42 2009 -0800
     8.2 +++ b/src/HOL/Nat.thy	Thu Feb 12 18:14:43 2009 +0100
     8.3 @@ -1367,6 +1367,9 @@
     8.4  
     8.5  end
     8.6  
     8.7 +lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
     8.8 +unfolding mono_def
     8.9 +by (auto intro:lift_Suc_mono_le[of f])
    8.10  
    8.11  lemma mono_nat_linear_lb:
    8.12    "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"