[isabelle-dev] setsum/setprod

[Lawrence Paulson]

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}"