equal
deleted
inserted
replaced
254 lemma natsum_Suc2: |
254 lemma natsum_Suc2: |
255 "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" |
255 "setsum f {..Suc n} = (f 0::'a::comm_monoid_add) + (setsum (%i. f (Suc i)) {..n})" |
256 proof (induct n) |
256 proof (induct n) |
257 case 0 show ?case by simp |
257 case 0 show ?case by simp |
258 next |
258 next |
259 case Suc thus ?case by (simp add: semigroup_add_class.add_assoc) |
259 case Suc thus ?case by (simp add: add_assoc) |
260 qed |
260 qed |
261 |
261 |
262 lemma natsum_cong [cong]: |
262 lemma natsum_cong [cong]: |
263 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> |
263 "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::comm_monoid_add) |] ==> |
264 setsum f {..j} = setsum g {..k}" |
264 setsum f {..j} = setsum g {..k}" |