src/HOL/Finite_Set.thy
changeset 15552 8ab8e425410b
parent 15543 0024472afce7
child 15554 03d4347b071d
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 28 13:10:36 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 28 18:29:55 2005 +0100
     1.3 @@ -997,6 +997,11 @@
     1.4    (if a:A then setsum f A - f a else setsum f A)"
     1.5    by (erule finite_induct) (auto simp add: insert_Diff_if)
     1.6  
     1.7 +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)"
     1.8 +  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))"])
     1.9 +  apply (auto simp add: insert_Diff_if add_ac)
    1.10 +  done
    1.11 +
    1.12  (* By Jeremy Siek: *)
    1.13  
    1.14  lemma setsum_diff_nat: