[isabelle-dev] setsum/setprod
Lawrence Paulson
lp15 at cam.ac.uk
Tue Feb 17 15:07:33 CET 2009
We implement a nice syntax for summations indexed over intervals, but
nothing comparable products. The code below is from the file
SetInterval.thy. Products are treated instead in the file
Finite_Set.thy. Is there a fundamental reason why sums and products
are treated so differently?
Larry
subsection {* Summation indexed over intervals *}
syntax
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a
\<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a
\<Rightarrow> 'b
...
translations
"\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
"\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
"\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
"\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
More information about the isabelle-dev
mailing list