src/HOL/SetInterval.thy
changeset 15539 333a88244569
parent 15418 e28853da5df5
child 15542 ee6cd48cf840
     1.1 --- a/src/HOL/SetInterval.thy	Sat Feb 19 18:44:34 2005 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 21 15:04:10 2005 +0100
     1.3 @@ -589,6 +589,22 @@
     1.4  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
     1.5  by (simp add:lessThan_Suc)
     1.6  
     1.7 +lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
     1.8 +  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
     1.9 +by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
    1.10 +
    1.11 +lemma setsum_diff_nat_ivl:
    1.12 +fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
    1.13 +shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    1.14 +  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
    1.15 +using setsum_add_nat_ivl [of m n p f,symmetric]
    1.16 +apply (simp add: add_ac)
    1.17 +done
    1.18 +
    1.19 +lemma setsum_shift_bounds_nat_ivl:
    1.20 +  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
    1.21 +by (induct "n", auto simp:atLeastLessThanSuc)
    1.22 +
    1.23  
    1.24  ML
    1.25  {*