# HG changeset patch # User nipkow # Date 1244443938 -7200 # Node ID 2a60c9b951e0dd03c032d8c454c90fd7984930d9 # Parent eced346b2231081e544236f15ed8a4f00f003cde New lemma diff -r eced346b2231 -r 2a60c9b951e0 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Mon Jun 08 00:26:57 2009 +0200 +++ b/src/HOL/SetInterval.thy Mon Jun 08 08:52:18 2009 +0200 @@ -833,6 +833,13 @@ apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) done +lemma setsum_ub_add_nat: assumes "(m::nat) \ n + 1" + shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" +proof- + have "{m .. n+p} = {m..n} \ {n+1..n+p}" using `m \ n+1` by auto + thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint + atLeastSucAtMost_greaterThanAtMost) +qed lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ setsum f {m..