--- 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)