--- a/src/HOL/Groups_Big.thy Fri Jan 16 10:59:15 2015 +0100
+++ b/src/HOL/Groups_Big.thy Tue Jan 20 17:13:05 2015 +0100
@@ -630,19 +630,20 @@
finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
qed
-lemma setsum_negf:
- "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
+lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
proof (cases "finite A")
case True thus ?thesis by (induct set: finite) auto
next
case False thus ?thesis by simp
qed
-lemma setsum_subtractf:
- "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
- setsum f A - setsum g A"
+lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x::'a::ab_group_add) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
+lemma setsum_subtractf_nat:
+ "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x::nat) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
+ by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
+
lemma setsum_nonneg:
assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
shows "0 \<le> setsum f A"
--- a/src/HOL/Set_Interval.thy Fri Jan 16 10:59:15 2015 +0100
+++ b/src/HOL/Set_Interval.thy Tue Jan 20 17:13:05 2015 +0100
@@ -1647,31 +1647,8 @@
"2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
by (fact arith_series_general) (* FIXME: duplicate *)
-lemma sum_diff_distrib:
- fixes P::"nat\<Rightarrow>nat"
- shows
- "\<forall>x. Q x \<le> P x \<Longrightarrow>
- (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n)
-
- let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
- let ?rhs = "\<Sum>x<n. P x - Q x"
-
- from Suc have "?lhs = ?rhs" by simp
- moreover
- from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
- moreover
- from Suc have
- "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
- by (subst diff_diff_left[symmetric],
- subst diff_add_assoc2)
- (auto simp: diff_add_assoc2 intro: setsum_mono)
- ultimately
- show ?case by simp
-qed
+lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
+ by (subst setsum_subtractf_nat) auto
lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto