# [isabelle] Using Formal_Power_Series.thy

Hello,
Based on Formal_Power_Series.thy (
http://www.cl.cam.ac.uk/research/hvg/isabelle/dist/library/HOL/HOL-Library/Formal_Power_Series.html),
I need to prove:
lemma "((%k . X * (setsum (λ n. (fps_const (f$n)) * (X^n)) {0..(k::nat)})))
----> X * f"
which of course is like fps_notation but with a factor of X.
It would seem however that dist_fps_def doesn't have the right properties
for me to pull out the X. I think I would need to have something like
dist (X * (∑n = 0..n. fps_const (f $ n) * X ^ n)) (X * f) < r ==> dist
((∑n = 0..n. fps_const (f $ n) * X ^ n)) f < r2
where r = r2 * X i.e. dist has norm like properties and not just those of
a metric space.
Is there anyway to prove what I need to prove?
By the way, what I am really after is
lemma "(X * (setsum (λ n. (fps_const (f$n)) * (X^n)) {0..})) = X * f"
but the definition of setsum gives 0 for sums over non-finite sets.
Cheers
Mark

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*