# HG changeset patch
# User hoelzl
# Date 1421770385 -3600
# Node ID fde2659085e1699bbf26e173751cc0dea33b1da3
# Parent  854fe701c9843dbd4052a5fb882c4f377fe6d678
generalized sum_diff_distrib to setsum_subtractf_nat

diff -r 854fe701c984 -r fde2659085e1 src/HOL/Groups_Big.thy
--- 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"
diff -r 854fe701c984 -r fde2659085e1 src/HOL/Set_Interval.thy
--- 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