src/HOL/Polynomial.thy
 changeset 29460 ad87e5d1488b parent 29457 2eadbc24de8c child 29462 dc97c6188a7a
```     1.1 --- a/src/HOL/Polynomial.thy	Mon Jan 12 10:09:23 2009 -0800
1.2 +++ b/src/HOL/Polynomial.thy	Mon Jan 12 12:09:54 2009 -0800
1.3 @@ -135,7 +135,7 @@
1.4  apply (rule degree_le, simp add: coeff_pCons split: nat.split)
1.5  done
1.6
1.7 -lemma degree_pCons_eq_if:
1.8 +lemma degree_pCons_eq_if [simp]:
1.9    "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
1.10  apply (cases "p = 0", simp_all)
1.11  apply (rule order_antisym [OF _ le0])
1.12 @@ -760,7 +760,7 @@
1.13      also have "\<dots> \<le> degree y"
1.14      proof (rule min_max.le_supI)
1.15        show "degree (pCons a r) \<le> degree y"
1.16 -        using r by (auto simp add: degree_pCons_eq_if)
1.17 +        using r by auto
1.18        show "degree (smult b y) \<le> degree y"
1.19          by (rule degree_smult_le)
1.20      qed
1.21 @@ -991,6 +991,14 @@
1.22    unfolding synthetic_div_def
1.23    by (simp add: split_def snd_synthetic_divmod)
1.24
1.25 +lemma synthetic_div_eq_0_iff:
1.26 +  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
1.27 +  by (induct p, simp, case_tac p, simp)
1.28 +
1.29 +lemma degree_synthetic_div:
1.30 +  "degree (synthetic_div p c) = degree p - 1"
1.31 +  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
1.32 +
1.33  lemma synthetic_div_correct:
1.34    "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
1.35    by (induct p) simp_all
1.36 @@ -1011,4 +1019,23 @@
1.37    using synthetic_div_correct [of p c]
1.38    by (simp add: group_simps)
1.39
1.40 +lemma poly_eq_0_iff_dvd:
1.41 +  fixes c :: "'a::idom"
1.42 +  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
1.43 +proof
1.44 +  assume "poly p c = 0"
1.45 +  with synthetic_div_correct' [of c p]
1.46 +  have "p = [:-c, 1:] * synthetic_div p c" by simp
1.47 +  then show "[:-c, 1:] dvd p" ..
1.48 +next
1.49 +  assume "[:-c, 1:] dvd p"
1.50 +  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
1.51 +  then show "poly p c = 0" by simp
1.52 +qed
1.53 +
1.54 +lemma dvd_iff_poly_eq_0:
1.55 +  fixes c :: "'a::idom"
1.56 +  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
1.57 +  by (simp add: poly_eq_0_iff_dvd)
1.58 +
1.59  end
```