# HG changeset patch
# User nipkow
# Date 1092038984 -7200
# Node ID 1d9b4fcd222dc472e50e3e390a394d1f0cf1abb4
# Parent  4c49281dc9a8150df1d31b3906e11a25d7f376a8
Aded a thm.

diff -r 4c49281dc9a8 -r 1d9b4fcd222d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 06 17:29:24 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Aug 09 10:09:44 2004 +0200
@@ -965,6 +965,34 @@
   apply (drule_tac a = a in mk_disjoint_insert, auto)
   done
 
+(* By Jeremy Siek: *)
+
+lemma setsum_diff: 
+  assumes finB: "finite B"
+  shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
+using finB
+proof (induct)
+  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
+next
+  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
+    and xFinA: "insert x F \<subseteq> A"
+    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
+  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
+  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
+    by (simp add: setsum_diff1)
+  from xFinA have "F \<subseteq> A" by simp
+  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
+  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
+    by simp
+  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
+  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
+    by simp
+  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
+  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
+    by simp
+  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
+qed
+
 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
   - setsum f A"
   by (induct set: Finites, auto)