author paulson Tue Feb 25 17:06:17 2014 +0000 (2014-02-25) changeset 55735 81ba62493610 parent 55734 3f5b2745d659 child 55736 f1ed1e9cd080
generalised some results using type classes
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 16:17:20 2014 +0000
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 17:06:17 2014 +0000
1.3 @@ -98,27 +98,29 @@
1.4  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
1.5    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
1.6
1.7 -subsection{* Basic lemmas about complex polynomials *}
1.8 +subsection{* Basic lemmas about polynomials *}
1.9
1.10  lemma poly_bound_exists:
1.11 -  shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
1.12 +  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.13 +  shows "\<exists>m. m > 0 \<and> (\<forall>z. norm z <= r \<longrightarrow> norm (poly p z) \<le> m)"
1.14  proof(induct p)
1.15    case 0 thus ?case by (rule exI[where x=1], simp)
1.16  next
1.17    case (pCons c cs)
1.18 -  from pCons.hyps obtain m where m: "\<forall>z. cmod z \<le> r \<longrightarrow> cmod (poly cs z) \<le> m"
1.19 +  from pCons.hyps obtain m where m: "\<forall>z. norm z \<le> r \<longrightarrow> norm (poly cs z) \<le> m"
1.20      by blast
1.21 -  let ?k = " 1 + cmod c + \<bar>r * m\<bar>"
1.22 +  let ?k = " 1 + norm c + \<bar>r * m\<bar>"
1.23    have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
1.24 -  {fix z
1.25 -    assume H: "cmod z \<le> r"
1.26 -    from m H have th: "cmod (poly cs z) \<le> m" by blast
1.27 +  {fix z :: 'a
1.28 +    assume H: "norm z \<le> r"
1.29 +    from m H have th: "norm (poly cs z) \<le> m" by blast
1.30      from H have rp: "r \<ge> 0" using norm_ge_zero[of z] by arith
1.31 -    have "cmod (poly (pCons c cs) z) \<le> cmod c + cmod (z* poly cs z)"
1.32 +    have "norm (poly (pCons c cs) z) \<le> norm c + norm (z* poly cs z)"
1.33        using norm_triangle_ineq[of c "z* poly cs z"] by simp
1.34 -    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)
1.35 +    also have "\<dots> \<le> norm c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]]
1.36 +      by (simp add: norm_mult)
1.37      also have "\<dots> \<le> ?k" by simp
1.38 -    finally have "cmod (poly (pCons c cs) z) \<le> ?k" .}
1.39 +    finally have "norm (poly (pCons c cs) z) \<le> ?k" .}
1.40    with kp show ?case by blast
1.41  qed
1.42
1.43 @@ -174,7 +176,9 @@
1.44  lemma psize_eq_0_iff [simp]: "psize p = 0 \<longleftrightarrow> p = 0"
1.45    unfolding psize_def by simp
1.46
1.47 -lemma poly_offset: "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q (x::complex) = poly p (a + x))"
1.48 +lemma poly_offset:
1.49 +  fixes p:: "('a::comm_ring_1) poly"
1.50 +  shows "\<exists> q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (a + x))"
1.51  proof (intro exI conjI)
1.52    show "psize (offset_poly p a) = psize p"
1.53      unfolding psize_def
1.54 @@ -331,8 +335,9 @@
1.55  text{* Polynomial is continuous. *}
1.56
1.57  lemma poly_cont:
1.58 +  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.59    assumes ep: "e > 0"
1.60 -  shows "\<exists>d >0. \<forall>w. 0 < cmod (w - z) \<and> cmod (w - z) < d \<longrightarrow> cmod (poly p w - poly p z) < e"
1.61 +  shows "\<exists>d >0. \<forall>w. 0 < norm (w - z) \<and> norm (w - z) < d \<longrightarrow> norm (poly p w - poly p z) < e"
1.62  proof-
1.63    obtain q where q: "degree q = degree p" "\<And>x. poly q x = poly p (z + x)"
1.64    proof
1.65 @@ -350,7 +355,7 @@
1.66    next
1.67      case (pCons c cs)
1.68      from poly_bound_exists[of 1 "cs"]
1.69 -    obtain m where m: "m > 0" "\<And>z. cmod z \<le> 1 \<Longrightarrow> cmod (poly cs z) \<le> m" by blast
1.70 +    obtain m where m: "m > 0" "\<And>z. norm z \<le> 1 \<Longrightarrow> norm (poly cs z) \<le> m" by blast
1.71      from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
1.72      have one0: "1 > (0::real)"  by arith
1.73      from real_lbound_gt_zero[OF one0 em0]
1.74 @@ -360,12 +365,12 @@
1.75      show ?case
1.76        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
1.77          fix d w
1.78 -        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "cmod (w-z) < d"
1.79 -        hence d1: "cmod (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.80 +        assume H: "d > 0" "d < 1" "d < e/m" "w\<noteq>z" "norm (w-z) < d"
1.81 +        hence d1: "norm (w-z) \<le> 1" "d \<ge> 0" by simp_all
1.82          from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
1.83 -        from H have th: "cmod (w-z) \<le> d" by simp
1.84 +        from H have th: "norm (w-z) \<le> d" by simp
1.85          from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
1.86 -        show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
1.87 +        show "norm (w - z) * norm (poly cs (w - z)) < e" by simp
1.88        qed
1.89      qed
1.90  qed
1.91 @@ -482,41 +487,42 @@
1.92  text {* Nonzero polynomial in z goes to infinity as z does. *}
1.93
1.94  lemma poly_infinity:
1.95 +  fixes p:: "('a::{comm_semiring_0,real_normed_div_algebra}) poly"
1.96    assumes ex: "p \<noteq> 0"
1.97 -  shows "\<exists>r. \<forall>z. r \<le> cmod z \<longrightarrow> d \<le> cmod (poly (pCons a p) z)"
1.98 +  shows "\<exists>r. \<forall>z. r \<le> norm z \<longrightarrow> d \<le> norm (poly (pCons a p) z)"
1.99  using ex
1.100  proof(induct p arbitrary: a d)
1.101    case (pCons c cs a d)
1.102    {assume H: "cs \<noteq> 0"
1.103 -    with pCons.hyps obtain r where r: "\<forall>z. r \<le> cmod z \<longrightarrow> d + cmod a \<le> cmod (poly (pCons c cs) z)" by blast
1.104 +    with pCons.hyps obtain r where r: "\<forall>z. r \<le> norm z \<longrightarrow> d + norm a \<le> norm (poly (pCons c cs) z)" by blast
1.105      let ?r = "1 + \<bar>r\<bar>"
1.106 -    {fix z assume h: "1 + \<bar>r\<bar> \<le> cmod z"
1.107 -      have r0: "r \<le> cmod z" using h by arith
1.108 +    {fix z::'a assume h: "1 + \<bar>r\<bar> \<le> norm z"
1.109 +      have r0: "r \<le> norm z" using h by arith
1.110        from r[rule_format, OF r0]
1.111 -      have th0: "d + cmod a \<le> 1 * cmod(poly (pCons c cs) z)" by arith
1.112 -      from h have z1: "cmod z \<ge> 1" by arith
1.113 +      have th0: "d + norm a \<le> 1 * norm(poly (pCons c cs) z)" by arith
1.114 +      from h have z1: "norm z \<ge> 1" by arith
1.115        from order_trans[OF th0 mult_right_mono[OF z1 norm_ge_zero[of "poly (pCons c cs) z"]]]
1.116 -      have th1: "d \<le> cmod(z * poly (pCons c cs) z) - cmod a"
1.117 +      have th1: "d \<le> norm(z * poly (pCons c cs) z) - norm a"
1.118          unfolding norm_mult by (simp add: algebra_simps)
1.119 -      from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
1.120 -      have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
1.121 +      from norm_diff_ineq[of "z * poly (pCons c cs) z" a]
1.122 +      have th2: "norm(z * poly (pCons c cs) z) - norm a \<le> norm (poly (pCons a (pCons c cs)) z)"
1.124 -      from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
1.125 +      from th1 th2 have "d \<le> norm (poly (pCons a (pCons c cs)) z)"  by arith}
1.126      hence ?case by blast}
1.127    moreover
1.128    {assume cs0: "\<not> (cs \<noteq> 0)"
1.129      with pCons.prems have c0: "c \<noteq> 0" by simp
1.130      from cs0 have cs0': "cs = 0" by simp
1.131 -    {fix z
1.132 -      assume h: "(\<bar>d\<bar> + cmod a) / cmod c \<le> cmod z"
1.133 -      from c0 have "cmod c > 0" by simp
1.134 -      from h c0 have th0: "\<bar>d\<bar> + cmod a \<le> cmod (z*c)"
1.135 +    {fix z::'a
1.136 +      assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
1.137 +      from c0 have "norm c > 0" by simp
1.138 +      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
1.139          by (simp add: field_simps norm_mult)
1.140        have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
1.141 -      from complex_mod_triangle_sub[of "z*c" a ]
1.142 -      have th1: "cmod (z * c) \<le> cmod (a + z * c) + cmod a"
1.143 +      from norm_diff_ineq[of "z*c" a ]
1.144 +      have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
1.146 -      from ath[OF th1 th0] have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"
1.147 +      from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
1.148          using cs0' by simp}
1.149      then have ?case  by blast}
1.150    ultimately show ?case by blast
1.151 @@ -850,7 +856,7 @@
1.152                from h have "poly p x = 0" by (subst s, simp)
1.153                with pq0 have "poly q x = 0" by blast
1.154                with r xa have "poly r x = 0"
1.156 +                by auto}
1.157              note impth = this
1.158              from IH[rule_format, OF dsn, of s r] impth ds0
1.159              have "s dvd (r ^ (degree s))" by blast
1.160 @@ -945,44 +951,38 @@
1.161  (* Arithmetic operations on multivariate polynomials.                        *)
1.162
1.163  lemma mpoly_base_conv:
1.164 -  "(0::complex) \<equiv> poly 0 x" "c \<equiv> poly [:c:] x" "x \<equiv> poly [:0,1:] x" by simp_all
1.165 +  fixes x :: "'a::comm_ring_1"
1.166 +  shows "0 = poly 0 x" "c = poly [:c:] x" "x = poly [:0,1:] x"
1.167 +  by simp_all
1.168
1.169  lemma mpoly_norm_conv:
1.170 -  "poly [:0:] (x::complex) \<equiv> poly 0 x" "poly [:poly 0 y:] x \<equiv> poly 0 x" by simp_all
1.171 +  fixes x :: "'a::comm_ring_1"
1.172 +  shows "poly [:0:] x = poly 0 x" "poly [:poly 0 y:] x = poly 0 x" by simp_all
1.173
1.174  lemma mpoly_sub_conv:
1.175 -  "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
1.176 +  fixes x :: "'a::comm_ring_1"
1.177 +  shows "poly p x - poly q x = poly p x + -1 * poly q x"
1.178    by simp
1.179
1.180 -lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
1.181 +lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = 0" by simp
1.182
1.183 -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
1.184 -
1.185 -lemma resolve_eq_raw:  "poly 0 x \<equiv> 0" "poly [:c:] x \<equiv> (c::complex)" by auto
1.186 +lemma poly_cancel_eq_conv:
1.187 +  fixes x :: "'a::field"
1.188 +  shows "x = 0 \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (y = 0) = (a * y - b * x = 0)"
1.189 +  by auto
1.190
1.192 -  fixes p q :: "complex poly"
1.193 +  fixes p:: "('a::comm_ring_1) poly"
1.194    assumes pq: "p dvd q"
1.195 -  shows "p dvd (pCons (0::complex) q)"
1.196 +shows "p dvd (pCons 0 q)"
1.197  proof-
1.198    have "pCons 0 q = q * [:0,1:]" by simp
1.199    then have "q dvd (pCons 0 q)" ..
1.200    with pq show ?thesis by (rule dvd_trans)
1.201  qed
1.202
1.204 -  fixes p q :: "complex poly"
1.205 -  assumes pq: "p dvd q"
1.206 -  shows "p dvd (smult a q)"
1.207 -proof-
1.208 -  have "smult a q = q * [:a:]" by simp
1.209 -  then have "q dvd smult a q" ..
1.210 -  with pq show ?thesis by (rule dvd_trans)
1.211 -qed
1.212 -
1.213 -
1.214  lemma poly_divides_conv0:
1.215 -  fixes p :: "complex poly"
1.216 +  fixes p:: "('a::field) poly"
1.217    assumes lgpq: "degree q < degree p" and lq:"p \<noteq> 0"
1.218    shows "p dvd q \<equiv> q = 0" (is "?lhs \<equiv> ?rhs")
1.219  proof-
1.220 @@ -1003,9 +1003,10 @@
1.221  qed
1.222
1.223  lemma poly_divides_conv1:
1.224 -  assumes a0: "a\<noteq> (0::complex)" and pp': "(p::complex poly) dvd p'"
1.225 +  fixes p:: "('a::field) poly"
1.226 +  assumes a0: "a\<noteq> 0" and pp': "p dvd p'"
1.227    and qrp': "smult a q - p' \<equiv> r"
1.228 -  shows "p dvd q \<equiv> p dvd (r::complex poly)" (is "?lhs \<equiv> ?rhs")
1.229 +  shows "p dvd q \<equiv> p dvd r" (is "?lhs \<equiv> ?rhs")
1.230  proof-
1.231    {
1.232    from pp' obtain t where t: "p' = p * t" ..
1.233 @@ -1068,8 +1069,9 @@
1.234    thus "p dvd (q ^ n) \<longleftrightarrow> p dvd r" by simp
1.235  qed
1.236
1.237 -lemma complex_entire: "(z::complex) \<noteq> 0 \<and> w \<noteq> 0 \<equiv> z*w \<noteq> 0" by simp
1.238 -
1.239 -lemma poly_const_conv: "poly [:c:] (x::complex) = y \<longleftrightarrow> c = y" by simp
1.240 +lemma poly_const_conv:
1.241 +  fixes x :: "'a::comm_ring_1"
1.242 +  shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
1.243
1.244  end
1.245 +
```