# HG changeset patch
# User huffman
# Date 1231827395 28800
# Node ID dc97c6188a7a806cba8482d78053eec348b1f41b
# Parent  7c1841a7bdf4c33c04f4952b2b1c1462c6f57b58
add lemmas poly_power, poly_roots_finite

diff -r 7c1841a7bdf4 -r dc97c6188a7a src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Mon Jan 12 12:10:41 2009 -0800
+++ b/src/HOL/Polynomial.thy	Mon Jan 12 22:16:35 2009 -0800
@@ -955,6 +955,11 @@
 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
   by (induct p, simp_all, simp add: ring_simps)
 
+lemma poly_power [simp]:
+  fixes p :: "'a::{comm_semiring_1,recpower} poly"
+  shows "poly (p ^ n) x = poly p x ^ n"
+  by (induct n, simp, simp add: power_Suc)
+
 
 subsection {* Synthetic division *}
 
@@ -1038,4 +1043,35 @@
   shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
   by (simp add: poly_eq_0_iff_dvd)
 
+lemma poly_roots_finite:
+  fixes p :: "'a::idom poly"
+  shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
+proof (induct n \<equiv> "degree p" arbitrary: p)
+  case (0 p)
+  then obtain a where "a \<noteq> 0" and "p = [:a:]"
+    by (cases p, simp split: if_splits)
+  then show "finite {x. poly p x = 0}" by simp
+next
+  case (Suc n p)
+  show "finite {x. poly p x = 0}"
+  proof (cases "\<exists>x. poly p x = 0")
+    case False
+    then show "finite {x. poly p x = 0}" by simp
+  next
+    case True
+    then obtain a where "poly p a = 0" ..
+    then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd)
+    then obtain k where k: "p = [:-a, 1:] * k" ..
+    with `p \<noteq> 0` have "k \<noteq> 0" by auto
+    with k have "degree p = Suc (degree k)"
+      by (simp add: degree_mult_eq del: mult_pCons_left)
+    with `Suc n = degree p` have "n = degree k" by simp
+    with `k \<noteq> 0` have "finite {x. poly k x = 0}" by (rule Suc.hyps)
+    then have "finite (insert a {x. poly k x = 0})" by simp
+    then show "finite {x. poly p x = 0}"
+      by (simp add: k uminus_add_conv_diff Collect_disj_eq
+               del: mult_pCons_left)
+  qed
+qed
+
 end