141 by (induct B rule: infinite_finite_induct) auto |
145 by (induct B rule: infinite_finite_induct) auto |
142 |
146 |
143 lemma strong_cong [cong]: |
147 lemma strong_cong [cong]: |
144 assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x" |
148 assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x" |
145 shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B" |
149 shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B" |
146 by (rule cong) (insert assms, simp_all add: simp_implies_def) |
150 by (rule cong) (use assms in \<open>simp_all add: simp_implies_def\<close>) |
147 |
151 |
148 lemma reindex_cong: |
152 lemma reindex_cong: |
149 assumes "inj_on l B" |
153 assumes "inj_on l B" |
150 assumes "A = l ` B" |
154 assumes "A = l ` B" |
151 assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x" |
155 assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x" |
152 shows "F g A = F h B" |
156 shows "F g A = F h B" |
153 using assms by (simp add: reindex) |
157 using assms by (simp add: reindex) |
154 |
158 |
155 lemma UNION_disjoint: |
159 lemma UNION_disjoint: |
156 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
160 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
157 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" |
161 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" |
158 shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I" |
162 shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I" |
159 apply (insert assms) |
163 apply (insert assms) |
160 apply (induct rule: finite_induct) |
164 apply (induct rule: finite_induct) |
161 apply simp |
165 apply simp |
162 apply atomize |
166 apply atomize |
163 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i") |
167 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i") |
164 prefer 2 apply blast |
168 prefer 2 apply blast |
165 apply (subgoal_tac "A x Int UNION Fa A = {}") |
169 apply (subgoal_tac "A x \<inter> UNION Fa A = {}") |
166 prefer 2 apply blast |
170 prefer 2 apply blast |
167 apply (simp add: union_disjoint) |
171 apply (simp add: union_disjoint) |
168 done |
172 done |
169 |
173 |
170 lemma Union_disjoint: |
174 lemma Union_disjoint: |
171 assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}" |
175 assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}" |
172 shows "F g (\<Union>C) = (F \<circ> F) g C" |
176 shows "F g (\<Union>C) = (F \<circ> F) g C" |
173 proof cases |
177 proof (cases "finite C") |
174 assume "finite C" |
178 case True |
175 from UNION_disjoint [OF this assms] |
179 from UNION_disjoint [OF this assms] show ?thesis by simp |
176 show ?thesis by simp |
180 next |
177 qed (auto dest: finite_UnionD intro: infinite) |
181 case False |
178 |
182 then show ?thesis by (auto dest: finite_UnionD intro: infinite) |
179 lemma distrib: |
183 qed |
180 "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A" |
184 |
|
185 lemma distrib: "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A" |
181 by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute) |
186 by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute) |
182 |
187 |
183 lemma Sigma: |
188 lemma Sigma: |
184 "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)" |
189 "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)" |
185 apply (subst Sigma_def) |
190 apply (subst Sigma_def) |
186 apply (subst UNION_disjoint, assumption, simp) |
191 apply (subst UNION_disjoint) |
187 apply blast |
192 apply assumption |
188 apply (rule cong) |
193 apply simp |
189 apply rule |
194 apply blast |
190 apply (simp add: fun_eq_iff) |
195 apply (rule cong) |
191 apply (subst UNION_disjoint, simp, simp) |
196 apply rule |
192 apply blast |
197 apply (simp add: fun_eq_iff) |
193 apply (simp add: comp_def) |
198 apply (subst UNION_disjoint) |
194 done |
199 apply simp |
|
200 apply simp |
|
201 apply blast |
|
202 apply (simp add: comp_def) |
|
203 done |
195 |
204 |
196 lemma related: |
205 lemma related: |
197 assumes Re: "R \<^bold>1 \<^bold>1" |
206 assumes Re: "R \<^bold>1 \<^bold>1" |
198 and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)" |
207 and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)" |
199 and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)" |
208 and fin: "finite S" |
|
209 and R_h_g: "\<forall>x\<in>S. R (h x) (g x)" |
200 shows "R (F h S) (F g S)" |
210 shows "R (F h S) (F g S)" |
201 using fS by (rule finite_subset_induct) (insert assms, auto) |
211 using fin by (rule finite_subset_induct) (use assms in auto) |
202 |
212 |
203 lemma mono_neutral_cong_left: |
213 lemma mono_neutral_cong_left: |
204 assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = \<^bold>1" |
214 assumes "finite T" |
205 and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T" |
215 and "S \<subseteq> T" |
|
216 and "\<forall>i \<in> T - S. h i = \<^bold>1" |
|
217 and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" |
|
218 shows "F g S = F h T" |
206 proof- |
219 proof- |
207 have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast |
220 have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast |
208 have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast |
221 have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast |
209 from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)" |
222 from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)" |
210 by (auto intro: finite_subset) |
223 by (auto intro: finite_subset) |
211 show ?thesis using assms(4) |
224 show ?thesis using assms(4) |
212 by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) |
225 by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) |
213 qed |
226 qed |
214 |
227 |
215 lemma mono_neutral_cong_right: |
228 lemma mono_neutral_cong_right: |
216 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk> |
229 "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> g x = h x) \<Longrightarrow> |
217 \<Longrightarrow> F g T = F h S" |
230 F g T = F h S" |
218 by (auto intro!: mono_neutral_cong_left [symmetric]) |
231 by (auto intro!: mono_neutral_cong_left [symmetric]) |
219 |
232 |
220 lemma mono_neutral_left: |
233 lemma mono_neutral_left: "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> F g S = F g T" |
221 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g S = F g T" |
|
222 by (blast intro: mono_neutral_cong_left) |
234 by (blast intro: mono_neutral_cong_left) |
223 |
235 |
224 lemma mono_neutral_right: |
236 lemma mono_neutral_right: "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> F g T = F g S" |
225 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = \<^bold>1 \<rbrakk> \<Longrightarrow> F g T = F g S" |
|
226 by (blast intro!: mono_neutral_left [symmetric]) |
237 by (blast intro!: mono_neutral_left [symmetric]) |
227 |
238 |
228 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T" |
239 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T" |
229 by (auto simp: bij_betw_def reindex) |
240 by (auto simp: bij_betw_def reindex) |
230 |
241 |
303 qed |
316 qed |
304 |
317 |
305 lemma delta: |
318 lemma delta: |
306 assumes fS: "finite S" |
319 assumes fS: "finite S" |
307 shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" |
320 shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" |
308 proof- |
321 proof - |
309 let ?f = "(\<lambda>k. if k=a then b k else \<^bold>1)" |
322 let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)" |
310 { assume a: "a \<notin> S" |
323 show ?thesis |
311 hence "\<forall>k\<in>S. ?f k = \<^bold>1" by simp |
324 proof (cases "a \<in> S") |
312 hence ?thesis using a by simp } |
325 case False |
313 moreover |
326 then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp |
314 { assume a: "a \<in> S" |
327 with False show ?thesis by simp |
|
328 next |
|
329 case True |
315 let ?A = "S - {a}" |
330 let ?A = "S - {a}" |
316 let ?B = "{a}" |
331 let ?B = "{a}" |
317 have eq: "S = ?A \<union> ?B" using a by blast |
332 from True have eq: "S = ?A \<union> ?B" by blast |
318 have dj: "?A \<inter> ?B = {}" by simp |
333 have dj: "?A \<inter> ?B = {}" by simp |
319 from fS have fAB: "finite ?A" "finite ?B" by auto |
334 from fS have fAB: "finite ?A" "finite ?B" by auto |
320 have "F ?f S = F ?f ?A \<^bold>* F ?f ?B" |
335 have "F ?f S = F ?f ?A \<^bold>* F ?f ?B" |
321 using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] |
336 using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp |
322 by simp |
337 with True show ?thesis by simp |
323 then have ?thesis using a by simp } |
338 qed |
324 ultimately show ?thesis by blast |
|
325 qed |
339 qed |
326 |
340 |
327 lemma delta': |
341 lemma delta': |
328 assumes fS: "finite S" |
342 assumes fin: "finite S" |
329 shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" |
343 shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" |
330 using delta [OF fS, of a b, symmetric] by (auto intro: cong) |
344 using delta [OF fin, of a b, symmetric] by (auto intro: cong) |
331 |
345 |
332 lemma If_cases: |
346 lemma If_cases: |
333 fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a" |
347 fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a" |
334 assumes fA: "finite A" |
348 assumes fin: "finite A" |
335 shows "F (\<lambda>x. if P x then h x else g x) A = |
349 shows "F (\<lambda>x. if P x then h x else g x) A = F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})" |
336 F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})" |
350 proof - |
337 proof - |
351 have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" |
338 have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" |
|
339 "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" |
|
340 by blast+ |
352 by blast+ |
341 from fA |
353 from fin have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto |
342 have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto |
|
343 let ?g = "\<lambda>x. if P x then h x else g x" |
354 let ?g = "\<lambda>x. if P x then h x else g x" |
344 from union_disjoint [OF f a(2), of ?g] a(1) |
355 from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis |
345 show ?thesis |
|
346 by (subst (1 2) cong) simp_all |
356 by (subst (1 2) cong) simp_all |
347 qed |
357 qed |
348 |
358 |
349 lemma cartesian_product: |
359 lemma cartesian_product: "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)" |
350 "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)" |
360 apply (rule sym) |
351 apply (rule sym) |
361 apply (cases "finite A") |
352 apply (cases "finite A") |
362 apply (cases "finite B") |
353 apply (cases "finite B") |
363 apply (simp add: Sigma) |
354 apply (simp add: Sigma) |
364 apply (cases "A = {}") |
355 apply (cases "A={}", simp) |
365 apply simp |
356 apply simp |
366 apply simp |
357 apply (auto intro: infinite dest: finite_cartesian_productD2) |
367 apply (auto intro: infinite dest: finite_cartesian_productD2) |
358 apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1) |
368 apply (cases "B = {}") |
359 done |
369 apply (auto intro: infinite dest: finite_cartesian_productD1) |
|
370 done |
360 |
371 |
361 lemma inter_restrict: |
372 lemma inter_restrict: |
362 assumes "finite A" |
373 assumes "finite A" |
363 shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A" |
374 shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A" |
364 proof - |
375 proof - |
365 let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1" |
376 let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1" |
366 have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1" |
377 have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1" by simp |
367 by simp |
|
368 moreover have "A \<inter> B \<subseteq> A" by blast |
378 moreover have "A \<inter> B \<subseteq> A" by blast |
369 ultimately have "F ?g (A \<inter> B) = F ?g A" using \<open>finite A\<close> |
379 ultimately have "F ?g (A \<inter> B) = F ?g A" |
370 by (intro mono_neutral_left) auto |
380 using \<open>finite A\<close> by (intro mono_neutral_left) auto |
371 then show ?thesis by simp |
381 then show ?thesis by simp |
372 qed |
382 qed |
373 |
383 |
374 lemma inter_filter: |
384 lemma inter_filter: |
375 "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A" |
385 "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A" |
376 by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def) |
386 by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def) |
377 |
387 |
378 lemma Union_comp: |
388 lemma Union_comp: |
379 assumes "\<forall>A \<in> B. finite A" |
389 assumes "\<forall>A \<in> B. finite A" |
380 and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = \<^bold>1" |
390 and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = \<^bold>1" |
381 shows "F g (\<Union>B) = (F \<circ> F) g B" |
391 shows "F g (\<Union>B) = (F \<circ> F) g B" |
382 using assms proof (induct B rule: infinite_finite_induct) |
392 using assms |
|
393 proof (induct B rule: infinite_finite_induct) |
383 case (infinite A) |
394 case (infinite A) |
384 then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD) |
395 then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD) |
385 with infinite show ?case by simp |
396 with infinite show ?case by simp |
386 next |
397 next |
387 case empty then show ?case by simp |
398 case empty |
|
399 then show ?case by simp |
388 next |
400 next |
389 case (insert A B) |
401 case (insert A B) |
390 then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B" |
402 then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B" |
391 and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1" |
403 and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1" |
392 and H: "F g (\<Union>B) = (F o F) g B" by auto |
404 and H: "F g (\<Union>B) = (F \<circ> F) g B" by auto |
393 then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)" |
405 then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)" |
394 by (simp add: union_inter_neutral) |
406 by (simp add: union_inter_neutral) |
395 with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case |
407 with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case |
396 by (simp add: H) |
408 by (simp add: H) |
397 qed |
409 qed |
398 |
410 |
399 lemma commute: |
411 lemma commute: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B" |
400 "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B" |
|
401 unfolding cartesian_product |
412 unfolding cartesian_product |
402 by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto |
413 by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto |
403 |
414 |
404 lemma commute_restrict: |
415 lemma commute_restrict: |
405 "finite A \<Longrightarrow> finite B \<Longrightarrow> |
416 "finite A \<Longrightarrow> finite B \<Longrightarrow> |
502 end |
510 end |
503 | setsum_tr' _ = raise Match; |
511 | setsum_tr' _ = raise Match; |
504 in [(@{const_syntax setsum}, K setsum_tr')] end |
512 in [(@{const_syntax setsum}, K setsum_tr')] end |
505 \<close> |
513 \<close> |
506 |
514 |
507 text \<open>TODO generalization candidates\<close> |
515 (* TODO generalization candidates *) |
508 |
516 |
509 lemma (in comm_monoid_add) setsum_image_gen: |
517 lemma (in comm_monoid_add) setsum_image_gen: |
510 assumes fS: "finite S" |
518 assumes fin: "finite S" |
511 shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
519 shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
512 proof- |
520 proof - |
513 { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } |
521 have "{y. y\<in> f`S \<and> f x = y} = {f x}" if "x \<in> S" for x |
514 hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" |
522 using that by auto |
|
523 then have "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" |
515 by simp |
524 by simp |
516 also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
525 also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" |
517 by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]]) |
526 by (rule setsum.commute_restrict [OF fin finite_imageI [OF fin]]) |
518 finally show ?thesis . |
527 finally show ?thesis . |
519 qed |
528 qed |
520 |
529 |
521 |
530 |
522 subsubsection \<open>Properties in more restricted classes of structures\<close> |
531 subsubsection \<open>Properties in more restricted classes of structures\<close> |
523 |
532 |
524 lemma setsum_Un: "finite A ==> finite B ==> |
533 lemma setsum_Un: |
525 (setsum f (A Un B) :: 'a :: ab_group_add) = |
534 "finite A \<Longrightarrow> finite B \<Longrightarrow> setsum f (A \<union> B) = setsum f A + setsum f B - setsum f (A \<inter> B)" |
526 setsum f A + setsum f B - setsum f (A Int B)" |
535 for f :: "'b \<Rightarrow> 'a::ab_group_add" |
527 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps) |
536 by (subst setsum.union_inter [symmetric]) (auto simp add: algebra_simps) |
528 |
537 |
529 lemma setsum_Un2: |
538 lemma setsum_Un2: |
530 assumes "finite (A \<union> B)" |
539 assumes "finite (A \<union> B)" |
531 shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)" |
540 shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)" |
532 proof - |
541 proof - |
533 have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B" |
542 have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B" |
534 by auto |
543 by auto |
535 with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+ |
544 with assms show ?thesis |
536 qed |
545 by simp (subst setsum.union_disjoint, auto)+ |
537 |
546 qed |
538 lemma setsum_diff1: "finite A \<Longrightarrow> |
547 |
539 (setsum f (A - {a}) :: ('a::ab_group_add)) = |
548 lemma setsum_diff1: |
540 (if a:A then setsum f A - f a else setsum f A)" |
549 fixes f :: "'b \<Rightarrow> 'a::ab_group_add" |
541 by (erule finite_induct) (auto simp add: insert_Diff_if) |
550 assumes "finite A" |
|
551 shows "setsum f (A - {a}) = (if a \<in> A then setsum f A - f a else setsum f A)" |
|
552 using assms by induct (auto simp: insert_Diff_if) |
542 |
553 |
543 lemma setsum_diff: |
554 lemma setsum_diff: |
544 assumes le: "finite A" "B \<subseteq> A" |
555 fixes f :: "'b \<Rightarrow> 'a::ab_group_add" |
545 shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))" |
556 assumes "finite A" "B \<subseteq> A" |
546 proof - |
557 shows "setsum f (A - B) = setsum f A - setsum f B" |
547 from le have finiteB: "finite B" using finite_subset by auto |
558 proof - |
548 show ?thesis using finiteB le |
559 from assms(2,1) have "finite B" by (rule finite_subset) |
|
560 from this \<open>B \<subseteq> A\<close> |
|
561 show ?thesis |
549 proof induct |
562 proof induct |
550 case empty |
563 case empty |
551 thus ?case by auto |
564 thus ?case by simp |
552 next |
565 next |
553 case (insert x F) |
566 case (insert x F) |
554 thus ?case using le finiteB |
567 with \<open>finite A\<close> \<open>finite B\<close> show ?case |
555 by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
568 by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
556 qed |
569 qed |
557 qed |
570 qed |
558 |
571 |
559 lemma (in ordered_comm_monoid_add) setsum_mono: |
572 lemma (in ordered_comm_monoid_add) setsum_mono: |
560 assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i" |
573 assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i" |
561 shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
574 shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
562 proof (cases "finite K") |
575 proof (cases "finite K") |
563 case True |
576 case True |
564 thus ?thesis using le |
577 from this le show ?thesis |
565 proof induct |
578 proof induct |
566 case empty |
579 case empty |
567 thus ?case by simp |
580 then show ?case by simp |
568 next |
581 next |
569 case insert |
582 case insert |
570 thus ?case using add_mono by fastforce |
583 then show ?case using add_mono by fastforce |
571 qed |
584 qed |
572 next |
585 next |
573 case False then show ?thesis by simp |
586 case False |
|
587 then show ?thesis by simp |
574 qed |
588 qed |
575 |
589 |
576 lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono: |
590 lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono: |
577 assumes "finite A" "A \<noteq> {}" and "\<And>x. x \<in> A \<Longrightarrow> f x < g x" |
591 assumes "finite A" "A \<noteq> {}" |
|
592 and "\<And>x. x \<in> A \<Longrightarrow> f x < g x" |
578 shows "setsum f A < setsum g A" |
593 shows "setsum f A < setsum g A" |
579 using assms |
594 using assms |
580 proof (induct rule: finite_ne_induct) |
595 proof (induct rule: finite_ne_induct) |
581 case singleton thus ?case by simp |
596 case singleton |
582 next |
597 then show ?case by simp |
583 case insert thus ?case by (auto simp: add_strict_mono) |
598 next |
|
599 case insert |
|
600 then show ?case by (auto simp: add_strict_mono) |
584 qed |
601 qed |
585 |
602 |
586 lemma setsum_strict_mono_ex1: |
603 lemma setsum_strict_mono_ex1: |
587 fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add" |
604 fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add" |
588 assumes "finite A" and "\<forall>x\<in>A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a" |
605 assumes "finite A" |
|
606 and "\<forall>x\<in>A. f x \<le> g x" |
|
607 and "\<exists>a\<in>A. f a < g a" |
589 shows "setsum f A < setsum g A" |
608 shows "setsum f A < setsum g A" |
590 proof- |
609 proof- |
591 from assms(3) obtain a where a: "a:A" "f a < g a" by blast |
610 from assms(3) obtain a where a: "a \<in> A" "f a < g a" by blast |
592 have "setsum f A = setsum f ((A-{a}) \<union> {a})" |
611 have "setsum f A = setsum f ((A - {a}) \<union> {a})" |
593 by(simp add:insert_absorb[OF \<open>a:A\<close>]) |
612 by(simp add: insert_absorb[OF \<open>a \<in> A\<close>]) |
594 also have "\<dots> = setsum f (A-{a}) + setsum f {a}" |
613 also have "\<dots> = setsum f (A - {a}) + setsum f {a}" |
595 using \<open>finite A\<close> by(subst setsum.union_disjoint) auto |
614 using \<open>finite A\<close> by(subst setsum.union_disjoint) auto |
596 also have "setsum f (A-{a}) \<le> setsum g (A-{a})" |
615 also have "setsum f (A - {a}) \<le> setsum g (A - {a})" |
597 by(rule setsum_mono)(simp add: assms(2)) |
616 by (rule setsum_mono) (simp add: assms(2)) |
598 also have "setsum f {a} < setsum g {a}" using a by simp |
617 also from a have "setsum f {a} < setsum g {a}" by simp |
599 also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})" |
618 also have "setsum g (A - {a}) + setsum g {a} = setsum g((A - {a}) \<union> {a})" |
600 using \<open>finite A\<close> by(subst setsum.union_disjoint[symmetric]) auto |
619 using \<open>finite A\<close> by (subst setsum.union_disjoint[symmetric]) auto |
601 also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF \<open>a:A\<close>]) |
620 also have "\<dots> = setsum g A" by (simp add: insert_absorb[OF \<open>a \<in> A\<close>]) |
602 finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono) |
621 finally show ?thesis |
|
622 by (auto simp add: add_right_mono add_strict_left_mono) |
603 qed |
623 qed |
604 |
624 |
605 lemma setsum_mono_inv: |
625 lemma setsum_mono_inv: |
606 fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add" |
626 fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add" |
607 assumes eq: "setsum f I = setsum g I" |
627 assumes eq: "setsum f I = setsum g I" |
608 assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i" |
628 assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i" |
609 assumes i: "i \<in> I" |
629 assumes i: "i \<in> I" |
610 assumes I: "finite I" |
630 assumes I: "finite I" |
611 shows "f i = g i" |
631 shows "f i = g i" |
612 proof(rule ccontr) |
632 proof (rule ccontr) |
613 assume "f i \<noteq> g i" |
633 assume "\<not> ?thesis" |
614 with le[OF i] have "f i < g i" by simp |
634 with le[OF i] have "f i < g i" by simp |
615 hence "\<exists>i\<in>I. f i < g i" using i .. |
635 with i have "\<exists>i\<in>I. f i < g i" .. |
616 from setsum_strict_mono_ex1[OF I _ this] le have "setsum f I < setsum g I" by blast |
636 from setsum_strict_mono_ex1[OF I _ this] le have "setsum f I < setsum g I" |
|
637 by blast |
617 with eq show False by simp |
638 with eq show False by simp |
618 qed |
639 qed |
619 |
640 |
620 lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)" |
641 lemma setsum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)" |
621 proof (cases "finite A") |
642 for f :: "'b \<Rightarrow> 'a::ab_group_add" |
622 case True thus ?thesis by (induct set: finite) auto |
643 proof (cases "finite A") |
623 next |
644 case True |
624 case False thus ?thesis by simp |
645 then show ?thesis by (induct set: finite) auto |
625 qed |
646 next |
626 |
647 case False |
627 lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x::'a::ab_group_add) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)" |
648 then show ?thesis by simp |
|
649 qed |
|
650 |
|
651 lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)" |
|
652 for f g :: "'b \<Rightarrow>'a::ab_group_add" |
628 using setsum.distrib [of f "- g" A] by (simp add: setsum_negf) |
653 using setsum.distrib [of f "- g" A] by (simp add: setsum_negf) |
629 |
654 |
630 lemma setsum_subtractf_nat: |
655 lemma setsum_subtractf_nat: |
631 "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x::nat) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)" |
656 "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)" |
632 by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono) |
657 for f g :: "'a \<Rightarrow> nat" |
633 |
658 by (induct A rule: infinite_finite_induct) (auto simp: setsum_mono) |
634 lemma (in ordered_comm_monoid_add) setsum_nonneg: |
659 |
|
660 context ordered_comm_monoid_add |
|
661 begin |
|
662 |
|
663 lemma setsum_nonneg: |
635 assumes nn: "\<forall>x\<in>A. 0 \<le> f x" |
664 assumes nn: "\<forall>x\<in>A. 0 \<le> f x" |
636 shows "0 \<le> setsum f A" |
665 shows "0 \<le> setsum f A" |
637 proof (cases "finite A") |
666 proof (cases "finite A") |
638 case True thus ?thesis using nn |
667 case True |
|
668 then show ?thesis |
|
669 using nn |
639 proof induct |
670 proof induct |
640 case empty then show ?case by simp |
671 case empty |
|
672 then show ?case by simp |
641 next |
673 next |
642 case (insert x F) |
674 case (insert x F) |
643 then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono) |
675 then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono) |
644 with insert show ?case by simp |
676 with insert show ?case by simp |
645 qed |
677 qed |
646 next |
678 next |
647 case False thus ?thesis by simp |
679 case False |
648 qed |
680 then show ?thesis by simp |
649 |
681 qed |
650 lemma (in ordered_comm_monoid_add) setsum_nonpos: |
682 |
|
683 lemma setsum_nonpos: |
651 assumes np: "\<forall>x\<in>A. f x \<le> 0" |
684 assumes np: "\<forall>x\<in>A. f x \<le> 0" |
652 shows "setsum f A \<le> 0" |
685 shows "setsum f A \<le> 0" |
653 proof (cases "finite A") |
686 proof (cases "finite A") |
654 case True thus ?thesis using np |
687 case True |
|
688 then show ?thesis |
|
689 using np |
655 proof induct |
690 proof induct |
656 case empty then show ?case by simp |
691 case empty |
|
692 then show ?case by simp |
657 next |
693 next |
658 case (insert x F) |
694 case (insert x F) |
659 then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono) |
695 then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono) |
660 with insert show ?case by simp |
696 with insert show ?case by simp |
661 qed |
697 qed |
662 next |
698 next |
663 case False thus ?thesis by simp |
699 case False thus ?thesis by simp |
664 qed |
700 qed |
665 |
701 |
666 lemma (in ordered_comm_monoid_add) setsum_nonneg_eq_0_iff: |
702 lemma setsum_nonneg_eq_0_iff: |
667 "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
703 "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" |
668 by (induct set: finite, simp) (simp add: add_nonneg_eq_0_iff setsum_nonneg) |
704 by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff setsum_nonneg) |
669 |
705 |
670 lemma (in ordered_comm_monoid_add) setsum_nonneg_0: |
706 lemma setsum_nonneg_0: |
671 "finite s \<Longrightarrow> (\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0) \<Longrightarrow> (\<Sum> i \<in> s. f i) = 0 \<Longrightarrow> i \<in> s \<Longrightarrow> f i = 0" |
707 "finite s \<Longrightarrow> (\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0) \<Longrightarrow> (\<Sum> i \<in> s. f i) = 0 \<Longrightarrow> i \<in> s \<Longrightarrow> f i = 0" |
672 by (simp add: setsum_nonneg_eq_0_iff) |
708 by (simp add: setsum_nonneg_eq_0_iff) |
673 |
709 |
674 lemma (in ordered_comm_monoid_add) setsum_nonneg_leq_bound: |
710 lemma setsum_nonneg_leq_bound: |
675 assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s" |
711 assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s" |
676 shows "f i \<le> B" |
712 shows "f i \<le> B" |
677 proof - |
713 proof - |
678 have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)" |
714 from assms have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)" |
679 using assms by (intro add_increasing2 setsum_nonneg) auto |
715 by (intro add_increasing2 setsum_nonneg) auto |
680 also have "\<dots> = B" |
716 also have "\<dots> = B" |
681 using setsum.remove[of s i f] assms by simp |
717 using setsum.remove[of s i f] assms by simp |
682 finally show ?thesis by auto |
718 finally show ?thesis by auto |
683 qed |
719 qed |
684 |
720 |
685 lemma (in ordered_comm_monoid_add) setsum_mono2: |
721 lemma setsum_mono2: |
686 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b" |
722 assumes fin: "finite B" |
|
723 and sub: "A \<subseteq> B" |
|
724 and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b" |
687 shows "setsum f A \<le> setsum f B" |
725 shows "setsum f A \<le> setsum f B" |
688 proof - |
726 proof - |
689 have "setsum f A \<le> setsum f A + setsum f (B-A)" |
727 have "setsum f A \<le> setsum f A + setsum f (B-A)" |
690 by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) |
728 by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) |
691 also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin] |
729 also from fin finite_subset[OF sub fin] have "\<dots> = setsum f (A \<union> (B-A))" |
692 by (simp add: setsum.union_disjoint del:Un_Diff_cancel) |
730 by (simp add: setsum.union_disjoint del: Un_Diff_cancel) |
693 also have "A \<union> (B-A) = B" using sub by blast |
731 also from sub have "A \<union> (B-A) = B" by blast |
694 finally show ?thesis . |
732 finally show ?thesis . |
695 qed |
733 qed |
696 |
734 |
697 lemma (in ordered_comm_monoid_add) setsum_le_included: |
735 lemma setsum_le_included: |
698 assumes "finite s" "finite t" |
736 assumes "finite s" "finite t" |
699 and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)" |
737 and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)" |
700 shows "setsum f s \<le> setsum g t" |
738 shows "setsum f s \<le> setsum g t" |
701 proof - |
739 proof - |
702 have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s" |
740 have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s" |
703 proof (rule setsum_mono) |
741 proof (rule setsum_mono) |
704 fix y assume "y \<in> s" |
742 fix y |
|
743 assume "y \<in> s" |
705 with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto |
744 with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto |
706 with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") |
745 with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") |
707 using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] |
746 using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] |
708 by (auto intro!: setsum_mono2) |
747 by (auto intro!: setsum_mono2) |
709 qed |
748 qed |
710 also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)" |
749 also have "\<dots> \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)" |
711 using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg) |
750 using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg) |
712 also have "... \<le> setsum g t" |
751 also have "\<dots> \<le> setsum g t" |
713 using assms by (auto simp: setsum_image_gen[symmetric]) |
752 using assms by (auto simp: setsum_image_gen[symmetric]) |
714 finally show ?thesis . |
753 finally show ?thesis . |
715 qed |
754 qed |
716 |
755 |
717 lemma (in ordered_comm_monoid_add) setsum_mono3: |
756 lemma setsum_mono3: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> setsum f A \<le> setsum f B" |
718 "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> setsum f A \<le> setsum f B" |
|
719 by (rule setsum_mono2) auto |
757 by (rule setsum_mono2) auto |
|
758 |
|
759 end |
720 |
760 |
721 lemma (in canonically_ordered_monoid_add) setsum_eq_0_iff [simp]: |
761 lemma (in canonically_ordered_monoid_add) setsum_eq_0_iff [simp]: |
722 "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)" |
762 "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)" |
723 by (intro ballI setsum_nonneg_eq_0_iff zero_le) |
763 by (intro ballI setsum_nonneg_eq_0_iff zero_le) |
724 |
764 |
725 lemma setsum_right_distrib: |
765 lemma setsum_right_distrib: |
726 fixes f :: "'a => ('b::semiring_0)" |
766 fixes f :: "'a \<Rightarrow> 'b::semiring_0" |
727 shows "r * setsum f A = setsum (%n. r * f n) A" |
767 shows "r * setsum f A = setsum (\<lambda>n. r * f n) A" |
728 proof (cases "finite A") |
|
729 case True |
|
730 thus ?thesis |
|
731 proof induct |
|
732 case empty thus ?case by simp |
|
733 next |
|
734 case (insert x A) thus ?case by (simp add: distrib_left) |
|
735 qed |
|
736 next |
|
737 case False thus ?thesis by simp |
|
738 qed |
|
739 |
|
740 lemma setsum_left_distrib: |
|
741 "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)" |
|
742 proof (cases "finite A") |
768 proof (cases "finite A") |
743 case True |
769 case True |
744 then show ?thesis |
770 then show ?thesis |
745 proof induct |
771 proof induct |
746 case empty thus ?case by simp |
772 case empty |
747 next |
773 then show ?case by simp |
748 case (insert x A) thus ?case by (simp add: distrib_right) |
774 next |
749 qed |
775 case insert |
750 next |
776 then show ?case by (simp add: distrib_left) |
751 case False thus ?thesis by simp |
777 qed |
752 qed |
778 next |
753 |
779 case False |
754 lemma setsum_divide_distrib: |
780 then show ?thesis by simp |
755 "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)" |
781 qed |
|
782 |
|
783 lemma setsum_left_distrib: "setsum f A * r = (\<Sum>n\<in>A. f n * r)" |
|
784 for r :: "'a::semiring_0" |
756 proof (cases "finite A") |
785 proof (cases "finite A") |
757 case True |
786 case True |
758 then show ?thesis |
787 then show ?thesis |
759 proof induct |
788 proof induct |
760 case empty thus ?case by simp |
789 case empty |
761 next |
790 then show ?case by simp |
762 case (insert x A) thus ?case by (simp add: add_divide_distrib) |
791 next |
763 qed |
792 case insert |
764 next |
793 then show ?case by (simp add: distrib_right) |
765 case False thus ?thesis by simp |
794 qed |
766 qed |
795 next |
767 |
796 case False |
768 lemma setsum_abs[iff]: |
797 then show ?thesis by simp |
769 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
798 qed |
770 shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A" |
799 |
771 proof (cases "finite A") |
800 lemma setsum_divide_distrib: "setsum f A / r = (\<Sum>n\<in>A. f n / r)" |
772 case True |
801 for r :: "'a::field" |
773 thus ?thesis |
802 proof (cases "finite A") |
|
803 case True |
|
804 then show ?thesis |
774 proof induct |
805 proof induct |
775 case empty thus ?case by simp |
806 case empty |
776 next |
807 then show ?case by simp |
777 case (insert x A) |
808 next |
778 thus ?case by (auto intro: abs_triangle_ineq order_trans) |
809 case insert |
779 qed |
810 then show ?case by (simp add: add_divide_distrib) |
780 next |
811 qed |
781 case False thus ?thesis by simp |
812 next |
782 qed |
813 case False |
783 |
814 then show ?thesis by simp |
784 lemma setsum_abs_ge_zero[iff]: |
815 qed |
785 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
816 |
786 shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A" |
817 lemma setsum_abs[iff]: "\<bar>setsum f A\<bar> \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A" |
|
818 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" |
|
819 proof (cases "finite A") |
|
820 case True |
|
821 then show ?thesis |
|
822 proof induct |
|
823 case empty |
|
824 then show ?case by simp |
|
825 next |
|
826 case insert |
|
827 then show ?case by (auto intro: abs_triangle_ineq order_trans) |
|
828 qed |
|
829 next |
|
830 case False |
|
831 then show ?thesis by simp |
|
832 qed |
|
833 |
|
834 lemma setsum_abs_ge_zero[iff]: "0 \<le> setsum (\<lambda>i. \<bar>f i\<bar>) A" |
|
835 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" |
787 by (simp add: setsum_nonneg) |
836 by (simp add: setsum_nonneg) |
788 |
837 |
789 lemma abs_setsum_abs[simp]: |
838 lemma abs_setsum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)" |
790 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
839 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" |
791 shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)" |
840 proof (cases "finite A") |
792 proof (cases "finite A") |
841 case True |
793 case True |
842 then show ?thesis |
794 thus ?thesis |
|
795 proof induct |
843 proof induct |
796 case empty thus ?case by simp |
844 case empty |
|
845 then show ?case by simp |
797 next |
846 next |
798 case (insert a A) |
847 case (insert a A) |
799 hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp |
848 then have "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp |
800 also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp |
849 also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp |
801 also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" |
850 also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg) |
802 by (simp del: abs_of_nonneg) |
851 also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp |
803 also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp |
|
804 finally show ?case . |
852 finally show ?case . |
805 qed |
853 qed |
806 next |
854 next |
807 case False thus ?thesis by simp |
855 case False |
808 qed |
856 then show ?thesis by simp |
809 |
857 qed |
810 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A" |
858 |
811 shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" |
859 lemma setsum_diff1_ring: |
|
860 fixes f :: "'b \<Rightarrow> 'a::ring" |
|
861 assumes "finite A" "a \<in> A" |
|
862 shows "setsum f (A - {a}) = setsum f A - (f a)" |
812 unfolding setsum.remove [OF assms] by auto |
863 unfolding setsum.remove [OF assms] by auto |
813 |
864 |
814 lemma setsum_product: |
865 lemma setsum_product: |
815 fixes f :: "'a => ('b::semiring_0)" |
866 fixes f :: "'a \<Rightarrow> 'b::semiring_0" |
816 shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" |
867 shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" |
817 by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute) |
868 by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute) |
818 |
869 |
819 lemma setsum_mult_setsum_if_inj: |
870 lemma setsum_mult_setsum_if_inj: |
820 fixes f :: "'a => ('b::semiring_0)" |
871 fixes f :: "'a \<Rightarrow> 'b::semiring_0" |
821 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==> |
872 shows "inj_on (\<lambda>(a, b). f a * g b) (A \<times> B) \<Longrightarrow> |
822 setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}" |
873 setsum f A * setsum g B = setsum id {f a * g b |a b. a \<in> A \<and> b \<in> B}" |
823 by(auto simp: setsum_product setsum.cartesian_product |
874 by(auto simp: setsum_product setsum.cartesian_product intro!: setsum.reindex_cong[symmetric]) |
824 intro!: setsum.reindex_cong[symmetric]) |
875 |
825 |
876 lemma setsum_SucD: |
826 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" |
877 assumes "setsum f A = Suc n" |
827 apply (case_tac "finite A") |
878 shows "\<exists>a\<in>A. 0 < f a" |
828 prefer 2 apply simp |
879 proof (cases "finite A") |
829 apply (erule rev_mp) |
880 case True |
830 apply (erule finite_induct, auto) |
881 from this assms show ?thesis by induct auto |
831 done |
882 next |
832 |
883 case False |
833 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow> |
884 with assms show ?thesis by simp |
834 setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))" |
885 qed |
835 apply(erule finite_induct) |
886 |
836 apply (auto simp add:add_is_1) |
887 lemma setsum_eq_Suc0_iff: |
837 done |
888 assumes "finite A" |
|
889 shows "setsum f A = Suc 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = Suc 0 \<and> (\<forall>b\<in>A. a \<noteq> b \<longrightarrow> f b = 0))" |
|
890 using assms by induct (auto simp add:add_is_1) |
838 |
891 |
839 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]] |
892 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]] |
840 |
893 |
841 lemma setsum_Un_nat: "finite A ==> finite B ==> |
894 lemma setsum_Un_nat: |
842 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" |
895 "finite A \<Longrightarrow> finite B \<Longrightarrow> setsum f (A \<union> B) = setsum f A + setsum f B - setsum f (A \<inter> B)" |
|
896 for f :: "'a \<Rightarrow> nat" |
843 \<comment> \<open>For the natural numbers, we have subtraction.\<close> |
897 \<comment> \<open>For the natural numbers, we have subtraction.\<close> |
844 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps) |
898 by (subst setsum.union_inter [symmetric]) (auto simp: algebra_simps) |
845 |
899 |
846 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = |
900 lemma setsum_diff1_nat: "setsum f (A - {a}) = (if a \<in> A then setsum f A - f a else setsum f A)" |
847 (if a:A then setsum f A - f a else setsum f A)" |
901 for f :: "'a \<Rightarrow> nat" |
848 apply (case_tac "finite A") |
902 proof (cases "finite A") |
849 prefer 2 apply simp |
903 case True |
850 apply (erule finite_induct) |
904 then show ?thesis |
851 apply (auto simp add: insert_Diff_if) |
905 apply induct |
852 apply (drule_tac a = a in mk_disjoint_insert, auto) |
906 apply (auto simp: insert_Diff_if) |
853 done |
907 apply (drule mk_disjoint_insert) |
|
908 apply auto |
|
909 done |
|
910 next |
|
911 case False |
|
912 then show ?thesis by simp |
|
913 qed |
854 |
914 |
855 lemma setsum_diff_nat: |
915 lemma setsum_diff_nat: |
856 assumes "finite B" and "B \<subseteq> A" |
916 fixes f :: "'a \<Rightarrow> nat" |
857 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
917 assumes "finite B" and "B \<subseteq> A" |
858 using assms |
918 shows "setsum f (A - B) = setsum f A - setsum f B" |
|
919 using assms |
859 proof induct |
920 proof induct |
860 show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp |
921 case empty |
861 next |
922 then show ?case by simp |
862 fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" |
923 next |
863 and xFinA: "insert x F \<subseteq> A" |
924 case (insert x F) |
864 and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F" |
925 note IH = \<open>F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F\<close> |
865 from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp |
926 from \<open>x \<notin> F\<close> \<open>insert x F \<subseteq> A\<close> have "x \<in> A - F" by simp |
866 from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
927 then have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
867 by (simp add: setsum_diff1_nat) |
928 by (simp add: setsum_diff1_nat) |
868 from xFinA have "F \<subseteq> A" by simp |
929 from \<open>insert x F \<subseteq> A\<close> have "F \<subseteq> A" by simp |
869 with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
930 with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
870 with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
931 with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
871 by simp |
932 by simp |
872 from xnotinF have "A - insert x F = (A - F) - {x}" by auto |
933 from \<open>x \<notin> F\<close> have "A - insert x F = (A - F) - {x}" by auto |
873 with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
934 with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
874 by simp |
935 by simp |
875 from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp |
936 from \<open>finite F\<close> \<open>x \<notin> F\<close> have "setsum f (insert x F) = setsum f F + f x" |
|
937 by simp |
876 with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
938 with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
877 by simp |
939 by simp |
878 thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp |
940 then show ?case by simp |
879 qed |
941 qed |
880 |
942 |
881 lemma setsum_comp_morphism: |
943 lemma setsum_comp_morphism: |
882 assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y" |
944 assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y" |
883 shows "setsum (h \<circ> g) A = h (setsum g A)" |
945 shows "setsum (h \<circ> g) A = h (setsum g A)" |
884 proof (cases "finite A") |
946 proof (cases "finite A") |
885 case False then show ?thesis by (simp add: assms) |
947 case False |
886 next |
948 then show ?thesis by (simp add: assms) |
887 case True then show ?thesis by (induct A) (simp_all add: assms) |
949 next |
888 qed |
950 case True |
889 |
951 then show ?thesis by (induct A) (simp_all add: assms) |
890 lemma (in comm_semiring_1) dvd_setsum: |
952 qed |
891 "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A" |
953 |
|
954 lemma (in comm_semiring_1) dvd_setsum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A" |
892 by (induct A rule: infinite_finite_induct) simp_all |
955 by (induct A rule: infinite_finite_induct) simp_all |
893 |
956 |
894 lemma (in ordered_comm_monoid_add) setsum_pos: |
957 lemma (in ordered_comm_monoid_add) setsum_pos: |
895 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I" |
958 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I" |
896 by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos) |
959 by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos) |
906 finally show ?thesis . |
969 finally show ?thesis . |
907 qed |
970 qed |
908 |
971 |
909 lemma setsum_cong_Suc: |
972 lemma setsum_cong_Suc: |
910 assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)" |
973 assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)" |
911 shows "setsum f A = setsum g A" |
974 shows "setsum f A = setsum g A" |
912 proof (rule setsum.cong) |
975 proof (rule setsum.cong) |
913 fix x assume "x \<in> A" |
976 fix x |
914 with assms(1) show "f x = g x" by (cases x) (auto intro!: assms(2)) |
977 assume "x \<in> A" |
|
978 with assms(1) show "f x = g x" |
|
979 by (cases x) (auto intro!: assms(2)) |
915 qed simp_all |
980 qed simp_all |
916 |
981 |
917 |
982 |
918 subsubsection \<open>Cardinality as special case of @{const setsum}\<close> |
983 subsubsection \<open>Cardinality as special case of @{const setsum}\<close> |
919 |
984 |
920 lemma card_eq_setsum: |
985 lemma card_eq_setsum: "card A = setsum (\<lambda>x. 1) A" |
921 "card A = setsum (\<lambda>x. 1) A" |
|
922 proof - |
986 proof - |
923 have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)" |
987 have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)" |
924 by (simp add: fun_eq_iff) |
988 by (simp add: fun_eq_iff) |
925 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)" |
989 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)" |
926 by (rule arg_cong) |
990 by (rule arg_cong) |
927 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A" |
991 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A" |
928 by (blast intro: fun_cong) |
992 by (blast intro: fun_cong) |
929 then show ?thesis by (simp add: card.eq_fold setsum.eq_fold) |
993 then show ?thesis |
930 qed |
994 by (simp add: card.eq_fold setsum.eq_fold) |
931 |
995 qed |
932 lemma setsum_constant [simp]: |
996 |
933 "(\<Sum>x \<in> A. y) = of_nat (card A) * y" |
997 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y" |
934 apply (cases "finite A") |
998 proof (cases "finite A") |
935 apply (erule finite_induct) |
999 case True |
936 apply (auto simp add: algebra_simps) |
1000 then show ?thesis by induct (auto simp: algebra_simps) |
937 done |
1001 next |
|
1002 case False |
|
1003 then show ?thesis by simp |
|
1004 qed |
938 |
1005 |
939 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A" |
1006 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A" |
940 using setsum.distrib[of f "\<lambda>_. 1" A] |
1007 using setsum.distrib[of f "\<lambda>_. 1" A] by simp |
941 by simp |
|
942 |
1008 |
943 lemma setsum_bounded_above: |
1009 lemma setsum_bounded_above: |
944 assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_comm_monoid_add})" |
1010 fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" |
|
1011 assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K" |
945 shows "setsum f A \<le> of_nat (card A) * K" |
1012 shows "setsum f A \<le> of_nat (card A) * K" |
946 proof (cases "finite A") |
1013 proof (cases "finite A") |
947 case True |
1014 case True |
948 thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp |
1015 then show ?thesis |
949 next |
1016 using le setsum_mono[where K=A and g = "\<lambda>x. K"] by simp |
950 case False thus ?thesis by simp |
1017 next |
|
1018 case False |
|
1019 then show ?thesis by simp |
951 qed |
1020 qed |
952 |
1021 |
953 lemma setsum_bounded_above_strict: |
1022 lemma setsum_bounded_above_strict: |
954 assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_comm_monoid_add,semiring_1})" |
1023 fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}" |
955 "card A > 0" |
1024 assumes "\<And>i. i\<in>A \<Longrightarrow> f i < K" "card A > 0" |
956 shows "setsum f A < of_nat (card A) * K" |
1025 shows "setsum f A < of_nat (card A) * K" |
957 using assms setsum_strict_mono[where A=A and g = "%x. K"] |
1026 using assms setsum_strict_mono[where A=A and g = "\<lambda>x. K"] |
958 by (simp add: card_gt_0_iff) |
1027 by (simp add: card_gt_0_iff) |
959 |
1028 |
960 lemma setsum_bounded_below: |
1029 lemma setsum_bounded_below: |
961 assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_comm_monoid_add}) \<le> f i" |
1030 fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" |
|
1031 assumes le: "\<And>i. i\<in>A \<Longrightarrow> K \<le> f i" |
962 shows "of_nat (card A) * K \<le> setsum f A" |
1032 shows "of_nat (card A) * K \<le> setsum f A" |
963 proof (cases "finite A") |
1033 proof (cases "finite A") |
964 case True |
1034 case True |
965 thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp |
1035 then show ?thesis |
966 next |
1036 using le setsum_mono[where K=A and f = "%x. K"] by simp |
967 case False thus ?thesis by simp |
1037 next |
|
1038 case False |
|
1039 then show ?thesis by simp |
968 qed |
1040 qed |
969 |
1041 |
970 lemma card_UN_disjoint: |
1042 lemma card_UN_disjoint: |
971 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
1043 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" |
972 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" |
1044 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" |
973 shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
1045 shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
974 proof - |
1046 proof - |
975 have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp |
1047 have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" |
976 with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant) |
1048 by simp |
|
1049 with assms show ?thesis |
|
1050 by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant) |
977 qed |
1051 qed |
978 |
1052 |
979 lemma card_Union_disjoint: |
1053 lemma card_Union_disjoint: |
980 "finite C ==> (ALL A:C. finite A) ==> |
1054 "finite C \<Longrightarrow> \<forall>A\<in>C. finite A \<Longrightarrow> \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow> |
981 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |
1055 card (\<Union>C) = setsum card C" |
982 ==> card (\<Union>C) = setsum card C" |
1056 by (frule card_UN_disjoint [of C id]) simp_all |
983 apply (frule card_UN_disjoint [of C id]) |
|
984 apply simp_all |
|
985 done |
|
986 |
1057 |
987 lemma setsum_multicount_gen: |
1058 lemma setsum_multicount_gen: |
988 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" |
1059 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" |
989 shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r") |
1060 shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" |
|
1061 (is "?l = ?r") |
990 proof- |
1062 proof- |
991 have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto |
1063 have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" |
992 also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)] |
1064 by auto |
|
1065 also have "\<dots> = ?r" |
|
1066 unfolding setsum.commute_restrict [OF assms(1-2)] |
993 using assms(3) by auto |
1067 using assms(3) by auto |
994 finally show ?thesis . |
1068 finally show ?thesis . |
995 qed |
1069 qed |
996 |
1070 |
997 lemma setsum_multicount: |
1071 lemma setsum_multicount: |
998 assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" |
1072 assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" |
999 shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") |
1073 shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") |
1000 proof- |
1074 proof- |
1001 have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms) |
1075 have "?l = setsum (\<lambda>i. k) T" |
|
1076 by (rule setsum_multicount_gen) (auto simp: assms) |
1002 also have "\<dots> = ?r" by (simp add: mult.commute) |
1077 also have "\<dots> = ?r" by (simp add: mult.commute) |
1003 finally show ?thesis by auto |
1078 finally show ?thesis by auto |
1004 qed |
1079 qed |
1005 |
1080 |
|
1081 |
1006 subsubsection \<open>Cardinality of products\<close> |
1082 subsubsection \<open>Cardinality of products\<close> |
1007 |
1083 |
1008 lemma card_SigmaI [simp]: |
1084 lemma card_SigmaI [simp]: |
1009 "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk> |
1085 "finite A \<Longrightarrow> \<forall>a\<in>A. finite (B a) \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
1010 \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
1086 by (simp add: card_eq_setsum setsum.Sigma del: setsum_constant) |
1011 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant) |
|
1012 |
1087 |
1013 (* |
1088 (* |
1014 lemma SigmaI_insert: "y \<notin> A ==> |
1089 lemma SigmaI_insert: "y \<notin> A ==> |
1015 (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))" |
1090 (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))" |
1016 by auto |
1091 by auto |
1017 *) |
1092 *) |
1018 |
1093 |
1019 lemma card_cartesian_product: "card (A \<times> B) = card(A) * card(B)" |
1094 lemma card_cartesian_product: "card (A \<times> B) = card A * card B" |
1020 by (cases "finite A \<and> finite B") |
1095 by (cases "finite A \<and> finite B") |
1021 (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) |
1096 (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) |
1022 |
1097 |
1023 lemma card_cartesian_product_singleton: "card({x} \<times> A) = card(A)" |
1098 lemma card_cartesian_product_singleton: "card ({x} \<times> A) = card A" |
1024 by (simp add: card_cartesian_product) |
1099 by (simp add: card_cartesian_product) |
1025 |
1100 |
1026 |
1101 |
1027 subsection \<open>Generalized product over a set\<close> |
1102 subsection \<open>Generalized product over a set\<close> |
1028 |
1103 |
1029 context comm_monoid_mult |
1104 context comm_monoid_mult |
1030 begin |
1105 begin |
1031 |
1106 |
1032 sublocale setprod: comm_monoid_set times 1 |
1107 sublocale setprod: comm_monoid_set times 1 |
1033 defines |
1108 defines setprod = setprod.F .. |
1034 setprod = setprod.F .. |
1109 |
1035 |
1110 abbreviation Setprod ("\<Prod>_" [1000] 999) |
1036 abbreviation |
1111 where "\<Prod>A \<equiv> setprod (\<lambda>x. x) A" |
1037 Setprod ("\<Prod>_" [1000] 999) where |
|
1038 "\<Prod>A \<equiv> setprod (\<lambda>x. x) A" |
|
1039 |
1112 |
1040 end |
1113 end |
1041 |
1114 |
1042 syntax (ASCII) |
1115 syntax (ASCII) |
1043 "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10) |
1116 "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD _:_./ _)" [0, 51, 10] 10) |
1124 qed |
1203 qed |
1125 |
1204 |
1126 end |
1205 end |
1127 |
1206 |
1128 lemma setprod_zero_iff [simp]: |
1207 lemma setprod_zero_iff [simp]: |
|
1208 fixes f :: "'b \<Rightarrow> 'a::semidom" |
1129 assumes "finite A" |
1209 assumes "finite A" |
1130 shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)" |
1210 shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)" |
1131 using assms by (induct A) (auto simp: no_zero_divisors) |
1211 using assms by (induct A) (auto simp: no_zero_divisors) |
1132 |
1212 |
1133 lemma (in semidom_divide) setprod_diff1: |
1213 lemma (in semidom_divide) setprod_diff1: |
1134 assumes "finite A" and "f a \<noteq> 0" |
1214 assumes "finite A" and "f a \<noteq> 0" |
1135 shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)" |
1215 shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)" |
1136 proof (cases "a \<notin> A") |
1216 proof (cases "a \<notin> A") |
1137 case True then show ?thesis by simp |
1217 case True |
1138 next |
1218 then show ?thesis by simp |
1139 case False with assms show ?thesis |
1219 next |
1140 proof (induct A rule: finite_induct) |
1220 case False |
1141 case empty then show ?case by simp |
1221 with assms show ?thesis |
|
1222 proof induct |
|
1223 case empty |
|
1224 then show ?case by simp |
1142 next |
1225 next |
1143 case (insert b B) |
1226 case (insert b B) |
1144 then show ?case |
1227 then show ?case |
1145 proof (cases "a = b") |
1228 proof (cases "a = b") |
1146 case True with insert show ?thesis by simp |
1229 case True |
|
1230 with insert show ?thesis by simp |
1147 next |
1231 next |
1148 case False with insert have "a \<in> B" by simp |
1232 case False |
|
1233 with insert have "a \<in> B" by simp |
1149 define C where "C = B - {a}" |
1234 define C where "C = B - {a}" |
1150 with \<open>finite B\<close> \<open>a \<in> B\<close> |
1235 with \<open>finite B\<close> \<open>a \<in> B\<close> have "B = insert a C" "finite C" "a \<notin> C" |
1151 have *: "B = insert a C" "finite C" "a \<notin> C" by auto |
1236 by auto |
1152 with insert show ?thesis by (auto simp add: insert_commute ac_simps) |
1237 with insert show ?thesis |
|
1238 by (auto simp add: insert_commute ac_simps) |
1153 qed |
1239 qed |
1154 qed |
1240 qed |
1155 qed |
1241 qed |
1156 |
1242 |
1157 lemma setsum_zero_power [simp]: |
1243 lemma setsum_zero_power [simp]: "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)" |
1158 fixes c :: "nat \<Rightarrow> 'a::division_ring" |
1244 for c :: "nat \<Rightarrow> 'a::division_ring" |
1159 shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)" |
1245 by (induct A rule: infinite_finite_induct) auto |
1160 apply (cases "finite A") |
|
1161 by (induction A rule: finite_induct) auto |
|
1162 |
1246 |
1163 lemma setsum_zero_power' [simp]: |
1247 lemma setsum_zero_power' [simp]: |
1164 fixes c :: "nat \<Rightarrow> 'a::field" |
1248 "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)" |
1165 shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)" |
1249 for c :: "nat \<Rightarrow> 'a::field" |
1166 using setsum_zero_power [of "\<lambda>i. c i / d i" A] |
1250 using setsum_zero_power [of "\<lambda>i. c i / d i" A] by auto |
1167 by auto |
|
1168 |
1251 |
1169 lemma (in field) setprod_inversef: |
1252 lemma (in field) setprod_inversef: |
1170 "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1253 "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1171 by (induct A rule: finite_induct) simp_all |
1254 by (induct A rule: finite_induct) simp_all |
1172 |
1255 |
1173 lemma (in field) setprod_dividef: |
1256 lemma (in field) setprod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A" |
1174 "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A" |
|
1175 using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib) |
1257 using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib) |
1176 |
1258 |
1177 lemma setprod_Un: |
1259 lemma setprod_Un: |
1178 fixes f :: "'b \<Rightarrow> 'a :: field" |
1260 fixes f :: "'b \<Rightarrow> 'a :: field" |
1179 assumes "finite A" and "finite B" |
1261 assumes "finite A" and "finite B" |
1180 and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0" |
1262 and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0" |
1181 shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)" |
1263 shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)" |
1182 proof - |
1264 proof - |
1183 from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)" |
1265 from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)" |
1184 by (simp add: setprod.union_inter [symmetric, of A B]) |
1266 by (simp add: setprod.union_inter [symmetric, of A B]) |
1185 with assms show ?thesis by simp |
1267 with assms show ?thesis |
1186 qed |
1268 by simp |
1187 |
1269 qed |
1188 lemma (in linordered_semidom) setprod_nonneg: |
1270 |
1189 "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A" |
1271 lemma (in linordered_semidom) setprod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A" |
1190 by (induct A rule: infinite_finite_induct) simp_all |
1272 by (induct A rule: infinite_finite_induct) simp_all |
1191 |
1273 |
1192 lemma (in linordered_semidom) setprod_pos: |
1274 lemma (in linordered_semidom) setprod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A" |
1193 "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A" |
|
1194 by (induct A rule: infinite_finite_induct) simp_all |
1275 by (induct A rule: infinite_finite_induct) simp_all |
1195 |
1276 |
1196 lemma (in linordered_semidom) setprod_mono: |
1277 lemma (in linordered_semidom) setprod_mono: |
1197 "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A" |
1278 "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A" |
1198 by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono) |
1279 by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono) |
1199 |
1280 |
1200 lemma (in linordered_semidom) setprod_mono_strict: |
1281 lemma (in linordered_semidom) setprod_mono_strict: |
1201 assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}" |
1282 assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}" |
1202 shows "setprod f A < setprod g A" |
1283 shows "setprod f A < setprod g A" |
1203 using assms |
1284 using assms |
1204 apply (induct A rule: finite_induct) |
1285 proof (induct A rule: finite_induct) |
1205 apply (simp add: ) |
1286 case empty |
1206 apply (force intro: mult_strict_mono' setprod_nonneg) |
1287 then show ?case by simp |
1207 done |
1288 next |
1208 |
1289 case insert |
1209 lemma (in linordered_field) abs_setprod: |
1290 then show ?case by (force intro: mult_strict_mono' setprod_nonneg) |
1210 "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)" |
1291 qed |
|
1292 |
|
1293 lemma (in linordered_field) abs_setprod: "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)" |
1211 by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult) |
1294 by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult) |
1212 |
1295 |
1213 lemma setprod_eq_1_iff [simp]: |
1296 lemma setprod_eq_1_iff [simp]: "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)" |
1214 "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))" |
1297 for f :: "'a \<Rightarrow> nat" |
1215 by (induct A rule: finite_induct) simp_all |
1298 by (induct A rule: finite_induct) simp_all |
1216 |
1299 |
1217 lemma setprod_pos_nat_iff [simp]: |
1300 lemma setprod_pos_nat_iff [simp]: "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)" |
1218 "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))" |
1301 for f :: "'a \<Rightarrow> nat" |
1219 using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero) |
1302 using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero) |
1220 |
1303 |
1221 lemma setprod_constant: |
1304 lemma setprod_constant: "(\<Prod>x\<in> A. y) = y ^ card A" |
1222 "(\<Prod>x\<in> A. (y::'a::comm_monoid_mult)) = y ^ card A" |
1305 for y :: "'a::comm_monoid_mult" |
1223 by (induct A rule: infinite_finite_induct) simp_all |
1306 by (induct A rule: infinite_finite_induct) simp_all |
1224 |
1307 |
1225 lemma setprod_power_distrib: |
1308 lemma setprod_power_distrib: "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A" |
1226 fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1" |
1309 for f :: "'a \<Rightarrow> 'b::comm_semiring_1" |
1227 shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A" |
1310 by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib) |
1228 proof (cases "finite A") |
1311 |
1229 case True then show ?thesis |
1312 lemma power_setsum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" |
1230 by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) |
|
1231 next |
|
1232 case False then show ?thesis |
|
1233 by simp |
|
1234 qed |
|
1235 |
|
1236 lemma power_setsum: |
|
1237 "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" |
|
1238 by (induct A rule: infinite_finite_induct) (simp_all add: power_add) |
1313 by (induct A rule: infinite_finite_induct) (simp_all add: power_add) |
1239 |
1314 |
1240 lemma setprod_gen_delta: |
1315 lemma setprod_gen_delta: |
1241 assumes fS: "finite S" |
1316 fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult" |
1242 shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" |
1317 assumes fin: "finite S" |
1243 proof- |
1318 shows "setprod (\<lambda>k. if k = a then b k else c) S = |
|
1319 (if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)" |
|
1320 proof - |
1244 let ?f = "(\<lambda>k. if k=a then b k else c)" |
1321 let ?f = "(\<lambda>k. if k=a then b k else c)" |
1245 {assume a: "a \<notin> S" |
1322 show ?thesis |
1246 hence "\<forall> k\<in> S. ?f k = c" by simp |
1323 proof (cases "a \<in> S") |
1247 hence ?thesis using a setprod_constant by simp } |
1324 case False |
1248 moreover |
1325 then have "\<forall> k\<in> S. ?f k = c" by simp |
1249 {assume a: "a \<in> S" |
1326 with False show ?thesis by (simp add: setprod_constant) |
|
1327 next |
|
1328 case True |
1250 let ?A = "S - {a}" |
1329 let ?A = "S - {a}" |
1251 let ?B = "{a}" |
1330 let ?B = "{a}" |
1252 have eq: "S = ?A \<union> ?B" using a by blast |
1331 from True have eq: "S = ?A \<union> ?B" by blast |
1253 have dj: "?A \<inter> ?B = {}" by simp |
1332 have disjoint: "?A \<inter> ?B = {}" by simp |
1254 from fS have fAB: "finite ?A" "finite ?B" by auto |
1333 from fin have fin': "finite ?A" "finite ?B" by auto |
1255 have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A" |
1334 have f_A0: "setprod ?f ?A = setprod (\<lambda>i. c) ?A" |
1256 by (rule setprod.cong) auto |
1335 by (rule setprod.cong) auto |
1257 have cA: "card ?A = card S - 1" using fS a by auto |
1336 from fin True have card_A: "card ?A = card S - 1" by auto |
1258 have fA1: "setprod ?f ?A = c ^ card ?A" |
1337 have f_A1: "setprod ?f ?A = c ^ card ?A" |
1259 unfolding fA0 by (rule setprod_constant) |
1338 unfolding f_A0 by (rule setprod_constant) |
1260 have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" |
1339 have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" |
1261 using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] |
1340 using setprod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]] |
1262 by simp |
1341 by simp |
1263 then have ?thesis using a cA |
1342 with True card_A show ?thesis |
1264 by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} |
1343 by (simp add: f_A1 field_simps cong add: setprod.cong cong del: if_weak_cong) |
1265 ultimately show ?thesis by blast |
1344 qed |
1266 qed |
1345 qed |
1267 |
1346 |
1268 end |
1347 end |