generalized sum_diff_distrib to setsum_subtractf_nat
authorhoelzl
Tue Jan 20 17:13:05 2015 +0100 (2015-01-20)
changeset 59416fde2659085e1
parent 59415 854fe701c984
child 59417 fc7054d65f5b
generalized sum_diff_distrib to setsum_subtractf_nat
src/HOL/Groups_Big.thy
src/HOL/Set_Interval.thy
     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.4    finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
     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.27    assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
    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],
    2.27 -        subst diff_add_assoc2)
    2.28 -       (auto simp: diff_add_assoc2 intro: setsum_mono)
    2.29 -  ultimately
    2.30 -  show ?case by simp
    2.31 -qed
    2.32 +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)"
    2.33 +  by (subst setsum_subtractf_nat) auto
    2.34  
    2.35  lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
    2.36    by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto