1.1 --- a/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Wed Jul 14 10:25:03 2004 +0200
     1.3 @@ -229,6 +229,9 @@
     1.4  lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
     1.5  by blast
     1.6  
     1.7 +lemma atLeast0LessThan [simp]: "{0::nat..n(} = {..n(}"
     1.8 +by(simp add:lessThan_def atLeastLessThan_def)
     1.9 +
    1.10  text {* Intervals of nats with @{text Suc} *}
    1.11  
    1.12  lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
    1.13 @@ -478,16 +481,30 @@
    1.14  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
    1.15  
    1.16  
    1.17 -subsection {* Summation indexed over natural numbers *}
    1.18 +subsection {* Summation indexed over intervals *}
    1.19 +
    1.20 +text{* We introduce the obvious syntax @{text"\<Sum>x=a..b. e"} for
    1.21 +@{term"\<Sum>x\<in>{a..b}. e"}. *}
    1.22 +
    1.23 +syntax
    1.24 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
    1.25 +syntax (xsymbols)
    1.26 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    1.27 +syntax (HTML output)
    1.28 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
    1.29 +
    1.30 +translations "\<Sum>x=a..b. t" == "setsum (%x. t) {a..b}"
    1.31 +
    1.32 +
    1.33 +subsection {* Summation up to *}
    1.34  
    1.35  text{* Legacy, only used in HoareParallel and Isar-Examples. Really
    1.36 -needed? Probably better to replace it with a more generic operator
    1.37 -like ``SUM i = m..n. b''. *}
    1.38 +needed? Probably better to replace it with above syntax. *}
    1.39  
    1.40  syntax
    1.41 -  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.42 +  "_Summation" :: "idt => 'a => 'b => 'b"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.43  translations
    1.44 -  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
    1.45 +  "\<Sum>i < n. b" == "setsum (\<lambda>i. b) {..n(}"
    1.46  
    1.47  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    1.48  by (simp add:lessThan_Suc)