[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.