author huffman Mon, 12 Jan 2009 09:35:15 -0800 changeset 29456 3f8b85444512 parent 29455 0139c9a01ca4 child 29457 2eadbc24de8c
add synthetic division algorithm for polynomials
 src/HOL/Polynomial.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Polynomial.thy	Mon Jan 12 09:04:25 2009 -0800
+++ b/src/HOL/Polynomial.thy	Mon Jan 12 09:35:15 2009 -0800
@@ -955,4 +955,44 @@
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
by (induct p, simp_all, simp add: ring_simps)

+
+subsection {* Synthetic division *}
+
+definition
+  synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a"
+where
+  "synthetic_divmod p c =
+    poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p"
+
+definition
+  synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly"
+where
+  "synthetic_div p c = fst (synthetic_divmod p c)"
+
+lemma synthetic_divmod_0 [simp]:
+  "synthetic_divmod 0 c = (0, 0)"
+  unfolding synthetic_divmod_def
+
+lemma synthetic_divmod_pCons [simp]:
+  "synthetic_divmod (pCons a p) c =
+    (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
+  unfolding synthetic_divmod_def
+
+lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
+  by (induct p, simp, simp add: split_def)
+
+lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
+  unfolding synthetic_div_def by simp
+
+lemma synthetic_div_pCons [simp]:
+  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
+  unfolding synthetic_div_def
+  by (simp add: split_def snd_synthetic_divmod)
+
+lemma synthetic_div:
+  "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)"
+  by (induct p) simp_all
+
end```