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

subsection {* Summation indexed over intervals *}

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


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