src/HOL/Library/Polynomial.thy
changeset 62065 1546a042e87b
parent 61945 1135b8de26c3
child 62067 0fd850943901
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 15:38:37 2016 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 17:54:10 2016 +0100
     1.3 @@ -281,7 +281,10 @@
     1.4  lemma Poly_eq_0:
     1.5    "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
     1.6    by (induct as) (auto simp add: Cons_replicate_eq)
     1.7 -
     1.8 +  
     1.9 +lemma degree_Poly: "degree (Poly xs) \<le> length xs"
    1.10 +  by (induction xs) simp_all
    1.11 +  
    1.12  definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
    1.13  where
    1.14    "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
    1.15 @@ -311,6 +314,14 @@
    1.16      by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
    1.17  qed
    1.18  
    1.19 +lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
    1.20 +  by (simp add: coeffs_def)
    1.21 +  
    1.22 +lemma coeffs_nth:
    1.23 +  assumes "p \<noteq> 0" "n \<le> degree p"
    1.24 +  shows   "coeffs p ! n = coeff p n"
    1.25 +  using assms unfolding coeffs_def by (auto simp del: upt_Suc)
    1.26 +
    1.27  lemma not_0_cCons_eq [simp]:
    1.28    "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
    1.29    by (simp add: cCons_def)
    1.30 @@ -450,6 +461,25 @@
    1.31    "poly (pCons a p) x = a + x * poly p x"
    1.32    by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)
    1.33  
    1.34 +lemma poly_altdef: 
    1.35 +  "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
    1.36 +proof (induction p rule: pCons_induct)
    1.37 +  case (pCons a p)
    1.38 +    show ?case
    1.39 +    proof (cases "p = 0")
    1.40 +      case False
    1.41 +      let ?p' = "pCons a p"
    1.42 +      note poly_pCons[of a p x]
    1.43 +      also note pCons.IH
    1.44 +      also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
    1.45 +                 coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
    1.46 +          by (simp add: field_simps setsum_right_distrib coeff_pCons)
    1.47 +      also note setsum_atMost_Suc_shift[symmetric]
    1.48 +      also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
    1.49 +      finally show ?thesis .
    1.50 +   qed simp
    1.51 +qed simp
    1.52 +
    1.53  
    1.54  subsection \<open>Monomials\<close>
    1.55  
    1.56 @@ -500,7 +530,7 @@
    1.57    by (cases "a = 0", simp_all)
    1.58      (induct n, simp_all add: mult.left_commute poly_def)
    1.59  
    1.60 -
    1.61 +    
    1.62  subsection \<open>Addition and subtraction\<close>
    1.63  
    1.64  instantiation poly :: (comm_monoid_add) comm_monoid_add
    1.65 @@ -714,6 +744,9 @@
    1.66  lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
    1.67    by (induct A rule: infinite_finite_induct) simp_all
    1.68  
    1.69 +lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
    1.70 +  by (induction xs) (simp_all add: monom_0 monom_Suc)
    1.71 +
    1.72  
    1.73  subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>
    1.74  
    1.75 @@ -924,6 +957,28 @@
    1.76    shows "poly (p ^ n) x = poly p x ^ n"
    1.77    by (induct n) simp_all
    1.78  
    1.79 +  
    1.80 +subsection \<open>Conversions from natural numbers\<close>
    1.81 +
    1.82 +lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
    1.83 +proof (induction n)
    1.84 +  case (Suc n)
    1.85 +  hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" 
    1.86 +    by simp
    1.87 +  also have "(of_nat n :: 'a poly) = [: of_nat n :]" 
    1.88 +    by (subst Suc) (rule refl)
    1.89 +  also have "1 = [:1:]" by (simp add: one_poly_def)
    1.90 +  finally show ?case by (subst (asm) add_pCons) simp
    1.91 +qed simp
    1.92 +
    1.93 +lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
    1.94 +  by (simp add: of_nat_poly)
    1.95 +
    1.96 +lemma degree_numeral [simp]: "degree (numeral n) = 0"
    1.97 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
    1.98 +
    1.99 +lemma numeral_poly: "numeral n = [:numeral n:]"
   1.100 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   1.101  
   1.102  subsection \<open>Lemmas about divisibility\<close>
   1.103  
   1.104 @@ -1787,6 +1842,9 @@
   1.105  apply (metis dvd_power dvd_trans order_1)
   1.106  done
   1.107  
   1.108 +lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
   1.109 +  by (subst (asm) order_root) auto
   1.110 +
   1.111  
   1.112  subsection \<open>GCD of polynomials\<close>
   1.113  
   1.114 @@ -1919,6 +1977,75 @@
   1.115    by (simp add: gcd_poly.simps)
   1.116  
   1.117  
   1.118 +subsection \<open>Additional induction rules on polynomials\<close>
   1.119 +
   1.120 +text \<open>
   1.121 +  An induction rule for induction over the roots of a polynomial with a certain property. 
   1.122 +  (e.g. all positive roots)
   1.123 +\<close>
   1.124 +lemma poly_root_induct [case_names 0 no_roots root]:
   1.125 +  fixes p :: "'a :: idom poly"
   1.126 +  assumes "Q 0"
   1.127 +  assumes "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
   1.128 +  assumes "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
   1.129 +  shows   "Q p"
   1.130 +proof (induction "degree p" arbitrary: p rule: less_induct)
   1.131 +  case (less p)
   1.132 +  show ?case
   1.133 +  proof (cases "p = 0")
   1.134 +    assume nz: "p \<noteq> 0"
   1.135 +    show ?case
   1.136 +    proof (cases "\<exists>a. P a \<and> poly p a = 0")
   1.137 +      case False
   1.138 +      thus ?thesis by (intro assms(2)) blast
   1.139 +    next
   1.140 +      case True
   1.141 +      then obtain a where a: "P a" "poly p a = 0" 
   1.142 +        by blast
   1.143 +      hence "-[:-a, 1:] dvd p" 
   1.144 +        by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
   1.145 +      then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
   1.146 +      with nz have q_nz: "q \<noteq> 0" by auto
   1.147 +      have "degree p = Suc (degree q)"
   1.148 +        by (subst q, subst degree_mult_eq) (simp_all add: q_nz)
   1.149 +      hence "Q q" by (intro less) simp
   1.150 +      from a(1) and this have "Q ([:a, -1:] * q)" 
   1.151 +        by (rule assms(3))
   1.152 +      with q show ?thesis by simp
   1.153 +    qed
   1.154 +  qed (simp add: assms(1))
   1.155 +qed
   1.156 +
   1.157 +lemma dropWhile_replicate_append: 
   1.158 +  "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys"
   1.159 +  by (induction n) simp_all
   1.160 +
   1.161 +lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
   1.162 +  by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
   1.163 +
   1.164 +text \<open>
   1.165 +  An induction rule for simultaneous induction over two polynomials, 
   1.166 +  prepending one coefficient in each step.
   1.167 +\<close>
   1.168 +lemma poly_induct2 [case_names 0 pCons]:
   1.169 +  assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
   1.170 +  shows   "P p q"
   1.171 +proof -
   1.172 +  def n \<equiv> "max (length (coeffs p)) (length (coeffs q))"
   1.173 +  def xs \<equiv> "coeffs p @ (replicate (n - length (coeffs p)) 0)"
   1.174 +  def ys \<equiv> "coeffs q @ (replicate (n - length (coeffs q)) 0)"
   1.175 +  have "length xs = length ys" 
   1.176 +    by (simp add: xs_def ys_def n_def)
   1.177 +  hence "P (Poly xs) (Poly ys)" 
   1.178 +    by (induction rule: list_induct2) (simp_all add: assms)
   1.179 +  also have "Poly xs = p" 
   1.180 +    by (simp add: xs_def Poly_append_replicate_0)
   1.181 +  also have "Poly ys = q" 
   1.182 +    by (simp add: ys_def Poly_append_replicate_0)
   1.183 +  finally show ?thesis .
   1.184 +qed
   1.185 +
   1.186 +
   1.187  subsection \<open>Composition of polynomials\<close>
   1.188  
   1.189  definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   1.190 @@ -1945,6 +2072,212 @@
   1.191  apply (rule order_trans [OF degree_mult_le], simp)
   1.192  done
   1.193  
   1.194 +lemma pcompose_add:
   1.195 +  fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly"
   1.196 +  shows "pcompose (p + q) r = pcompose p r + pcompose q r"
   1.197 +proof (induction p q rule: poly_induct2)
   1.198 +  case (pCons a p b q)
   1.199 +  have "pcompose (pCons a p + pCons b q) r = 
   1.200 +          [:a + b:] + r * pcompose p r + r * pcompose q r"
   1.201 +    by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
   1.202 +  also have "[:a + b:] = [:a:] + [:b:]" by simp
   1.203 +  also have "\<dots> + r * pcompose p r + r * pcompose q r = 
   1.204 +                 pcompose (pCons a p) r + pcompose (pCons b q) r"
   1.205 +    by (simp only: pcompose_pCons add_ac)
   1.206 +  finally show ?case .
   1.207 +qed simp
   1.208 +
   1.209 +lemma pcompose_minus:
   1.210 +  fixes p r :: "'a :: comm_ring poly"
   1.211 +  shows "pcompose (-p) r = -pcompose p r"
   1.212 +  by (induction p) (simp_all add: pcompose_pCons)
   1.213 +
   1.214 +lemma pcompose_diff:
   1.215 +  fixes p q r :: "'a :: comm_ring poly"
   1.216 +  shows "pcompose (p - q) r = pcompose p r - pcompose q r"
   1.217 +  using pcompose_add[of p "-q"] by (simp add: pcompose_minus)
   1.218 +
   1.219 +lemma pcompose_smult:
   1.220 +  fixes p r :: "'a :: comm_semiring_0 poly"
   1.221 +  shows "pcompose (smult a p) r = smult a (pcompose p r)"
   1.222 +  by (induction p) 
   1.223 +     (simp_all add: pcompose_pCons pcompose_add smult_add_right)
   1.224 +
   1.225 +lemma pcompose_mult:
   1.226 +  fixes p q r :: "'a :: comm_semiring_0 poly"
   1.227 +  shows "pcompose (p * q) r = pcompose p r * pcompose q r"
   1.228 +  by (induction p arbitrary: q)
   1.229 +     (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
   1.230 +
   1.231 +lemma pcompose_assoc: 
   1.232 +  "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) =
   1.233 +     pcompose (pcompose p q) r"
   1.234 +  by (induction p arbitrary: q) 
   1.235 +     (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
   1.236 +
   1.237 +
   1.238 +(* The remainder of this section and the next were contributed by Wenda Li *)
   1.239 +
   1.240 +lemma degree_mult_eq_0:
   1.241 +  fixes p q:: "'a :: idom poly"
   1.242 +  shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
   1.243 +by (auto simp add:degree_mult_eq)
   1.244 +
   1.245 +lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) 
   1.246 +
   1.247 +lemma pcompose_0':"pcompose p 0=[:coeff p 0:]"
   1.248 +  apply (induct p)
   1.249 +  apply (auto simp add:pcompose_pCons)
   1.250 +done
   1.251 +
   1.252 +lemma degree_pcompose:
   1.253 +  fixes p q:: "'a::idom poly"
   1.254 +  shows "degree(pcompose p q) = degree p * degree q"
   1.255 +proof (induct p)
   1.256 +  case 0
   1.257 +  thus ?case by auto
   1.258 +next
   1.259 +  case (pCons a p)
   1.260 +  have "degree (q * pcompose p q) = 0 \<Longrightarrow> ?case" 
   1.261 +    proof (cases "p=0")
   1.262 +      case True
   1.263 +      thus ?thesis by auto
   1.264 +    next
   1.265 +      case False assume "degree (q * pcompose p q) = 0"
   1.266 +      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
   1.267 +      moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0` 
   1.268 +        proof -
   1.269 +          assume "pcompose p q=0" "degree q\<noteq>0"
   1.270 +          hence "degree p=0" using pCons.hyps(2) by auto
   1.271 +          then obtain a1 where "p=[:a1:]"
   1.272 +            by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
   1.273 +          thus False using `pcompose p q=0` `p\<noteq>0` by auto
   1.274 +        qed
   1.275 +      ultimately have "degree (pCons a p) * degree q=0" by auto
   1.276 +      moreover have "degree (pcompose (pCons a p) q) = 0" 
   1.277 +        proof -
   1.278 +          have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
   1.279 +            using `degree (q * pcompose p q) = 0` by simp
   1.280 +          also have "... \<ge> degree ([:a:] + q * pcompose p q)"
   1.281 +            by (rule degree_add_le_max)
   1.282 +          finally show ?thesis by (auto simp add:pcompose_pCons)
   1.283 +        qed
   1.284 +      ultimately show ?thesis by simp
   1.285 +    qed
   1.286 +  moreover have "degree (q * pcompose p q)>0 \<Longrightarrow> ?case" 
   1.287 +    proof -
   1.288 +      assume asm:"0 < degree (q * pcompose p q)"
   1.289 +      hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto
   1.290 +      have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"
   1.291 +        unfolding pcompose_pCons
   1.292 +        using degree_add_eq_right[of "[:a:]" ] asm by auto       
   1.293 +      thus ?thesis 
   1.294 +        using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
   1.295 +    qed
   1.296 +  ultimately show ?case by blast
   1.297 +qed
   1.298 +
   1.299 +lemma pcompose_eq_0:
   1.300 +  fixes p q:: "'a::idom poly"
   1.301 +  assumes "pcompose p q=0" "degree q>0" 
   1.302 +  shows "p=0"
   1.303 +proof -
   1.304 +  have "degree p=0" using assms degree_pcompose[of p q] by auto
   1.305 +  then obtain a where "p=[:a:]" 
   1.306 +    by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
   1.307 +  hence "a=0" using assms(1) by auto
   1.308 +  thus ?thesis using `p=[:a:]` by simp
   1.309 +qed
   1.310 +
   1.311 +
   1.312 +section{*lead coefficient*}
   1.313 +
   1.314 +definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
   1.315 +  "lead_coeff p= coeff p (degree p)"
   1.316 +
   1.317 +lemma lead_coeff_pCons[simp]:
   1.318 +    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
   1.319 +    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
   1.320 +unfolding lead_coeff_def by auto
   1.321 +
   1.322 +lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
   1.323 +  unfolding lead_coeff_def by auto
   1.324 +
   1.325 +lemma lead_coeff_mult:
   1.326 +   fixes p q::"'a ::idom poly"
   1.327 +   shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
   1.328 +by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
   1.329 +
   1.330 +lemma lead_coeff_add_le:
   1.331 +  assumes "degree p < degree q"
   1.332 +  shows "lead_coeff (p+q) = lead_coeff q" 
   1.333 +using assms unfolding lead_coeff_def
   1.334 +by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
   1.335 +
   1.336 +lemma lead_coeff_minus:
   1.337 +  "lead_coeff (-p) = - lead_coeff p"
   1.338 +by (metis coeff_minus degree_minus lead_coeff_def)
   1.339 +
   1.340 +
   1.341 +lemma lead_coeff_comp:
   1.342 +  fixes p q:: "'a::idom poly"
   1.343 +  assumes "degree q > 0" 
   1.344 +  shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
   1.345 +proof (induct p)
   1.346 +  case 0
   1.347 +  thus ?case unfolding lead_coeff_def by auto
   1.348 +next
   1.349 +  case (pCons a p)
   1.350 +  have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
   1.351 +    proof -
   1.352 +      assume "degree ( q * pcompose p q) = 0"
   1.353 +      hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
   1.354 +      hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp
   1.355 +      thus ?thesis by auto
   1.356 +    qed
   1.357 +  moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case" 
   1.358 +    proof -
   1.359 +      assume "degree ( q * pcompose p q) > 0"
   1.360 +      hence "lead_coeff (pcompose (pCons a p) q) =lead_coeff ( q * pcompose p q)"
   1.361 +        by (auto simp add:pcompose_pCons lead_coeff_add_le)
   1.362 +      also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
   1.363 +        using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
   1.364 +      also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"
   1.365 +        by auto
   1.366 +      finally show ?thesis by auto
   1.367 +    qed
   1.368 +  ultimately show ?case by blast
   1.369 +qed
   1.370 +
   1.371 +lemma lead_coeff_smult: 
   1.372 +  "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"
   1.373 +proof -
   1.374 +  have "smult c p = [:c:] * p" by simp
   1.375 +  also have "lead_coeff \<dots> = c * lead_coeff p" 
   1.376 +    by (subst lead_coeff_mult) simp_all
   1.377 +  finally show ?thesis .
   1.378 +qed
   1.379 +
   1.380 +lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   1.381 +  by (simp add: lead_coeff_def)
   1.382 +
   1.383 +lemma lead_coeff_of_nat [simp]:
   1.384 +  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
   1.385 +  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
   1.386 +
   1.387 +lemma lead_coeff_numeral [simp]: 
   1.388 +  "lead_coeff (numeral n) = numeral n"
   1.389 +  unfolding lead_coeff_def
   1.390 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
   1.391 +
   1.392 +lemma lead_coeff_power: 
   1.393 +  "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"
   1.394 +  by (induction n) (simp_all add: lead_coeff_mult)
   1.395 +
   1.396 +lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
   1.397 +  by (simp add: lead_coeff_def)
   1.398 +  
   1.399 +  
   1.400  
   1.401  no_notation cCons (infixr "##" 65)
   1.402