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