src/HOL/SetInterval.thy
changeset 15041 a6b1f0cef7b3
parent 14846 b1fcade3880b
child 15042 fa7d27ef7e59
     1.1 --- a/src/HOL/SetInterval.thy	Mon Jul 12 19:56:58 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Tue Jul 13 12:32:01 2004 +0200
     1.3 @@ -477,4 +477,19 @@
     1.4  
     1.5  lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two
     1.6  
     1.7 +
     1.8 +subsection {* Summation indexed over natural numbers *}
     1.9 +
    1.10 +text{* Legacy, only used in HoareParallel and Isar-Examples. Really
    1.11 +needed? Probably better to replace it with a more generic operator
    1.12 +like ``SUM i = m..n. b''. *}
    1.13 +
    1.14 +syntax
    1.15 +  "_Summation" :: "id => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
    1.16 +translations
    1.17 +  "\<Sum>i < n. b" == "setsum (\<lambda>i::nat. b) {..n(}"
    1.18 +
    1.19 +lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    1.20 +by (simp add:lessThan_Suc)
    1.21 +
    1.22  end