New lemma
authornipkow
Mon Jun 08 08:52:18 2009 +0200 (2009-06-08)
changeset 315012a60c9b951e0
parent 31500 eced346b2231
child 31503 cca1281e6384
New lemma
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/SetInterval.thy	Mon Jun 08 00:26:57 2009 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Jun 08 08:52:18 2009 +0200
     1.3 @@ -833,6 +833,13 @@
     1.4  apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps)
     1.5  done
     1.6  
     1.7 +lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
     1.8 +  shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}"
     1.9 +proof-
    1.10 +  have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto
    1.11 +  thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint
    1.12 +    atLeastSucAtMost_greaterThanAtMost)
    1.13 +qed
    1.14  
    1.15  lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    1.16    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"