Expands a real number sum over an explicit interval of numerals
DESCRIPTION
The conversion EXPAND_SUM_CONV applied to a term of the form
`sum (m..n) f` where m and n are explicit numerals (the double-dot being
an infix set construction for a range), returns an expansion theorem
|- sum (m..n) f = f(m) + ... + f(n). In the common case where f is a
lambda-term, each application f(i) will be beta-reduced at the top level.
FAILURE CONDITIONS
EXPAND_SUM_CONV tm fails if tm is not a sum of the specified form.
EXAMPLE
The following is a typical use of the conversion:
# EXPAND_SUM_CONV `sum(1..8) f`;;
val it : thm =
|- sum (1..8) f = f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8
COMMENTS
As well as the natural-number version EXPAND_NSUM_CONV in the core HOL Light,
the library file Library/isum.ml contains a corresponding form for integer
sums EXPAND_ISUM_CONV.