equal
deleted
inserted
replaced
995 lemma setsum_diff1: "finite A \<Longrightarrow> |
995 lemma setsum_diff1: "finite A \<Longrightarrow> |
996 (setsum f (A - {a}) :: ('a::ab_group_add)) = |
996 (setsum f (A - {a}) :: ('a::ab_group_add)) = |
997 (if a:A then setsum f A - f a else setsum f A)" |
997 (if a:A then setsum f A - f a else setsum f A)" |
998 by (erule finite_induct) (auto simp add: insert_Diff_if) |
998 by (erule finite_induct) (auto simp add: insert_Diff_if) |
999 |
999 |
|
1000 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)" |
|
1001 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))"]) |
|
1002 apply (auto simp add: insert_Diff_if add_ac) |
|
1003 done |
|
1004 |
1000 (* By Jeremy Siek: *) |
1005 (* By Jeremy Siek: *) |
1001 |
1006 |
1002 lemma setsum_diff_nat: |
1007 lemma setsum_diff_nat: |
1003 assumes finB: "finite B" |
1008 assumes finB: "finite B" |
1004 shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
1009 shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |