192 then have "P (pCons a q)" |
192 then have "P (pCons a q)" |
193 by (rule pCons) |
193 by (rule pCons) |
194 then show ?case |
194 then show ?case |
195 using `p = pCons a q` by simp |
195 using `p = pCons a q` by simp |
196 qed |
196 qed |
|
197 |
|
198 |
|
199 subsection {* Recursion combinator for polynomials *} |
|
200 |
|
201 function |
|
202 poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b" |
|
203 where |
|
204 poly_rec_pCons_eq_if [simp del]: |
|
205 "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)" |
|
206 by (case_tac x, rename_tac q, case_tac q, auto) |
|
207 |
|
208 termination poly_rec |
|
209 by (relation "measure (degree \<circ> snd \<circ> snd)", simp) |
|
210 (simp add: degree_pCons_eq) |
|
211 |
|
212 lemma poly_rec_0: |
|
213 "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z" |
|
214 using poly_rec_pCons_eq_if [of z f 0 0] by simp |
|
215 |
|
216 lemma poly_rec_pCons: |
|
217 "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)" |
|
218 by (simp add: poly_rec_pCons_eq_if poly_rec_0) |
197 |
219 |
198 |
220 |
199 subsection {* Monomials *} |
221 subsection {* Monomials *} |
200 |
222 |
201 definition |
223 definition |
883 |
905 |
884 |
906 |
885 subsection {* Evaluation of polynomials *} |
907 subsection {* Evaluation of polynomials *} |
886 |
908 |
887 definition |
909 definition |
888 poly :: "'a::{comm_semiring_1,recpower} poly \<Rightarrow> 'a \<Rightarrow> 'a" where |
910 poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where |
889 "poly p = (\<lambda>x. \<Sum>n\<le>degree p. coeff p n * x ^ n)" |
911 "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)" |
890 |
912 |
891 lemma poly_0 [simp]: "poly 0 x = 0" |
913 lemma poly_0 [simp]: "poly 0 x = 0" |
892 unfolding poly_def by simp |
914 unfolding poly_def by (simp add: poly_rec_0) |
893 |
915 |
894 lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" |
916 lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" |
895 unfolding poly_def |
917 unfolding poly_def by (simp add: poly_rec_pCons) |
896 by (simp add: degree_pCons_eq_if setsum_atMost_Suc_shift power_Suc |
|
897 setsum_left_distrib setsum_right_distrib mult_ac |
|
898 del: setsum_atMost_Suc) |
|
899 |
918 |
900 lemma poly_1 [simp]: "poly 1 x = 1" |
919 lemma poly_1 [simp]: "poly 1 x = 1" |
901 unfolding one_poly_def by simp |
920 unfolding one_poly_def by simp |
902 |
921 |
903 lemma poly_monom: "poly (monom a n) x = a * x ^ n" |
922 lemma poly_monom: |
|
923 fixes a x :: "'a::{comm_semiring_1,recpower}" |
|
924 shows "poly (monom a n) x = a * x ^ n" |
904 by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) |
925 by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) |
905 |
926 |
906 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
927 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
907 apply (induct p arbitrary: q, simp) |
928 apply (induct p arbitrary: q, simp) |
908 apply (case_tac q, simp, simp add: ring_simps) |
929 apply (case_tac q, simp, simp add: ring_simps) |
909 done |
930 done |
910 |
931 |
911 lemma poly_minus [simp]: |
932 lemma poly_minus [simp]: |
912 fixes x :: "'a::{comm_ring_1,recpower}" |
933 fixes x :: "'a::comm_ring" |
913 shows "poly (- p) x = - poly p x" |
934 shows "poly (- p) x = - poly p x" |
914 by (induct p, simp_all) |
935 by (induct p, simp_all) |
915 |
936 |
916 lemma poly_diff [simp]: |
937 lemma poly_diff [simp]: |
917 fixes x :: "'a::{comm_ring_1,recpower}" |
938 fixes x :: "'a::comm_ring" |
918 shows "poly (p - q) x = poly p x - poly q x" |
939 shows "poly (p - q) x = poly p x - poly q x" |
919 by (simp add: diff_minus) |
940 by (simp add: diff_minus) |
920 |
941 |
921 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
942 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
922 by (cases "finite A", induct set: finite, simp_all) |
943 by (cases "finite A", induct set: finite, simp_all) |