# HG changeset patch
# User obua
# Date 1109611795 -3600
# Node ID 8ab8e425410b5491a3699b939aba55ffaab83cca
# Parent  af78481b37bfca122449f6d3fd51214a41357b16
added setsum_diff1' which holds in more general cases than setsum_diff1

diff -r af78481b37bf -r 8ab8e425410b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Feb 28 13:10:36 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 28 18:29:55 2005 +0100
@@ -997,6 +997,11 @@
   (if a:A then setsum f A - f a else setsum f A)"
   by (erule finite_induct) (auto simp add: insert_Diff_if)
 
+lemma setsum_diff1'[rule_format]: "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
+  apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
+  apply (auto simp add: insert_Diff_if add_ac)
+  done
+
 (* By Jeremy Siek: *)
 
 lemma setsum_diff_nat: