# HG changeset patch # User nipkow # Date 1101224574 -3600 # Node ID a358e31572d943bb236cb4c520e0b3c45d68cb50 # Parent 55eec5c6d40119fa3ca6c6b0e10d3e8fd01788c6 renamed 2 lemmas diff -r 55eec5c6d401 -r a358e31572d9 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Nov 23 15:50:27 2004 +0100 +++ b/src/HOL/Finite_Set.thy Tue Nov 23 16:42:54 2004 +0100 @@ -962,7 +962,7 @@ setsum f A + setsum f B - setsum f (A Int B)" by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) -lemma setsum_diff1: "(setsum f (A - {a}) :: nat) = +lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = (if a:A then setsum f A - f a else setsum f A)" apply (case_tac "finite A") prefer 2 apply (simp add: setsum_def) @@ -971,9 +971,14 @@ apply (drule_tac a = a in mk_disjoint_insert, auto) done +lemma setsum_diff1: "finite A \ + (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) = + (if a:A then setsum f A - f a else setsum f A)" + by (erule finite_induct) (auto simp add: insert_Diff_if) + (* By Jeremy Siek: *) -lemma setsum_diff: +lemma setsum_diff_nat: assumes finB: "finite B" shows "B \ A \ (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" using finB @@ -985,7 +990,7 @@ and IH: "F \ A \ setsum f (A - F) = setsum f A - setsum f F" from xnotinF xFinA have xinAF: "x \ (A - F)" by simp from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" - by (simp add: setsum_diff1) + by (simp add: setsum_diff1_nat) from xFinA have "F \ A" by simp with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" @@ -999,6 +1004,26 @@ thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp qed +lemma setsum_diff: + assumes le: "finite A" "B \ A" + shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))" +proof - + from le have finiteB: "finite B" using finite_subset by auto + show ?thesis using le finiteB + proof (induct rule: Finites.induct[OF finiteB]) + case 1 + thus ?case by auto + next + case 2 + thus ?case using le + apply auto + apply (subst Diff_insert) + apply (subst setsum_diff1) + apply (auto simp add: insert_absorb) + done + qed + qed + lemma setsum_mono: assumes le: "\i. i\K \ f (i::'a) \ ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" shows "(\i\K. f i) \ (\i\K. g i)" @@ -1019,30 +1044,6 @@ by (simp add: setsum_def) qed -lemma finite_setsum_diff1: "finite A \ (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) = - (if a:A then setsum f A - f a else setsum f A)" - by (erule finite_induct) (auto simp add: insert_Diff_if) - -lemma finite_setsum_diff: - assumes le: "finite A" "B \ A" - shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))" -proof - - from le have finiteB: "finite B" using finite_subset by auto - show ?thesis using le finiteB - proof (induct rule: Finites.induct[OF finiteB]) - case 1 - thus ?case by auto - next - case 2 - thus ?case using le - apply auto - apply (subst Diff_insert) - apply (subst finite_setsum_diff1) - apply (auto simp add: insert_absorb) - done - qed - qed - lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" by (induct set: Finites, auto)