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.

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)