author hoelzl Tue Jan 20 17:13:05 2015 +0100 (2015-01-20) changeset 59416 fde2659085e1 parent 59415 854fe701c984 child 59417 fc7054d65f5b
generalized sum_diff_distrib to setsum_subtractf_nat
 src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Groups_Big.thy	Fri Jan 16 10:59:15 2015 +0100
1.2 +++ b/src/HOL/Groups_Big.thy	Tue Jan 20 17:13:05 2015 +0100
1.3 @@ -630,19 +630,20 @@
1.5  qed
1.6
1.7 -lemma setsum_negf:
1.8 -  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
1.9 +lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
1.10  proof (cases "finite A")
1.11    case True thus ?thesis by (induct set: finite) auto
1.12  next
1.13    case False thus ?thesis by simp
1.14  qed
1.15
1.16 -lemma setsum_subtractf:
1.17 -  "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1.18 -    setsum f A - setsum g A"
1.19 +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)"
1.20    using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
1.21
1.22 +lemma setsum_subtractf_nat:
1.23 +  "(\<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)"
1.24 +  by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
1.25 +
1.26  lemma setsum_nonneg:
1.28    shows "0 \<le> setsum f A"
```
```     2.1 --- a/src/HOL/Set_Interval.thy	Fri Jan 16 10:59:15 2015 +0100
2.2 +++ b/src/HOL/Set_Interval.thy	Tue Jan 20 17:13:05 2015 +0100
2.3 @@ -1647,31 +1647,8 @@
2.4    "2 * (\<Sum>i\<in>{..<n}. a + int i * d) = int n * (a + (a + int(n - 1)*d))"
2.5    by (fact arith_series_general) (* FIXME: duplicate *)
2.6
2.7 -lemma sum_diff_distrib:
2.8 -  fixes P::"nat\<Rightarrow>nat"
2.9 -  shows
2.10 -  "\<forall>x. Q x \<le> P x  \<Longrightarrow>
2.11 -  (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x)"
2.12 -proof (induct n)
2.13 -  case 0 show ?case by simp
2.14 -next
2.15 -  case (Suc n)
2.16 -
2.17 -  let ?lhs = "(\<Sum>x<n. P x) - (\<Sum>x<n. Q x)"
2.18 -  let ?rhs = "\<Sum>x<n. P x - Q x"
2.19 -
2.20 -  from Suc have "?lhs = ?rhs" by simp
2.21 -  moreover
2.22 -  from Suc have "?lhs + P n - Q n = ?rhs + (P n - Q n)" by simp
2.23 -  moreover
2.24 -  from Suc have
2.25 -    "(\<Sum>x<n. P x) + P n - ((\<Sum>x<n. Q x) + Q n) = ?rhs + (P n - Q n)"
2.26 -    by (subst diff_diff_left[symmetric],