src/HOL/Finite_Set.thy
changeset 15552 8ab8e425410b
parent 15543 0024472afce7
child 15554 03d4347b071d
--- 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: