[isabelle-dev] setsum/setprod

[Tobias Nipkow]

I assume I simply forgot products, or possibly they did not exist when I 
added the fancy sum syntax. Feel free to make a product copy of the sum 
syntax.

Tobias

Lawrence Paulson wrote:
> 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}"
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev