generalised some results using type classes
authorpaulson <lp15@cam.ac.uk>
Tue Feb 25 17:06:17 2014 +0000 (2014-02-25)
changeset 5573581ba62493610
parent 55734 3f5b2745d659
child 55736 f1ed1e9cd080
generalised some results using type classes
src/HOL/Library/Fundamental_Theorem_Algebra.thy
     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.123          by (simp add: algebra_simps)
   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.145          by (simp add: algebra_simps)
   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.155 -                by (auto simp add: uminus_add_conv_diff)}
   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.191  lemma poly_divides_pad_rule:
   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.203 -lemma poly_divides_pad_const_rule:
   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 +