author nipkow Mon Aug 09 10:09:44 2004 +0200 (2004-08-09) changeset 15124 1d9b4fcd222d parent 15123 4c49281dc9a8 child 15125 5224130bc0d6
Aded a thm.
 src/HOL/Finite_Set.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Finite_Set.thy	Fri Aug 06 17:29:24 2004 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Mon Aug 09 10:09:44 2004 +0200
1.3 @@ -965,6 +965,34 @@
1.4    apply (drule_tac a = a in mk_disjoint_insert, auto)
1.5    done
1.6
1.7 +(* By Jeremy Siek: *)
1.8 +
1.9 +lemma setsum_diff:
1.10 +  assumes finB: "finite B"
1.11 +  shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
1.12 +using finB
1.13 +proof (induct)
1.14 +  show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
1.15 +next
1.16 +  fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
1.17 +    and xFinA: "insert x F \<subseteq> A"
1.18 +    and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
1.19 +  from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
1.20 +  from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
1.21 +    by (simp add: setsum_diff1)
1.22 +  from xFinA have "F \<subseteq> A" by simp
1.23 +  with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
1.24 +  with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
1.25 +    by simp
1.26 +  from xnotinF have "A - insert x F = (A - F) - {x}" by auto
1.27 +  with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
1.28 +    by simp
1.29 +  from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
1.30 +  with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
1.31 +    by simp
1.32 +  thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
1.33 +qed
1.34 +
1.35  lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::comm_ring_1) A =
1.36    - setsum f A"
1.37    by (induct set: Finites, auto)
```