author chaieb Fri Apr 24 19:29:44 2009 +0100 (2009-04-24) changeset 30993 796cee3729f0 parent 30922 96d053e00ec0 parent 30992 3b143758dfe9 child 30994 ba5bce0c26de
merged
```     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Apr 21 17:07:44 2009 -0700
1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 24 19:29:44 2009 +0100
1.3 @@ -979,7 +979,7 @@
1.4    (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\<lambda>i. a_i * x^i))/x^h, for h>0*)
1.5
1.6  lemma fps_power_mult_eq_shift:
1.7 -  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}" (is "?lhs = ?rhs")
1.8 +  "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}" (is "?lhs = ?rhs")
1.9  proof-
1.10    {fix n:: nat
1.11      have "?lhs \$ n = (if n < Suc k then 0 else a n)"
1.12 @@ -990,7 +990,7 @@
1.13      next
1.14        case (Suc k)
1.15        note th = Suc.hyps[symmetric]
1.16 -      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. Suc k})\$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: field) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) \$ n" by (simp add: ring_simps)
1.17 +      have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})\$n = (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) \$ n" by (simp add: ring_simps)
1.18        also  have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)\$n"
1.19  	using th
1.20  	unfolding fps_sub_nth by simp
1.21 @@ -1027,7 +1027,7 @@
1.22
1.23  lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a\$n)" by (simp add: fps_eq_iff)
1.24
1.25 -lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a\$n)"
1.26 +lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a\$n)"
1.27  by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def)
1.28
1.29  subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
```