# HG changeset patch
# User huffman
# Date 1231790994 28800
# Node ID ad87e5d1488bdb978a2a14dd406a44e3ee9c2a59
# Parent  2eadbc24de8c6b54c7c011f240adf07280a657d7
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]

diff -r 2eadbc24de8c -r ad87e5d1488b src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Mon Jan 12 10:09:23 2009 -0800
+++ b/src/HOL/Polynomial.thy	Mon Jan 12 12:09:54 2009 -0800
@@ -135,7 +135,7 @@
 apply (rule degree_le, simp add: coeff_pCons split: nat.split)
 done
 
-lemma degree_pCons_eq_if:
+lemma degree_pCons_eq_if [simp]:
   "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
 apply (cases "p = 0", simp_all)
 apply (rule order_antisym [OF _ le0])
@@ -760,7 +760,7 @@
     also have "\<dots> \<le> degree y"
     proof (rule min_max.le_supI)
       show "degree (pCons a r) \<le> degree y"
-        using r by (auto simp add: degree_pCons_eq_if)
+        using r by auto
       show "degree (smult b y) \<le> degree y"
         by (rule degree_smult_le)
     qed
@@ -991,6 +991,14 @@
   unfolding synthetic_div_def
   by (simp add: split_def snd_synthetic_divmod)
 
+lemma synthetic_div_eq_0_iff:
+  "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0"
+  by (induct p, simp, case_tac p, simp)
+
+lemma degree_synthetic_div:
+  "degree (synthetic_div p c) = degree p - 1"
+  by (induct p, simp, simp add: synthetic_div_eq_0_iff)
+
 lemma synthetic_div_correct:
   "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
   by (induct p) simp_all
@@ -1011,4 +1019,23 @@
   using synthetic_div_correct [of p c]
   by (simp add: group_simps)
 
+lemma poly_eq_0_iff_dvd:
+  fixes c :: "'a::idom"
+  shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
+proof
+  assume "poly p c = 0"
+  with synthetic_div_correct' [of c p]
+  have "p = [:-c, 1:] * synthetic_div p c" by simp
+  then show "[:-c, 1:] dvd p" ..
+next
+  assume "[:-c, 1:] dvd p"
+  then obtain k where "p = [:-c, 1:] * k" by (rule dvdE)
+  then show "poly p c = 0" by simp
+qed
+
+lemma dvd_iff_poly_eq_0:
+  fixes c :: "'a::idom"
+  shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
+  by (simp add: poly_eq_0_iff_dvd)
+
 end