# HG changeset patch # User huffman # Date 1231778767 28800 # Node ID b0f586f38dd7c56095603885ce6a0a799a2b341b # Parent de4f26f59135c0f0d4f1b5a02e359a5865580d68 add recursion combinator poly_rec; define poly function using poly_rec diff -r de4f26f59135 -r b0f586f38dd7 src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Mon Jan 12 08:15:07 2009 -0800 +++ b/src/HOL/Polynomial.thy Mon Jan 12 08:46:07 2009 -0800 @@ -196,6 +196,28 @@ qed +subsection {* Recursion combinator for polynomials *} + +function + poly_rec :: "'b \ ('a::zero \ 'a poly \ 'b \ 'b) \ 'a poly \ 'b" +where + poly_rec_pCons_eq_if [simp del]: + "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)" +by (case_tac x, rename_tac q, case_tac q, auto) + +termination poly_rec +by (relation "measure (degree \ snd \ snd)", simp) + (simp add: degree_pCons_eq) + +lemma poly_rec_0: + "f 0 0 z = z \ poly_rec z f 0 = z" + using poly_rec_pCons_eq_if [of z f 0 0] by simp + +lemma poly_rec_pCons: + "f 0 0 z = z \ poly_rec z f (pCons a p) = f a p (poly_rec z f p)" + by (simp add: poly_rec_pCons_eq_if poly_rec_0) + + subsection {* Monomials *} definition @@ -885,22 +907,21 @@ subsection {* Evaluation of polynomials *} definition - poly :: "'a::{comm_semiring_1,recpower} poly \ 'a \ 'a" where - "poly p = (\x. \n\degree p. coeff p n * x ^ n)" + poly :: "'a::comm_semiring_0 poly \ 'a \ 'a" where + "poly = poly_rec (\x. 0) (\a p f x. a + x * f x)" lemma poly_0 [simp]: "poly 0 x = 0" - unfolding poly_def by simp + unfolding poly_def by (simp add: poly_rec_0) lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" - unfolding poly_def - by (simp add: degree_pCons_eq_if setsum_atMost_Suc_shift power_Suc - setsum_left_distrib setsum_right_distrib mult_ac - del: setsum_atMost_Suc) + unfolding poly_def by (simp add: poly_rec_pCons) lemma poly_1 [simp]: "poly 1 x = 1" unfolding one_poly_def by simp -lemma poly_monom: "poly (monom a n) x = a * x ^ n" +lemma poly_monom: + fixes a x :: "'a::{comm_semiring_1,recpower}" + shows "poly (monom a n) x = a * x ^ n" by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" @@ -909,12 +930,12 @@ done lemma poly_minus [simp]: - fixes x :: "'a::{comm_ring_1,recpower}" + fixes x :: "'a::comm_ring" shows "poly (- p) x = - poly p x" by (induct p, simp_all) lemma poly_diff [simp]: - fixes x :: "'a::{comm_ring_1,recpower}" + fixes x :: "'a::comm_ring" shows "poly (p - q) x = poly p x - poly q x" by (simp add: diff_minus)