# HG changeset patch # User huffman # Date 1231781715 28800 # Node ID 3f8b85444512e7171e103afa7c8f01fda8085260 # Parent 0139c9a01ca44c1b88fb410f0ec59c668800791e add synthetic division algorithm for polynomials diff -r 0139c9a01ca4 -r 3f8b85444512 src/HOL/Polynomial.thy --- 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 \ 'a \ 'a poly \ 'a" +where + "synthetic_divmod p c = + poly_rec (0, 0) (\a p (q, r). (pCons r q, a + c * r)) p" + +definition + synthetic_div :: "'a::comm_semiring_0 poly \ 'a \ '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 + by (simp add: poly_rec_0) + +lemma synthetic_divmod_pCons [simp]: + "synthetic_divmod (pCons a p) c = + (\(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" + unfolding synthetic_divmod_def + by (simp add: poly_rec_pCons) + +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