# HG changeset patch # User chaieb # Date 1233149039 0 # Node ID 3857d7eba390ec669dc83890cd1a38a8e4e0f214 # Parent f2584b0c76b5466ce88005b7358a97bd453cfad1 Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta diff -r f2584b0c76b5 -r 3857d7eba390 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Jan 28 13:36:24 2009 +0100 +++ b/src/HOL/Finite_Set.thy Wed Jan 28 13:23:59 2009 +0000 @@ -897,6 +897,46 @@ "inj_on f B ==> setsum f B = setsum id (f ` B)" by (auto simp add: setsum_reindex) +lemma setsum_reindex_nonzero: + assumes fS: "finite S" + and nz: "\ x y. x \ S \ y \ S \ x \ y \ f x = f y \ h (f x) = 0" + shows "setsum h (f ` S) = setsum (h o f) S" +using nz +proof(induct rule: finite_induct[OF fS]) + case 1 thus ?case by simp +next + case (2 x F) + {assume fxF: "f x \ f ` F" hence "\y \ F . f y = f x" by auto + then obtain y where y: "y \ F" "f x = f y" by auto + from "2.hyps" y have xy: "x \ y" by auto + + from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp + have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto + also have "\ = setsum (h o f) (insert x F)" + unfolding setsum_insert[OF `finite F` `x\F`] + using h0 + apply simp + apply (rule "2.hyps"(3)) + apply (rule_tac y="y" in "2.prems") + apply simp_all + done + finally have ?case .} + moreover + {assume fxF: "f x \ f ` F" + have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" + using fxF "2.hyps" by simp + also have "\ = setsum (h o f) (insert x F)" + unfolding setsum_insert[OF `finite F` `x\F`] + apply simp + apply (rule cong[OF refl[of "op + (h (f x))"]]) + apply (rule "2.hyps"(3)) + apply (rule_tac y="y" in "2.prems") + apply simp_all + done + finally have ?case .} + ultimately show ?case by blast +qed + lemma setsum_cong: "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong) @@ -914,6 +954,7 @@ ==> setsum h B = setsum g A" by (simp add: setsum_reindex cong: setsum_cong) + lemma setsum_0[simp]: "setsum (%i. 0) A = 0" apply (clarsimp simp: setsum_def) apply (erule finite_induct, auto) @@ -931,6 +972,73 @@ ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" by (subst setsum_Un_Int [symmetric], auto) +lemma setsum_mono_zero_left: + assumes fT: "finite T" and ST: "S \ T" + and z: "\i \ T - S. f i = 0" + shows "setsum f S = setsum f T" +proof- + have eq: "T = S \ (T - S)" using ST by blast + have d: "S \ (T - S) = {}" using ST by blast + from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) + show ?thesis + by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) +qed + +lemma setsum_mono_zero_right: + assumes fT: "finite T" and ST: "S \ T" + and z: "\i \ T - S. f i = 0" + shows "setsum f T = setsum f S" +using setsum_mono_zero_left[OF fT ST z] by simp + +lemma setsum_mono_zero_cong_left: + assumes fT: "finite T" and ST: "S \ T" + and z: "\i \ T - S. g i = 0" + and fg: "\x. x \ S \ f x = g x" + shows "setsum f S = setsum g T" +proof- + have eq: "T = S \ (T - S)" using ST by blast + have d: "S \ (T - S) = {}" using ST by blast + from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) + show ?thesis + using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) +qed + +lemma setsum_mono_zero_cong_right: + assumes fT: "finite T" and ST: "S \ T" + and z: "\i \ T - S. f i = 0" + and fg: "\x. x \ S \ f x = g x" + shows "setsum f T = setsum g S" +using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto + +lemma setsum_delta: + assumes fS: "finite S" + shows "setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" +proof- + let ?f = "(\k. if k=a then b k else 0)" + {assume a: "a \ S" + hence "\ k\ S. ?f k = 0" by simp + hence ?thesis using a by simp} + moreover + {assume a: "a \ S" + let ?A = "S - {a}" + let ?B = "{a}" + have eq: "S = ?A \ ?B" using a by blast + have dj: "?A \ ?B = {}" by simp + from fS have fAB: "finite ?A" "finite ?B" by auto + have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" + using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + by simp + then have ?thesis using a by simp} + ultimately show ?thesis by blast +qed +lemma setsum_delta': + assumes fS: "finite S" shows + "setsum (\k. if a = k then b k else 0) S = + (if a\ S then b a else 0)" + using setsum_delta[OF fS, of a b, symmetric] + by (auto intro: setsum_cong) + + (*But we can't get rid of finite I. If infinite, although the rhs is 0, the lhs need not be, since UNION I A could still be finite.*) lemma setsum_UN_disjoint: @@ -1365,6 +1473,18 @@ B = f ` A ==> g = h \ f ==> setprod h B = setprod g A" by (frule setprod_reindex, simp) +lemma strong_setprod_reindex_cong: assumes i: "inj_on f A" + and B: "B = f ` A" and eq: "\x. x \ A \ g x = (h \ f) x" + shows "setprod h B = setprod g A" +proof- + have "setprod h B = setprod (h o f) A" + by (simp add: B setprod_reindex[OF i, of h]) + then show ?thesis apply simp + apply (rule setprod_cong) + apply simp + by (erule eq[symmetric]) +qed + lemma setprod_1: "setprod (%i. 1) A = 1" apply (case_tac "finite A") @@ -1385,6 +1505,37 @@ ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" by (subst setprod_Un_Int [symmetric], auto) +lemma setprod_delta: + assumes fS: "finite S" + shows "setprod (\k. if k=a then b k else 1) S = (if a \ S then b a else 1)" +proof- + let ?f = "(\k. if k=a then b k else 1)" + {assume a: "a \ S" + hence "\ k\ S. ?f k = 1" by simp + hence ?thesis using a by (simp add: setprod_1 cong add: setprod_cong) } + moreover + {assume a: "a \ S" + let ?A = "S - {a}" + let ?B = "{a}" + have eq: "S = ?A \ ?B" using a by blast + have dj: "?A \ ?B = {}" by simp + from fS have fAB: "finite ?A" "finite ?B" by auto + have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto + have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" + using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + by simp + then have ?thesis using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)} + ultimately show ?thesis by blast +qed + +lemma setprod_delta': + assumes fS: "finite S" shows + "setprod (\k. if a = k then b k else 1) S = + (if a\ S then b a else 1)" + using setprod_delta[OF fS, of a b, symmetric] + by (auto intro: setprod_cong) + + lemma setprod_UN_disjoint: "finite I ==> (ALL i:I. finite (A i)) ==> (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> @@ -1675,6 +1826,34 @@ apply (auto simp add: power_Suc) done +lemma setprod_gen_delta: + assumes fS: "finite S" + shows "setprod (\k. if k=a then b k else c) S = (if a \ S then (b a ::'a::{comm_monoid_mult, recpower}) * c^ (card S - 1) else c^ card S)" +proof- + let ?f = "(\k. if k=a then b k else c)" + {assume a: "a \ S" + hence "\ k\ S. ?f k = c" by simp + hence ?thesis using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) } + moreover + {assume a: "a \ S" + let ?A = "S - {a}" + let ?B = "{a}" + have eq: "S = ?A \ ?B" using a by blast + have dj: "?A \ ?B = {}" by simp + from fS have fAB: "finite ?A" "finite ?B" by auto + have fA0:"setprod ?f ?A = setprod (\i. c) ?A" + apply (rule setprod_cong) by auto + have cA: "card ?A = card S - 1" using fS a by auto + have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto + have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" + using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] + by simp + then have ?thesis using a cA + by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)} + ultimately show ?thesis by blast +qed + + lemma setsum_bounded: assumes le: "\i. i\A \ f i \ (K::'a::{semiring_1, pordered_ab_semigroup_add})" shows "setsum f A \ of_nat(card A) * K"