# HG changeset patch
# User nipkow
# Date 1089793503 -7200
# Node ID fa7d27ef7e59224e18fcce134da5f56e7b0c007b
# Parent  a6b1f0cef7b33097534d03781473e67d0a6fc101
added {0::nat..n(} = {..n(}

diff -r a6b1f0cef7b3 -r fa7d27ef7e59 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jul 13 12:32:01 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 14 10:25:03 2004 +0200
@@ -761,6 +761,9 @@
   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   "setsum f A == if finite A then fold (op + o f) 0 A else 0"
 
+text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
+written @{text"\<Sum>x\<in>A. e"}. *}
+
 syntax
   "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_:_. _)" [0, 51, 10] 10)
 syntax (xsymbols)
@@ -770,6 +773,34 @@
 translations
   "\<Sum>i:A. b" == "setsum (%i. b) A"  -- {* Beware of argument permutation! *}
 
+text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
+ @{text"\<Sum>x|P. e"}. *}
+
+syntax
+  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ | / _./ _)" [0,0,10] 10)
+syntax (xsymbols)
+  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+syntax (HTML output)
+  "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
+
+translations "\<Sum>x|P. t" => "setsum (%x. t) {x. P}"
+
+print_translation {*
+let
+  fun setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = 
+    (if x<>y then raise Match
+     else let val x' = Syntax.mark_bound x
+              val t' = subst_bound(x',t)
+              val P' = subst_bound(x',P)
+          in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end)
+in
+[("setsum", setsum_tr')]
+end
+*}
+
+text{* As Jeremy Avigad notes: ultimately the analogous
+   thing should be done for setprod as well \dots *}
+
 
 lemma setsum_empty [simp]: "setsum f {} = 0"
   by (simp add: setsum_def)
diff -r a6b1f0cef7b3 -r fa7d27ef7e59 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jul 14 10:25:03 2004 +0200
@@ -229,6 +229,9 @@
 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
 by blast
 
+lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
+by(simp add:lessThan_def atLeastLessThan_def)
+
 text {* Intervals of nats with @{text Suc} *}
 
 lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
@@ -478,16 +481,30 @@
 lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
 
 
-subsection {* Summation indexed over natural numbers *}
+subsection {* Summation indexed over intervals *}
+
+text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
+@{term"\<Sum>x\<in>{a..b}. e"}. *}
+
+syntax
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
+syntax (xsymbols)
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
+syntax (HTML output)
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
+
+translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
+
+
+subsection {* Summation up to *}
 
 text{* Legacy, only used in HoareParallel and Isar-Examples. Really
-needed? Probably better to replace it with a more generic operator
-like ``SUM i = m..n. b''. *}
+needed? Probably better to replace it with above syntax. *}
 
 syntax
-  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
+  "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
 translations
-  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
+  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
 
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)