equal
deleted
inserted
replaced
76 lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)" |
76 lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)" |
77 unfolding fps_uminus_def by simp |
77 unfolding fps_uminus_def by simp |
78 |
78 |
79 instantiation fps :: ("{comm_monoid_add, times}") times |
79 instantiation fps :: ("{comm_monoid_add, times}") times |
80 begin |
80 begin |
81 definition fps_times_def: "( * ) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))" |
81 definition fps_times_def: "(*) = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))" |
82 instance .. |
82 instance .. |
83 end |
83 end |
84 |
84 |
85 lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n - i))" |
85 lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n - i))" |
86 unfolding fps_times_def by simp |
86 unfolding fps_times_def by simp |
2035 |
2035 |
2036 (* We can not reach the form of Wilf, but still near to it using rewrite rules*) |
2036 (* We can not reach the form of Wilf, but still near to it using rewrite rules*) |
2037 (* If f reprents {a_n} and P is a polynomial, then |
2037 (* If f reprents {a_n} and P is a polynomial, then |
2038 P(xD) f represents {P(n) a_n}*) |
2038 P(xD) f represents {P(n) a_n}*) |
2039 |
2039 |
2040 definition "fps_XD = ( * ) fps_X \<circ> fps_deriv" |
2040 definition "fps_XD = (*) fps_X \<circ> fps_deriv" |
2041 |
2041 |
2042 lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)" |
2042 lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)" |
2043 by (simp add: fps_XD_def field_simps) |
2043 by (simp add: fps_XD_def field_simps) |
2044 |
2044 |
2045 lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a" |
2045 lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a" |