Aded a thm.
authornipkow
Mon Aug 09 10:09:44 2004 +0200 (2004-08-09)
changeset 151241d9b4fcd222d
parent 15123 4c49281dc9a8
child 15125 5224130bc0d6
Aded a thm.
src/HOL/Finite_Set.thy
     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)