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.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.63
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.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.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.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.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.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.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.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.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.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.313 +
1.314 +definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
1.315 +  "lead_coeff p= coeff p (degree p)"
1.316 +
1.319 +    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
1.321 +
1.323 +  unfolding lead_coeff_def by auto
1.324 +
1.326 +   fixes p q::"'a ::idom poly"
1.329 +
1.331 +  assumes "degree p < degree q"
1.335 +
1.338 +by (metis coeff_minus degree_minus lead_coeff_def)
1.339 +
1.340 +
1.342 +  fixes p q:: "'a::idom poly"
1.343 +  assumes "degree q > 0"
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.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.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.376 +    by (subst lead_coeff_mult) simp_all
1.377 +  finally show ?thesis .
1.378 +qed
1.379 +
1.382 +
1.384 +  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
1.386 +
1.388 +  "lead_coeff (numeral n) = numeral n"
1.390 +  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
1.391 +