1(* Title: HOL/Groups_Big.thy 2 Author: Tobias Nipkow 3 Author: Lawrence C Paulson 4 Author: Markus Wenzel 5 Author: Jeremy Avigad 6*) 7 8section \<open>Big sum and product over finite (non-empty) sets\<close> 9 10theory Groups_Big 11 imports Power 12begin 13 14subsection \<open>Generic monoid operation over a set\<close> 15 16locale comm_monoid_set = comm_monoid 17begin 18 19subsubsection \<open>Standard sum or product indexed by a finite set\<close> 20 21interpretation comp_fun_commute f 22 by standard (simp add: fun_eq_iff left_commute) 23 24interpretation comp?: comp_fun_commute "f \<circ> g" 25 by (fact comp_comp_fun_commute) 26 27definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" 28 where eq_fold: "F g A = Finite_Set.fold (f \<circ> g) \<^bold>1 A" 29 30lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F g A = \<^bold>1" 31 by (simp add: eq_fold) 32 33lemma empty [simp]: "F g {} = \<^bold>1" 34 by (simp add: eq_fold) 35 36lemma insert [simp]: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g A" 37 by (simp add: eq_fold) 38 39lemma remove: 40 assumes "finite A" and "x \<in> A" 41 shows "F g A = g x \<^bold>* F g (A - {x})" 42proof - 43 from \<open>x \<in> A\<close> obtain B where B: "A = insert x B" and "x \<notin> B" 44 by (auto dest: mk_disjoint_insert) 45 moreover from \<open>finite A\<close> B have "finite B" by simp 46 ultimately show ?thesis by simp 47qed 48 49lemma insert_remove: "finite A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g (A - {x})" 50 by (cases "x \<in> A") (simp_all add: remove insert_absorb) 51 52lemma insert_if: "finite A \<Longrightarrow> F g (insert x A) = (if x \<in> A then F g A else g x \<^bold>* F g A)" 53 by (cases "x \<in> A") (simp_all add: insert_absorb) 54 55lemma neutral: "\<forall>x\<in>A. g x = \<^bold>1 \<Longrightarrow> F g A = \<^bold>1" 56 by (induct A rule: infinite_finite_induct) simp_all 57 58lemma neutral_const [simp]: "F (\<lambda>_. \<^bold>1) A = \<^bold>1" 59 by (simp add: neutral) 60 61lemma union_inter: 62 assumes "finite A" and "finite B" 63 shows "F g (A \<union> B) \<^bold>* F g (A \<inter> B) = F g A \<^bold>* F g B" 64 \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close> 65 using assms 66proof (induct A) 67 case empty 68 then show ?case by simp 69next 70 case (insert x A) 71 then show ?case 72 by (auto simp: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute) 73qed 74 75corollary union_inter_neutral: 76 assumes "finite A" and "finite B" 77 and "\<forall>x \<in> A \<inter> B. g x = \<^bold>1" 78 shows "F g (A \<union> B) = F g A \<^bold>* F g B" 79 using assms by (simp add: union_inter [symmetric] neutral) 80 81corollary union_disjoint: 82 assumes "finite A" and "finite B" 83 assumes "A \<inter> B = {}" 84 shows "F g (A \<union> B) = F g A \<^bold>* F g B" 85 using assms by (simp add: union_inter_neutral) 86 87lemma union_diff2: 88 assumes "finite A" and "finite B" 89 shows "F g (A \<union> B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \<inter> B)" 90proof - 91 have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B" 92 by auto 93 with assms show ?thesis 94 by simp (subst union_disjoint, auto)+ 95qed 96 97lemma subset_diff: 98 assumes "B \<subseteq> A" and "finite A" 99 shows "F g A = F g (A - B) \<^bold>* F g B" 100proof - 101 from assms have "finite (A - B)" by auto 102 moreover from assms have "finite B" by (rule finite_subset) 103 moreover from assms have "(A - B) \<inter> B = {}" by auto 104 ultimately have "F g (A - B \<union> B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint) 105 moreover from assms have "A \<union> B = A" by auto 106 ultimately show ?thesis by simp 107qed 108 109lemma Int_Diff: 110 assumes "finite A" 111 shows "F g A = F g (A \<inter> B) \<^bold>* F g (A - B)" 112 by (subst subset_diff [where B = "A - B"]) (auto simp: Diff_Diff_Int assms) 113 114lemma setdiff_irrelevant: 115 assumes "finite A" 116 shows "F g (A - {x. g x = z}) = F g A" 117 using assms by (induct A) (simp_all add: insert_Diff_if) 118 119lemma not_neutral_contains_not_neutral: 120 assumes "F g A \<noteq> \<^bold>1" 121 obtains a where "a \<in> A" and "g a \<noteq> \<^bold>1" 122proof - 123 from assms have "\<exists>a\<in>A. g a \<noteq> \<^bold>1" 124 proof (induct A rule: infinite_finite_induct) 125 case infinite 126 then show ?case by simp 127 next 128 case empty 129 then show ?case by simp 130 next 131 case (insert a A) 132 then show ?case by fastforce 133 qed 134 with that show thesis by blast 135qed 136 137lemma reindex: 138 assumes "inj_on h A" 139 shows "F g (h ` A) = F (g \<circ> h) A" 140proof (cases "finite A") 141 case True 142 with assms show ?thesis 143 by (simp add: eq_fold fold_image comp_assoc) 144next 145 case False 146 with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD) 147 with False show ?thesis by simp 148qed 149 150lemma cong [fundef_cong]: 151 assumes "A = B" 152 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" 153 shows "F g A = F h B" 154 using g_h unfolding \<open>A = B\<close> 155 by (induct B rule: infinite_finite_induct) auto 156 157lemma cong_simp [cong]: 158 "\<lbrakk> A = B; \<And>x. x \<in> B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F (\<lambda>x. g x) A = F (\<lambda>x. h x) B" 159by (rule cong) (simp_all add: simp_implies_def) 160 161lemma reindex_cong: 162 assumes "inj_on l B" 163 assumes "A = l ` B" 164 assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x" 165 shows "F g A = F h B" 166 using assms by (simp add: reindex) 167 168lemma UNION_disjoint: 169 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" 170 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" 171 shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I" 172 using assms 173proof (induction rule: finite_induct) 174 case (insert i I) 175 then have "\<forall>j\<in>I. j \<noteq> i" 176 by blast 177 with insert.prems have "A i \<inter> \<Union>(A ` I) = {}" 178 by blast 179 with insert show ?case 180 by (simp add: union_disjoint) 181qed auto 182 183lemma Union_disjoint: 184 assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}" 185 shows "F g (\<Union>C) = (F \<circ> F) g C" 186proof (cases "finite C") 187 case True 188 from UNION_disjoint [OF this assms] show ?thesis by simp 189next 190 case False 191 then show ?thesis by (auto dest: finite_UnionD intro: infinite) 192qed 193 194lemma distrib: "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A" 195 by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute) 196 197lemma Sigma: 198 assumes "finite A" "\<forall>x\<in>A. finite (B x)" 199 shows "F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)" 200 unfolding Sigma_def 201proof (subst UNION_disjoint) 202 show "F (\<lambda>x. F (g x) (B x)) A = F (\<lambda>x. F (\<lambda>(x, y). g x y) (\<Union>y\<in>B x. {(x, y)})) A" 203 proof (rule cong [OF refl]) 204 show "F (g x) (B x) = F (\<lambda>(x, y). g x y) (\<Union>y\<in>B x. {(x, y)})" 205 if "x \<in> A" for x 206 using that assms by (simp add: UNION_disjoint) 207 qed 208qed (use assms in auto) 209 210lemma related: 211 assumes Re: "R \<^bold>1 \<^bold>1" 212 and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)" 213 and fin: "finite S" 214 and R_h_g: "\<forall>x\<in>S. R (h x) (g x)" 215 shows "R (F h S) (F g S)" 216 using fin by (rule finite_subset_induct) (use assms in auto) 217 218lemma mono_neutral_cong_left: 219 assumes "finite T" 220 and "S \<subseteq> T" 221 and "\<forall>i \<in> T - S. h i = \<^bold>1" 222 and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" 223 shows "F g S = F h T" 224proof- 225 have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast 226 have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast 227 from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)" 228 by (auto intro: finite_subset) 229 show ?thesis using assms(4) 230 by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)]) 231qed 232 233lemma mono_neutral_cong_right: 234 "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> 235 F g T = F h S" 236 by (auto intro!: mono_neutral_cong_left [symmetric]) 237 238lemma 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" 239 by (blast intro: mono_neutral_cong_left) 240 241lemma 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" 242 by (blast intro!: mono_neutral_left [symmetric]) 243 244lemma mono_neutral_cong: 245 assumes [simp]: "finite T" "finite S" 246 and *: "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1" "\<And>i. i \<in> S - T \<Longrightarrow> g i = \<^bold>1" 247 and gh: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x = h x" 248 shows "F g S = F h T" 249proof- 250 have "F g S = F g (S \<inter> T)" 251 by(rule mono_neutral_right)(auto intro: *) 252 also have "\<dots> = F h (S \<inter> T)" using refl gh by(rule cong) 253 also have "\<dots> = F h T" 254 by(rule mono_neutral_left)(auto intro: *) 255 finally show ?thesis . 256qed 257 258lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T" 259 by (auto simp: bij_betw_def reindex) 260 261lemma reindex_bij_witness: 262 assumes witness: 263 "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a" 264 "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T" 265 "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b" 266 "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S" 267 assumes eq: 268 "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a" 269 shows "F g S = F h T" 270proof - 271 have "bij_betw j S T" 272 using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto 273 moreover have "F g S = F (\<lambda>x. h (j x)) S" 274 by (intro cong) (auto simp: eq) 275 ultimately show ?thesis 276 by (simp add: reindex_bij_betw) 277qed 278 279lemma reindex_bij_betw_not_neutral: 280 assumes fin: "finite S'" "finite T'" 281 assumes bij: "bij_betw h (S - S') (T - T')" 282 assumes nn: 283 "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z" 284 "\<And>b. b \<in> T' \<Longrightarrow> g b = z" 285 shows "F (\<lambda>x. g (h x)) S = F g T" 286proof - 287 have [simp]: "finite S \<longleftrightarrow> finite T" 288 using bij_betw_finite[OF bij] fin by auto 289 show ?thesis 290 proof (cases "finite S") 291 case True 292 with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')" 293 by (intro mono_neutral_cong_right) auto 294 also have "\<dots> = F g (T - T')" 295 using bij by (rule reindex_bij_betw) 296 also have "\<dots> = F g T" 297 using nn \<open>finite S\<close> by (intro mono_neutral_cong_left) auto 298 finally show ?thesis . 299 next 300 case False 301 then show ?thesis by simp 302 qed 303qed 304 305lemma reindex_nontrivial: 306 assumes "finite A" 307 and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = \<^bold>1" 308 shows "F g (h ` A) = F (g \<circ> h) A" 309proof (subst reindex_bij_betw_not_neutral [symmetric]) 310 show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = \<^bold>1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = \<^bold>1})" 311 using nz by (auto intro!: inj_onI simp: bij_betw_def) 312qed (use \<open>finite A\<close> in auto) 313 314lemma reindex_bij_witness_not_neutral: 315 assumes fin: "finite S'" "finite T'" 316 assumes witness: 317 "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a" 318 "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'" 319 "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b" 320 "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'" 321 assumes nn: 322 "\<And>a. a \<in> S' \<Longrightarrow> g a = z" 323 "\<And>b. b \<in> T' \<Longrightarrow> h b = z" 324 assumes eq: 325 "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a" 326 shows "F g S = F h T" 327proof - 328 have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))" 329 using witness by (intro bij_betw_byWitness[where f'=i]) auto 330 have F_eq: "F g S = F (\<lambda>x. h (j x)) S" 331 by (intro cong) (auto simp: eq) 332 show ?thesis 333 unfolding F_eq using fin nn eq 334 by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto 335qed 336 337lemma delta_remove: 338 assumes fS: "finite S" 339 shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))" 340proof - 341 let ?f = "(\<lambda>k. if k = a then b k else c k)" 342 show ?thesis 343 proof (cases "a \<in> S") 344 case False 345 then have "\<forall>k\<in>S. ?f k = c k" by simp 346 with False show ?thesis by simp 347 next 348 case True 349 let ?A = "S - {a}" 350 let ?B = "{a}" 351 from True have eq: "S = ?A \<union> ?B" by blast 352 have dj: "?A \<inter> ?B = {}" by simp 353 from fS have fAB: "finite ?A" "finite ?B" by auto 354 have "F ?f S = F ?f ?A \<^bold>* F ?f ?B" 355 using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp 356 with True show ?thesis 357 using comm_monoid_set.remove comm_monoid_set_axioms fS by fastforce 358 qed 359qed 360 361lemma delta [simp]: 362 assumes fS: "finite S" 363 shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" 364 by (simp add: delta_remove [OF assms]) 365 366lemma delta' [simp]: 367 assumes fin: "finite S" 368 shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)" 369 using delta [OF fin, of a b, symmetric] by (auto intro: cong) 370 371lemma If_cases: 372 fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a" 373 assumes fin: "finite A" 374 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})" 375proof - 376 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}) = {}" 377 by blast+ 378 from fin have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto 379 let ?g = "\<lambda>x. if P x then h x else g x" 380 from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis 381 by (subst (1 2) cong) simp_all 382qed 383 384lemma cartesian_product: "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)" 385proof (cases "A = {} \<or> B = {}") 386 case True 387 then show ?thesis 388 by auto 389next 390 case False 391 then have "A \<noteq> {}" "B \<noteq> {}" by auto 392 show ?thesis 393 proof (cases "finite A \<and> finite B") 394 case True 395 then show ?thesis 396 by (simp add: Sigma) 397 next 398 case False 399 then consider "infinite A" | "infinite B" by auto 400 then have "infinite (A \<times> B)" 401 by cases (use \<open>A \<noteq> {}\<close> \<open>B \<noteq> {}\<close> in \<open>auto dest: finite_cartesian_productD1 finite_cartesian_productD2\<close>) 402 then show ?thesis 403 using False by auto 404 qed 405qed 406 407lemma inter_restrict: 408 assumes "finite A" 409 shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A" 410proof - 411 let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1" 412 have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1" by simp 413 moreover have "A \<inter> B \<subseteq> A" by blast 414 ultimately have "F ?g (A \<inter> B) = F ?g A" 415 using \<open>finite A\<close> by (intro mono_neutral_left) auto 416 then show ?thesis by simp 417qed 418 419lemma inter_filter: 420 "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A" 421 by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def) 422 423lemma Union_comp: 424 assumes "\<forall>A \<in> B. finite A" 425 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" 426 shows "F g (\<Union>B) = (F \<circ> F) g B" 427 using assms 428proof (induct B rule: infinite_finite_induct) 429 case (infinite A) 430 then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD) 431 with infinite show ?case by simp 432next 433 case empty 434 then show ?case by simp 435next 436 case (insert A B) 437 then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B" 438 and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1" 439 and H: "F g (\<Union>B) = (F \<circ> F) g B" by auto 440 then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)" 441 by (simp add: union_inter_neutral) 442 with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case 443 by (simp add: H) 444qed 445 446lemma swap: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B" 447 unfolding cartesian_product 448 by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto 449 450lemma swap_restrict: 451 "finite A \<Longrightarrow> finite B \<Longrightarrow> 452 F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B" 453 by (simp add: inter_filter) (rule swap) 454 455lemma image_gen: 456 assumes fin: "finite S" 457 shows "F h S = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)" 458proof - 459 have "{y. y\<in> g`S \<and> g x = y} = {g x}" if "x \<in> S" for x 460 using that by auto 461 then have "F h S = F (\<lambda>x. F (\<lambda>y. h x) {y. y\<in> g`S \<and> g x = y}) S" 462 by simp 463 also have "\<dots> = F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) (g ` S)" 464 by (rule swap_restrict [OF fin finite_imageI [OF fin]]) 465 finally show ?thesis . 466qed 467 468lemma group: 469 assumes fS: "finite S" and fT: "finite T" and fST: "g ` S \<subseteq> T" 470 shows "F (\<lambda>y. F h {x. x \<in> S \<and> g x = y}) T = F h S" 471 unfolding image_gen[OF fS, of h g] 472 by (auto intro: neutral mono_neutral_right[OF fT fST]) 473 474lemma Plus: 475 fixes A :: "'b set" and B :: "'c set" 476 assumes fin: "finite A" "finite B" 477 shows "F g (A <+> B) = F (g \<circ> Inl) A \<^bold>* F (g \<circ> Inr) B" 478proof - 479 have "A <+> B = Inl ` A \<union> Inr ` B" by auto 480 moreover from fin have "finite (Inl ` A)" "finite (Inr ` B)" by auto 481 moreover have "Inl ` A \<inter> Inr ` B = {}" by auto 482 moreover have "inj_on Inl A" "inj_on Inr B" by (auto intro: inj_onI) 483 ultimately show ?thesis 484 using fin by (simp add: union_disjoint reindex) 485qed 486 487lemma same_carrier: 488 assumes "finite C" 489 assumes subset: "A \<subseteq> C" "B \<subseteq> C" 490 assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1" 491 shows "F g A = F h B \<longleftrightarrow> F g C = F h C" 492proof - 493 have "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)" 494 using \<open>finite C\<close> subset by (auto elim: finite_subset) 495 from subset have [simp]: "A - (C - A) = A" by auto 496 from subset have [simp]: "B - (C - B) = B" by auto 497 from subset have "C = A \<union> (C - A)" by auto 498 then have "F g C = F g (A \<union> (C - A))" by simp 499 also have "\<dots> = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \<inter> (C - A))" 500 using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2) 501 finally have *: "F g C = F g A" using trivial by simp 502 from subset have "C = B \<union> (C - B)" by auto 503 then have "F h C = F h (B \<union> (C - B))" by simp 504 also have "\<dots> = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \<inter> (C - B))" 505 using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2) 506 finally have "F h C = F h B" 507 using trivial by simp 508 with * show ?thesis by simp 509qed 510 511lemma same_carrierI: 512 assumes "finite C" 513 assumes subset: "A \<subseteq> C" "B \<subseteq> C" 514 assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1" 515 assumes "F g C = F h C" 516 shows "F g A = F h B" 517 using assms same_carrier [of C A B] by simp 518 519lemma eq_general: 520 assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>!x. x \<in> A \<and> h x = y" and A: "\<And>x. x \<in> A \<Longrightarrow> h x \<in> B \<and> \<gamma>(h x) = \<phi> x" 521 shows "F \<phi> A = F \<gamma> B" 522proof - 523 have eq: "B = h ` A" 524 by (auto dest: assms) 525 have h: "inj_on h A" 526 using assms by (blast intro: inj_onI) 527 have "F \<phi> A = F (\<gamma> \<circ> h) A" 528 using A by auto 529 also have "\<dots> = F \<gamma> B" 530 by (simp add: eq reindex h) 531 finally show ?thesis . 532qed 533 534lemma eq_general_inverses: 535 assumes B: "\<And>y. y \<in> B \<Longrightarrow> k y \<in> A \<and> h(k y) = y" and A: "\<And>x. x \<in> A \<Longrightarrow> h x \<in> B \<and> k(h x) = x \<and> \<gamma>(h x) = \<phi> x" 536 shows "F \<phi> A = F \<gamma> B" 537 by (rule eq_general [where h=h]) (force intro: dest: A B)+ 538 539subsubsection \<open>HOL Light variant: sum/product indexed by the non-neutral subset\<close> 540text \<open>NB only a subset of the properties above are proved\<close> 541 542definition G :: "['b \<Rightarrow> 'a,'b set] \<Rightarrow> 'a" 543 where "G p I \<equiv> if finite {x \<in> I. p x \<noteq> \<^bold>1} then F p {x \<in> I. p x \<noteq> \<^bold>1} else \<^bold>1" 544 545lemma finite_Collect_op: 546 shows "\<lbrakk>finite {i \<in> I. x i \<noteq> \<^bold>1}; finite {i \<in> I. y i \<noteq> \<^bold>1}\<rbrakk> \<Longrightarrow> finite {i \<in> I. x i \<^bold>* y i \<noteq> \<^bold>1}" 547 apply (rule finite_subset [where B = "{i \<in> I. x i \<noteq> \<^bold>1} \<union> {i \<in> I. y i \<noteq> \<^bold>1}"]) 548 using left_neutral by force+ 549 550lemma empty' [simp]: "G p {} = \<^bold>1" 551 by (auto simp: G_def) 552 553lemma eq_sum [simp]: "finite I \<Longrightarrow> G p I = F p I" 554 by (auto simp: G_def intro: mono_neutral_cong_left) 555 556lemma insert' [simp]: 557 assumes "finite {x \<in> I. p x \<noteq> \<^bold>1}" 558 shows "G p (insert i I) = (if i \<in> I then G p I else p i \<^bold>* G p I)" 559proof - 560 have "{x. x = i \<and> p x \<noteq> \<^bold>1 \<or> x \<in> I \<and> p x \<noteq> \<^bold>1} = (if p i = \<^bold>1 then {x \<in> I. p x \<noteq> \<^bold>1} else insert i {x \<in> I. p x \<noteq> \<^bold>1})" 561 by auto 562 then show ?thesis 563 using assms by (simp add: G_def conj_disj_distribR insert_absorb) 564qed 565 566lemma distrib_triv': 567 assumes "finite I" 568 shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I" 569 by (simp add: assms local.distrib) 570 571lemma non_neutral': "G g {x \<in> I. g x \<noteq> \<^bold>1} = G g I" 572 by (simp add: G_def) 573 574lemma distrib': 575 assumes "finite {x \<in> I. g x \<noteq> \<^bold>1}" "finite {x \<in> I. h x \<noteq> \<^bold>1}" 576 shows "G (\<lambda>i. g i \<^bold>* h i) I = G g I \<^bold>* G h I" 577proof - 578 have "a \<^bold>* a \<noteq> a \<Longrightarrow> a \<noteq> \<^bold>1" for a 579 by auto 580 then have "G (\<lambda>i. g i \<^bold>* h i) I = G (\<lambda>i. g i \<^bold>* h i) ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1})" 581 using assms by (force simp: G_def finite_Collect_op intro!: mono_neutral_cong) 582 also have "\<dots> = G g I \<^bold>* G h I" 583 proof - 584 have "F g ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G g I" 585 "F h ({i \<in> I. g i \<noteq> \<^bold>1} \<union> {i \<in> I. h i \<noteq> \<^bold>1}) = G h I" 586 by (auto simp: G_def assms intro: mono_neutral_right) 587 then show ?thesis 588 using assms by (simp add: distrib) 589 qed 590 finally show ?thesis . 591qed 592 593lemma cong': 594 assumes "A = B" 595 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" 596 shows "G g A = G h B" 597 using assms by (auto simp: G_def cong: conj_cong intro: cong) 598 599 600lemma mono_neutral_cong_left': 601 assumes "S \<subseteq> T" 602 and "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1" 603 and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" 604 shows "G g S = G h T" 605proof - 606 have *: "{x \<in> S. g x \<noteq> \<^bold>1} = {x \<in> T. h x \<noteq> \<^bold>1}" 607 using assms by (metis DiffI subset_eq) 608 then have "finite {x \<in> S. g x \<noteq> \<^bold>1} = finite {x \<in> T. h x \<noteq> \<^bold>1}" 609 by simp 610 then show ?thesis 611 using assms by (auto simp add: G_def * intro: cong) 612qed 613 614lemma mono_neutral_cong_right': 615 "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> 616 G g T = G h S" 617 by (auto intro!: mono_neutral_cong_left' [symmetric]) 618 619lemma mono_neutral_left': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g S = G g T" 620 by (blast intro: mono_neutral_cong_left') 621 622lemma mono_neutral_right': "S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> G g T = G g S" 623 by (blast intro!: mono_neutral_left' [symmetric]) 624 625end 626 627 628subsection \<open>Generalized summation over a set\<close> 629 630context comm_monoid_add 631begin 632 633sublocale sum: comm_monoid_set plus 0 634 defines sum = sum.F and sum' = sum.G .. 635 636abbreviation Sum ("\<Sum>") 637 where "\<Sum> \<equiv> sum (\<lambda>x. x)" 638 639end 640 641text \<open>Now: lots of fancy syntax. First, \<^term>\<open>sum (\<lambda>x. e) A\<close> is written \<open>\<Sum>x\<in>A. e\<close>.\<close> 642 643syntax (ASCII) 644 "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10) 645syntax 646 "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10) 647translations \<comment> \<open>Beware of argument permutation!\<close> 648 "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A" 649 650text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close> 651 652syntax (ASCII) 653 "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0, 0, 10] 10) 654syntax 655 "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10) 656translations 657 "\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}" 658 659print_translation \<open> 660let 661 fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ Abs (y, Ty, P)] = 662 if x <> y then raise Match 663 else 664 let 665 val x' = Syntax_Trans.mark_bound_body (x, Tx); 666 val t' = subst_bound (x', t); 667 val P' = subst_bound (x', P); 668 in 669 Syntax.const \<^syntax_const>\<open>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' 670 end 671 | sum_tr' _ = raise Match; 672in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end 673\<close> 674 675 676subsubsection \<open>Properties in more restricted classes of structures\<close> 677 678lemma sum_Un: 679 "finite A \<Longrightarrow> finite B \<Longrightarrow> sum f (A \<union> B) = sum f A + sum f B - sum f (A \<inter> B)" 680 for f :: "'b \<Rightarrow> 'a::ab_group_add" 681 by (subst sum.union_inter [symmetric]) (auto simp add: algebra_simps) 682 683lemma sum_Un2: 684 assumes "finite (A \<union> B)" 685 shows "sum f (A \<union> B) = sum f (A - B) + sum f (B - A) + sum f (A \<inter> B)" 686proof - 687 have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B" 688 by auto 689 with assms show ?thesis 690 by simp (subst sum.union_disjoint, auto)+ 691qed 692 693lemma sum_diff1: 694 fixes f :: "'b \<Rightarrow> 'a::ab_group_add" 695 assumes "finite A" 696 shows "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)" 697 using assms by induct (auto simp: insert_Diff_if) 698 699lemma sum_diff: 700 fixes f :: "'b \<Rightarrow> 'a::ab_group_add" 701 assumes "finite A" "B \<subseteq> A" 702 shows "sum f (A - B) = sum f A - sum f B" 703proof - 704 from assms(2,1) have "finite B" by (rule finite_subset) 705 from this \<open>B \<subseteq> A\<close> 706 show ?thesis 707 proof induct 708 case empty 709 thus ?case by simp 710 next 711 case (insert x F) 712 with \<open>finite A\<close> \<open>finite B\<close> show ?case 713 by (simp add: Diff_insert[where a=x and B=F] sum_diff1 insert_absorb) 714 qed 715qed 716 717lemma sum_diff1'_aux: 718 fixes f :: "'a \<Rightarrow> 'b::ab_group_add" 719 assumes "finite F" "{i \<in> I. f i \<noteq> 0} \<subseteq> F" 720 shows "sum' f (I - {i}) = (if i \<in> I then sum' f I - f i else sum' f I)" 721 using assms 722proof induct 723 case (insert x F) 724 have 1: "finite {x \<in> I. f x \<noteq> 0} \<Longrightarrow> finite {x \<in> I. x \<noteq> i \<and> f x \<noteq> 0}" 725 by (erule rev_finite_subset) auto 726 have 2: "finite {x \<in> I. x \<noteq> i \<and> f x \<noteq> 0} \<Longrightarrow> finite {x \<in> I. f x \<noteq> 0}" 727 apply (drule finite_insert [THEN iffD2]) 728 by (erule rev_finite_subset) auto 729 have 3: "finite {i \<in> I. f i \<noteq> 0}" 730 using finite_subset insert by blast 731 show ?case 732 using insert sum_diff1 [of "{i \<in> I. f i \<noteq> 0}" f i] 733 by (auto simp: sum.G_def 1 2 3 set_diff_eq conj_ac) 734qed (simp add: sum.G_def) 735 736lemma sum_diff1': 737 fixes f :: "'a \<Rightarrow> 'b::ab_group_add" 738 assumes "finite {i \<in> I. f i \<noteq> 0}" 739 shows "sum' f (I - {i}) = (if i \<in> I then sum' f I - f i else sum' f I)" 740 by (rule sum_diff1'_aux [OF assms order_refl]) 741 742lemma (in ordered_comm_monoid_add) sum_mono: 743 "(\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" 744 by (induct K rule: infinite_finite_induct) (use add_mono in auto) 745 746lemma (in strict_ordered_comm_monoid_add) sum_strict_mono: 747 assumes "finite A" "A \<noteq> {}" 748 and "\<And>x. x \<in> A \<Longrightarrow> f x < g x" 749 shows "sum f A < sum g A" 750 using assms 751proof (induct rule: finite_ne_induct) 752 case singleton 753 then show ?case by simp 754next 755 case insert 756 then show ?case by (auto simp: add_strict_mono) 757qed 758 759lemma sum_strict_mono_ex1: 760 fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add" 761 assumes "finite A" 762 and "\<forall>x\<in>A. f x \<le> g x" 763 and "\<exists>a\<in>A. f a < g a" 764 shows "sum f A < sum g A" 765proof- 766 from assms(3) obtain a where a: "a \<in> A" "f a < g a" by blast 767 have "sum f A = sum f ((A - {a}) \<union> {a})" 768 by(simp add: insert_absorb[OF \<open>a \<in> A\<close>]) 769 also have "\<dots> = sum f (A - {a}) + sum f {a}" 770 using \<open>finite A\<close> by(subst sum.union_disjoint) auto 771 also have "sum f (A - {a}) \<le> sum g (A - {a})" 772 by (rule sum_mono) (simp add: assms(2)) 773 also from a have "sum f {a} < sum g {a}" by simp 774 also have "sum g (A - {a}) + sum g {a} = sum g((A - {a}) \<union> {a})" 775 using \<open>finite A\<close> by (subst sum.union_disjoint[symmetric]) auto 776 also have "\<dots> = sum g A" by (simp add: insert_absorb[OF \<open>a \<in> A\<close>]) 777 finally show ?thesis 778 by (auto simp add: add_right_mono add_strict_left_mono) 779qed 780 781lemma sum_mono_inv: 782 fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add" 783 assumes eq: "sum f I = sum g I" 784 assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i" 785 assumes i: "i \<in> I" 786 assumes I: "finite I" 787 shows "f i = g i" 788proof (rule ccontr) 789 assume "\<not> ?thesis" 790 with le[OF i] have "f i < g i" by simp 791 with i have "\<exists>i\<in>I. f i < g i" .. 792 from sum_strict_mono_ex1[OF I _ this] le have "sum f I < sum g I" 793 by blast 794 with eq show False by simp 795qed 796 797lemma member_le_sum: 798 fixes f :: "_ \<Rightarrow> 'b::{semiring_1, ordered_comm_monoid_add}" 799 assumes "i \<in> A" 800 and le: "\<And>x. x \<in> A - {i} \<Longrightarrow> 0 \<le> f x" 801 and "finite A" 802 shows "f i \<le> sum f A" 803proof - 804 have "f i \<le> sum f (A \<inter> {i})" 805 by (simp add: assms) 806 also have "... = (\<Sum>x\<in>A. if x \<in> {i} then f x else 0)" 807 using assms sum.inter_restrict by blast 808 also have "... \<le> sum f A" 809 apply (rule sum_mono) 810 apply (auto simp: le) 811 done 812 finally show ?thesis . 813qed 814 815lemma sum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)" 816 for f :: "'b \<Rightarrow> 'a::ab_group_add" 817 by (induct A rule: infinite_finite_induct) auto 818 819lemma sum_subtractf: "(\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)" 820 for f g :: "'b \<Rightarrow>'a::ab_group_add" 821 using sum.distrib [of f "- g" A] by (simp add: sum_negf) 822 823lemma sum_subtractf_nat: 824 "(\<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)" 825 for f g :: "'a \<Rightarrow> nat" 826 by (induct A rule: infinite_finite_induct) (auto simp: sum_mono) 827 828context ordered_comm_monoid_add 829begin 830 831lemma sum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> sum f A" 832proof (induct A rule: infinite_finite_induct) 833 case infinite 834 then show ?case by simp 835next 836 case empty 837 then show ?case by simp 838next 839 case (insert x F) 840 then have "0 + 0 \<le> f x + sum f F" by (blast intro: add_mono) 841 with insert show ?case by simp 842qed 843 844lemma sum_nonpos: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> 0) \<Longrightarrow> sum f A \<le> 0" 845proof (induct A rule: infinite_finite_induct) 846 case infinite 847 then show ?case by simp 848next 849 case empty 850 then show ?case by simp 851next 852 case (insert x F) 853 then have "f x + sum f F \<le> 0 + 0" by (blast intro: add_mono) 854 with insert show ?case by simp 855qed 856 857lemma sum_nonneg_eq_0_iff: 858 "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" 859 by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg) 860 861lemma sum_nonneg_0: 862 "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" 863 by (simp add: sum_nonneg_eq_0_iff) 864 865lemma sum_nonneg_leq_bound: 866 assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s" 867 shows "f i \<le> B" 868proof - 869 from assms have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)" 870 by (intro add_increasing2 sum_nonneg) auto 871 also have "\<dots> = B" 872 using sum.remove[of s i f] assms by simp 873 finally show ?thesis by auto 874qed 875 876lemma sum_mono2: 877 assumes fin: "finite B" 878 and sub: "A \<subseteq> B" 879 and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b" 880 shows "sum f A \<le> sum f B" 881proof - 882 have "sum f A \<le> sum f A + sum f (B-A)" 883 by (auto intro: add_increasing2 [OF sum_nonneg] nn) 884 also from fin finite_subset[OF sub fin] have "\<dots> = sum f (A \<union> (B-A))" 885 by (simp add: sum.union_disjoint del: Un_Diff_cancel) 886 also from sub have "A \<union> (B-A) = B" by blast 887 finally show ?thesis . 888qed 889 890lemma sum_le_included: 891 assumes "finite s" "finite t" 892 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)" 893 shows "sum f s \<le> sum g t" 894proof - 895 have "sum f s \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) s" 896 proof (rule sum_mono) 897 fix y 898 assume "y \<in> s" 899 with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto 900 with assms show "f y \<le> sum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") 901 using order_trans[of "?A (i z)" "sum g {z}" "?B (i z)", intro] 902 by (auto intro!: sum_mono2) 903 qed 904 also have "\<dots> \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) (i ` t)" 905 using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg) 906 also have "\<dots> \<le> sum g t" 907 using assms by (auto simp: sum.image_gen[symmetric]) 908 finally show ?thesis . 909qed 910 911end 912 913lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]: 914 "finite F \<Longrightarrow> (sum f F = 0) = (\<forall>a\<in>F. f a = 0)" 915 by (intro ballI sum_nonneg_eq_0_iff zero_le) 916 917context semiring_0 918begin 919 920lemma sum_distrib_left: "r * sum f A = (\<Sum>n\<in>A. r * f n)" 921 by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) 922 923lemma sum_distrib_right: "sum f A * r = (\<Sum>n\<in>A. f n * r)" 924 by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) 925 926end 927 928lemma sum_divide_distrib: "sum f A / r = (\<Sum>n\<in>A. f n / r)" 929 for r :: "'a::field" 930proof (induct A rule: infinite_finite_induct) 931 case infinite 932 then show ?case by simp 933next 934 case empty 935 then show ?case by simp 936next 937 case insert 938 then show ?case by (simp add: add_divide_distrib) 939qed 940 941lemma sum_abs[iff]: "\<bar>sum f A\<bar> \<le> sum (\<lambda>i. \<bar>f i\<bar>) A" 942 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" 943proof (induct A rule: infinite_finite_induct) 944 case infinite 945 then show ?case by simp 946next 947 case empty 948 then show ?case by simp 949next 950 case insert 951 then show ?case by (auto intro: abs_triangle_ineq order_trans) 952qed 953 954lemma sum_abs_ge_zero[iff]: "0 \<le> sum (\<lambda>i. \<bar>f i\<bar>) A" 955 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" 956 by (simp add: sum_nonneg) 957 958lemma abs_sum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)" 959 for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs" 960proof (induct A rule: infinite_finite_induct) 961 case infinite 962 then show ?case by simp 963next 964 case empty 965 then show ?case by simp 966next 967 case (insert a A) 968 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 969 also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp 970 also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg) 971 also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp 972 finally show ?case . 973qed 974 975lemma sum_product: 976 fixes f :: "'a \<Rightarrow> 'b::semiring_0" 977 shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" 978 by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap) 979 980lemma sum_mult_sum_if_inj: 981 fixes f :: "'a \<Rightarrow> 'b::semiring_0" 982 shows "inj_on (\<lambda>(a, b). f a * g b) (A \<times> B) \<Longrightarrow> 983 sum f A * sum g B = sum id {f a * g b |a b. a \<in> A \<and> b \<in> B}" 984 by(auto simp: sum_product sum.cartesian_product intro!: sum.reindex_cong[symmetric]) 985 986lemma sum_SucD: "sum f A = Suc n \<Longrightarrow> \<exists>a\<in>A. 0 < f a" 987 by (induct A rule: infinite_finite_induct) auto 988 989lemma sum_eq_Suc0_iff: 990 "finite A \<Longrightarrow> sum 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))" 991 by (induct A rule: finite_induct) (auto simp add: add_is_1) 992 993lemmas sum_eq_1_iff = sum_eq_Suc0_iff[simplified One_nat_def[symmetric]] 994 995lemma sum_Un_nat: 996 "finite A \<Longrightarrow> finite B \<Longrightarrow> sum f (A \<union> B) = sum f A + sum f B - sum f (A \<inter> B)" 997 for f :: "'a \<Rightarrow> nat" 998 \<comment> \<open>For the natural numbers, we have subtraction.\<close> 999 by (subst sum.union_inter [symmetric]) (auto simp: algebra_simps) 1000 1001lemma sum_diff1_nat: "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)" 1002 for f :: "'a \<Rightarrow> nat" 1003proof (induct A rule: infinite_finite_induct) 1004 case infinite 1005 then show ?case by simp 1006next 1007 case empty 1008 then show ?case by simp 1009next 1010 case insert 1011 then show ?case 1012 apply (auto simp: insert_Diff_if) 1013 apply (drule mk_disjoint_insert) 1014 apply auto 1015 done 1016qed 1017 1018lemma sum_diff_nat: 1019 fixes f :: "'a \<Rightarrow> nat" 1020 assumes "finite B" and "B \<subseteq> A" 1021 shows "sum f (A - B) = sum f A - sum f B" 1022 using assms 1023proof induct 1024 case empty 1025 then show ?case by simp 1026next 1027 case (insert x F) 1028 note IH = \<open>F \<subseteq> A \<Longrightarrow> sum f (A - F) = sum f A - sum f F\<close> 1029 from \<open>x \<notin> F\<close> \<open>insert x F \<subseteq> A\<close> have "x \<in> A - F" by simp 1030 then have A: "sum f ((A - F) - {x}) = sum f (A - F) - f x" 1031 by (simp add: sum_diff1_nat) 1032 from \<open>insert x F \<subseteq> A\<close> have "F \<subseteq> A" by simp 1033 with IH have "sum f (A - F) = sum f A - sum f F" by simp 1034 with A have B: "sum f ((A - F) - {x}) = sum f A - sum f F - f x" 1035 by simp 1036 from \<open>x \<notin> F\<close> have "A - insert x F = (A - F) - {x}" by auto 1037 with B have C: "sum f (A - insert x F) = sum f A - sum f F - f x" 1038 by simp 1039 from \<open>finite F\<close> \<open>x \<notin> F\<close> have "sum f (insert x F) = sum f F + f x" 1040 by simp 1041 with C have "sum f (A - insert x F) = sum f A - sum f (insert x F)" 1042 by simp 1043 then show ?case by simp 1044qed 1045 1046lemma sum_comp_morphism: 1047 "h 0 = 0 \<Longrightarrow> (\<And>x y. h (x + y) = h x + h y) \<Longrightarrow> sum (h \<circ> g) A = h (sum g A)" 1048 by (induct A rule: infinite_finite_induct) simp_all 1049 1050lemma (in comm_semiring_1) dvd_sum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd sum f A" 1051 by (induct A rule: infinite_finite_induct) simp_all 1052 1053lemma (in ordered_comm_monoid_add) sum_pos: 1054 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < sum f I" 1055 by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos) 1056 1057lemma (in ordered_comm_monoid_add) sum_pos2: 1058 assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" 1059 shows "0 < sum f I" 1060proof - 1061 have "0 < f i + sum f (I - {i})" 1062 using assms by (intro add_pos_nonneg sum_nonneg) auto 1063 also have "\<dots> = sum f I" 1064 using assms by (simp add: sum.remove) 1065 finally show ?thesis . 1066qed 1067 1068lemma sum_cong_Suc: 1069 assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)" 1070 shows "sum f A = sum g A" 1071proof (rule sum.cong) 1072 fix x 1073 assume "x \<in> A" 1074 with assms(1) show "f x = g x" 1075 by (cases x) (auto intro!: assms(2)) 1076qed simp_all 1077 1078 1079subsubsection \<open>Cardinality as special case of \<^const>\<open>sum\<close>\<close> 1080 1081lemma card_eq_sum: "card A = sum (\<lambda>x. 1) A" 1082proof - 1083 have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)" 1084 by (simp add: fun_eq_iff) 1085 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)" 1086 by (rule arg_cong) 1087 then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A" 1088 by (blast intro: fun_cong) 1089 then show ?thesis 1090 by (simp add: card.eq_fold sum.eq_fold) 1091qed 1092 1093context semiring_1 1094begin 1095 1096lemma sum_constant [simp]: 1097 "(\<Sum>x \<in> A. y) = of_nat (card A) * y" 1098 by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps) 1099 1100end 1101 1102lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A" 1103 using sum.distrib[of f "\<lambda>_. 1" A] by simp 1104 1105lemma sum_bounded_above: 1106 fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" 1107 assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K" 1108 shows "sum f A \<le> of_nat (card A) * K" 1109proof (cases "finite A") 1110 case True 1111 then show ?thesis 1112 using le sum_mono[where K=A and g = "\<lambda>x. K"] by simp 1113next 1114 case False 1115 then show ?thesis by simp 1116qed 1117 1118lemma sum_bounded_above_divide: 1119 fixes K :: "'a::linordered_field" 1120 assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K / of_nat (card A)" and fin: "finite A" "A \<noteq> {}" 1121 shows "sum f A \<le> K" 1122 using sum_bounded_above [of A f "K / of_nat (card A)", OF le] fin by simp 1123 1124lemma sum_bounded_above_strict: 1125 fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}" 1126 assumes "\<And>i. i\<in>A \<Longrightarrow> f i < K" "card A > 0" 1127 shows "sum f A < of_nat (card A) * K" 1128 using assms sum_strict_mono[where A=A and g = "\<lambda>x. K"] 1129 by (simp add: card_gt_0_iff) 1130 1131lemma sum_bounded_below: 1132 fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}" 1133 assumes le: "\<And>i. i\<in>A \<Longrightarrow> K \<le> f i" 1134 shows "of_nat (card A) * K \<le> sum f A" 1135proof (cases "finite A") 1136 case True 1137 then show ?thesis 1138 using le sum_mono[where K=A and f = "\<lambda>x. K"] by simp 1139next 1140 case False 1141 then show ?thesis by simp 1142qed 1143 1144lemma convex_sum_bound_le: 1145 fixes x :: "'a \<Rightarrow> 'b::linordered_idom" 1146 assumes 0: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> x i" and 1: "sum x I = 1" 1147 and \<delta>: "\<And>i. i \<in> I \<Longrightarrow> \<bar>a i - b\<bar> \<le> \<delta>" 1148 shows "\<bar>(\<Sum>i\<in>I. a i * x i) - b\<bar> \<le> \<delta>" 1149proof - 1150 have [simp]: "(\<Sum>i\<in>I. c * x i) = c" for c 1151 by (simp flip: sum_distrib_left 1) 1152 then have "\<bar>(\<Sum>i\<in>I. a i * x i) - b\<bar> = \<bar>\<Sum>i\<in>I. (a i - b) * x i\<bar>" 1153 by (simp add: sum_subtractf left_diff_distrib) 1154 also have "\<dots> \<le> (\<Sum>i\<in>I. \<bar>(a i - b) * x i\<bar>)" 1155 using abs_abs abs_of_nonneg by blast 1156 also have "\<dots> \<le> (\<Sum>i\<in>I. \<bar>(a i - b)\<bar> * x i)" 1157 by (simp add: abs_mult 0) 1158 also have "\<dots> \<le> (\<Sum>i\<in>I. \<delta> * x i)" 1159 by (rule sum_mono) (use \<delta> "0" mult_right_mono in blast) 1160 also have "\<dots> = \<delta>" 1161 by simp 1162 finally show ?thesis . 1163qed 1164 1165lemma card_UN_disjoint: 1166 assumes "finite I" and "\<forall>i\<in>I. finite (A i)" 1167 and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}" 1168 shows "card (\<Union>(A ` I)) = (\<Sum>i\<in>I. card(A i))" 1169proof - 1170 have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" 1171 by simp 1172 with assms show ?thesis 1173 by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant) 1174qed 1175 1176lemma card_Union_disjoint: 1177 assumes "pairwise disjnt C" and fin: "\<And>A. A \<in> C \<Longrightarrow> finite A" 1178 shows "card (\<Union>C) = sum card C" 1179proof (cases "finite C") 1180 case True 1181 then show ?thesis 1182 using card_UN_disjoint [OF True, of "\<lambda>x. x"] assms 1183 by (simp add: disjnt_def fin pairwise_def) 1184next 1185 case False 1186 then show ?thesis 1187 using assms card_eq_0_iff finite_UnionD by fastforce 1188qed 1189 1190lemma card_Union_le_sum_card: 1191 fixes U :: "'a set set" 1192 assumes "\<forall>u \<in> U. finite u" 1193 shows "card (\<Union>U) \<le> sum card U" 1194proof (cases "finite U") 1195 case False 1196 then show "card (\<Union>U) \<le> sum card U" 1197 using card_eq_0_iff finite_UnionD by auto 1198next 1199 case True 1200 then show "card (\<Union>U) \<le> sum card U" 1201 proof (induct U rule: finite_induct) 1202 case empty 1203 then show ?case by auto 1204 next 1205 case (insert x F) 1206 then have "card(\<Union>(insert x F)) \<le> card(x) + card (\<Union>F)" using card_Un_le by auto 1207 also have "... \<le> card(x) + sum card F" using insert.hyps by auto 1208 also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto 1209 finally show ?case . 1210 qed 1211qed 1212 1213lemma card_UN_le: 1214 assumes "finite I" 1215 shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))" 1216 using assms 1217proof induction 1218 case (insert i I) 1219 then show ?case 1220 using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) 1221qed auto 1222 1223lemma sum_multicount_gen: 1224 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" 1225 shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t" 1226 (is "?l = ?r") 1227proof- 1228 have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s" 1229 by auto 1230 also have "\<dots> = ?r" 1231 unfolding sum.swap_restrict [OF assms(1-2)] 1232 using assms(3) by auto 1233 finally show ?thesis . 1234qed 1235 1236lemma sum_multicount: 1237 assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" 1238 shows "sum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") 1239proof- 1240 have "?l = sum (\<lambda>i. k) T" 1241 by (rule sum_multicount_gen) (auto simp: assms) 1242 also have "\<dots> = ?r" by (simp add: mult.commute) 1243 finally show ?thesis by auto 1244qed 1245 1246lemma sum_card_image: 1247 assumes "finite A" 1248 assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) A" 1249 shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A" 1250using assms 1251proof (induct A) 1252 case (insert a A) 1253 show ?case 1254 proof cases 1255 assume "f a = {}" 1256 with insert show ?case 1257 by (subst sum.mono_neutral_right[where S="f ` A"]) (auto simp: pairwise_insert) 1258 next 1259 assume "f a \<noteq> {}" 1260 then have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)" 1261 using insert 1262 by (subst sum.insert) (auto simp: pairwise_insert) 1263 with insert show ?case by (simp add: pairwise_insert) 1264 qed 1265qed simp 1266 1267 1268subsubsection \<open>Cardinality of products\<close> 1269 1270lemma card_SigmaI [simp]: 1271 "finite A \<Longrightarrow> \<forall>a\<in>A. finite (B a) \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" 1272 by (simp add: card_eq_sum sum.Sigma del: sum_constant) 1273 1274(* 1275lemma SigmaI_insert: "y \<notin> A ==> 1276 (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))" 1277 by auto 1278*) 1279 1280lemma card_cartesian_product: "card (A \<times> B) = card A * card B" 1281 by (cases "finite A \<and> finite B") 1282 (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2) 1283 1284lemma card_cartesian_product_singleton: "card ({x} \<times> A) = card A" 1285 by (simp add: card_cartesian_product) 1286 1287 1288subsection \<open>Generalized product over a set\<close> 1289 1290context comm_monoid_mult 1291begin 1292 1293sublocale prod: comm_monoid_set times 1 1294 defines prod = prod.F and prod' = prod.G .. 1295 1296abbreviation Prod ("\<Prod>_" [1000] 999) 1297 where "\<Prod>A \<equiv> prod (\<lambda>x. x) A" 1298 1299end 1300 1301syntax (ASCII) 1302 "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10) 1303syntax 1304 "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10) 1305translations \<comment> \<open>Beware of argument permutation!\<close> 1306 "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A" 1307 1308text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close> 1309 1310syntax (ASCII) 1311 "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10) 1312syntax 1313 "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10) 1314translations 1315 "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}" 1316 1317context comm_monoid_mult 1318begin 1319 1320lemma prod_dvd_prod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> prod f A dvd prod g A" 1321proof (induct A rule: infinite_finite_induct) 1322 case infinite 1323 then show ?case by (auto intro: dvdI) 1324next 1325 case empty 1326 then show ?case by (auto intro: dvdI) 1327next 1328 case (insert a A) 1329 then have "f a dvd g a" and "prod f A dvd prod g A" 1330 by simp_all 1331 then obtain r s where "g a = f a * r" and "prod g A = prod f A * s" 1332 by (auto elim!: dvdE) 1333 then have "g a * prod g A = f a * prod f A * (r * s)" 1334 by (simp add: ac_simps) 1335 with insert.hyps show ?case 1336 by (auto intro: dvdI) 1337qed 1338 1339lemma prod_dvd_prod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> prod f A dvd prod f B" 1340 by (auto simp add: prod.subset_diff ac_simps intro: dvdI) 1341 1342end 1343 1344 1345subsubsection \<open>Properties in more restricted classes of structures\<close> 1346 1347context linordered_nonzero_semiring 1348begin 1349 1350lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A" 1351proof (induct A rule: infinite_finite_induct) 1352 case infinite 1353 then show ?case by simp 1354next 1355 case empty 1356 then show ?case by simp 1357next 1358 case (insert x F) 1359 have "1 * 1 \<le> f x * prod f F" 1360 by (rule mult_mono') (use insert in auto) 1361 with insert show ?case by simp 1362qed 1363 1364lemma prod_le_1: 1365 fixes f :: "'b \<Rightarrow> 'a" 1366 assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1" 1367 shows "prod f A \<le> 1" 1368 using assms 1369proof (induct A rule: infinite_finite_induct) 1370 case infinite 1371 then show ?case by simp 1372next 1373 case empty 1374 then show ?case by simp 1375next 1376 case (insert x F) 1377 then show ?case by (force simp: mult.commute intro: dest: mult_le_one) 1378qed 1379 1380end 1381 1382context comm_semiring_1 1383begin 1384 1385lemma dvd_prod_eqI [intro]: 1386 assumes "finite A" and "a \<in> A" and "b = f a" 1387 shows "b dvd prod f A" 1388proof - 1389 from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})" 1390 by (intro prod.insert) auto 1391 also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A" 1392 by blast 1393 finally have "prod f A = f a * prod f (A - {a})" . 1394 with \<open>b = f a\<close> show ?thesis 1395 by simp 1396qed 1397 1398lemma dvd_prodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd prod f A" 1399 by auto 1400 1401lemma prod_zero: 1402 assumes "finite A" and "\<exists>a\<in>A. f a = 0" 1403 shows "prod f A = 0" 1404 using assms 1405proof (induct A) 1406 case empty 1407 then show ?case by simp 1408next 1409 case (insert a A) 1410 then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp 1411 then have "f a * prod f A = 0" by rule (simp_all add: insert) 1412 with insert show ?case by simp 1413qed 1414 1415lemma prod_dvd_prod_subset2: 1416 assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a" 1417 shows "prod f A dvd prod g B" 1418proof - 1419 from assms have "prod f A dvd prod g A" 1420 by (auto intro: prod_dvd_prod) 1421 moreover from assms have "prod g A dvd prod g B" 1422 by (auto intro: prod_dvd_prod_subset) 1423 ultimately show ?thesis by (rule dvd_trans) 1424qed 1425 1426end 1427 1428lemma (in semidom) prod_zero_iff [simp]: 1429 fixes f :: "'b \<Rightarrow> 'a" 1430 assumes "finite A" 1431 shows "prod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)" 1432 using assms by (induct A) (auto simp: no_zero_divisors) 1433 1434lemma (in semidom_divide) prod_diff1: 1435 assumes "finite A" and "f a \<noteq> 0" 1436 shows "prod f (A - {a}) = (if a \<in> A then prod f A div f a else prod f A)" 1437proof (cases "a \<notin> A") 1438 case True 1439 then show ?thesis by simp 1440next 1441 case False 1442 with assms show ?thesis 1443 proof induct 1444 case empty 1445 then show ?case by simp 1446 next 1447 case (insert b B) 1448 then show ?case 1449 proof (cases "a = b") 1450 case True 1451 with insert show ?thesis by simp 1452 next 1453 case False 1454 with insert have "a \<in> B" by simp 1455 define C where "C = B - {a}" 1456 with \<open>finite B\<close> \<open>a \<in> B\<close> have "B = insert a C" "finite C" "a \<notin> C" 1457 by auto 1458 with insert show ?thesis 1459 by (auto simp add: insert_commute ac_simps) 1460 qed 1461 qed 1462qed 1463 1464lemma sum_zero_power [simp]: "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)" 1465 for c :: "nat \<Rightarrow> 'a::division_ring" 1466 by (induct A rule: infinite_finite_induct) auto 1467 1468lemma sum_zero_power' [simp]: 1469 "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)" 1470 for c :: "nat \<Rightarrow> 'a::field" 1471 using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto 1472 1473lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)" 1474 proof (cases "finite A") 1475 case True 1476 then show ?thesis 1477 by (induct A rule: finite_induct) simp_all 1478 next 1479 case False 1480 then show ?thesis 1481 by auto 1482 qed 1483 1484lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A" 1485 using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib) 1486 1487lemma prod_Un: 1488 fixes f :: "'b \<Rightarrow> 'a :: field" 1489 assumes "finite A" and "finite B" 1490 and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0" 1491 shows "prod f (A \<union> B) = prod f A * prod f B / prod f (A \<inter> B)" 1492proof - 1493 from assms have "prod f A * prod f B = prod f (A \<union> B) * prod f (A \<inter> B)" 1494 by (simp add: prod.union_inter [symmetric, of A B]) 1495 with assms show ?thesis 1496 by simp 1497qed 1498 1499context linordered_semidom 1500begin 1501 1502lemma prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A" 1503 by (induct A rule: infinite_finite_induct) simp_all 1504 1505lemma prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A" 1506 by (induct A rule: infinite_finite_induct) simp_all 1507 1508lemma prod_mono: 1509 "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A" 1510 by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+ 1511 1512lemma prod_mono_strict: 1513 assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}" 1514 shows "prod f A < prod g A" 1515 using assms 1516proof (induct A rule: finite_induct) 1517 case empty 1518 then show ?case by simp 1519next 1520 case insert 1521 then show ?case by (force intro: mult_strict_mono' prod_nonneg) 1522qed 1523 1524end 1525 1526lemma prod_mono2: 1527 fixes f :: "'a \<Rightarrow> 'b :: linordered_idom" 1528 assumes fin: "finite B" 1529 and sub: "A \<subseteq> B" 1530 and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 1 \<le> f b" 1531 and A: "\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a" 1532 shows "prod f A \<le> prod f B" 1533proof - 1534 have "prod f A \<le> prod f A * prod f (B-A)" 1535 by (metis prod_ge_1 A mult_le_cancel_left1 nn not_less prod_nonneg) 1536 also from fin finite_subset[OF sub fin] have "\<dots> = prod f (A \<union> (B-A))" 1537 by (simp add: prod.union_disjoint del: Un_Diff_cancel) 1538 also from sub have "A \<union> (B-A) = B" by blast 1539 finally show ?thesis . 1540qed 1541 1542lemma less_1_prod: 1543 fixes f :: "'a \<Rightarrow> 'b::linordered_idom" 1544 shows "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 1 < f i) \<Longrightarrow> 1 < prod f I" 1545 by (induct I rule: finite_ne_induct) (auto intro: less_1_mult) 1546 1547lemma less_1_prod2: 1548 fixes f :: "'a \<Rightarrow> 'b::linordered_idom" 1549 assumes I: "finite I" "i \<in> I" "1 < f i" "\<And>i. i \<in> I \<Longrightarrow> 1 \<le> f i" 1550 shows "1 < prod f I" 1551proof - 1552 have "1 < f i * prod f (I - {i})" 1553 using assms 1554 by (meson DiffD1 leI less_1_mult less_le_trans mult_le_cancel_left1 prod_ge_1) 1555 also have "\<dots> = prod f I" 1556 using assms by (simp add: prod.remove) 1557 finally show ?thesis . 1558qed 1559 1560lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)" 1561 by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult) 1562 1563lemma prod_eq_1_iff [simp]: "finite A \<Longrightarrow> prod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)" 1564 for f :: "'a \<Rightarrow> nat" 1565 by (induct A rule: finite_induct) simp_all 1566 1567lemma prod_pos_nat_iff [simp]: "finite A \<Longrightarrow> prod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)" 1568 for f :: "'a \<Rightarrow> nat" 1569 using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero) 1570 1571lemma prod_constant [simp]: "(\<Prod>x\<in> A. y) = y ^ card A" 1572 for y :: "'a::comm_monoid_mult" 1573 by (induct A rule: infinite_finite_induct) simp_all 1574 1575lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A" 1576 for f :: "'a \<Rightarrow> 'b::comm_semiring_1" 1577 by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib) 1578 1579lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" 1580 by (induct A rule: infinite_finite_induct) (simp_all add: power_add) 1581 1582lemma prod_gen_delta: 1583 fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult" 1584 assumes fin: "finite S" 1585 shows "prod (\<lambda>k. if k = a then b k else c) S = 1586 (if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)" 1587proof - 1588 let ?f = "(\<lambda>k. if k=a then b k else c)" 1589 show ?thesis 1590 proof (cases "a \<in> S") 1591 case False 1592 then have "\<forall> k\<in> S. ?f k = c" by simp 1593 with False show ?thesis by (simp add: prod_constant) 1594 next 1595 case True 1596 let ?A = "S - {a}" 1597 let ?B = "{a}" 1598 from True have eq: "S = ?A \<union> ?B" by blast 1599 have disjoint: "?A \<inter> ?B = {}" by simp 1600 from fin have fin': "finite ?A" "finite ?B" by auto 1601 have f_A0: "prod ?f ?A = prod (\<lambda>i. c) ?A" 1602 by (rule prod.cong) auto 1603 from fin True have card_A: "card ?A = card S - 1" by auto 1604 have f_A1: "prod ?f ?A = c ^ card ?A" 1605 unfolding f_A0 by (rule prod_constant) 1606 have "prod ?f ?A * prod ?f ?B = prod ?f S" 1607 using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]] 1608 by simp 1609 with True card_A show ?thesis 1610 by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong) 1611 qed 1612qed 1613 1614lemma sum_image_le: 1615 fixes g :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add" 1616 assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)" 1617 shows "sum g (f ` I) \<le> sum (g \<circ> f) I" 1618 using assms 1619proof induction 1620 case empty 1621 then show ?case by auto 1622next 1623 case (insert x F) 1624 from insertI1 have "0 \<le> g (f x)" by (rule insert) 1625 hence 1: "sum g (f ` F) \<le> g (f x) + sum g (f ` F)" using add_increasing by blast 1626 have 2: "sum g (f ` F) \<le> sum (g \<circ> f) F" using insert by blast 1627 have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp 1628 also have "\<dots> \<le> g (f x) + sum g (f ` F)" by (simp add: 1 insert sum.insert_if) 1629 also from 2 have "\<dots> \<le> g (f x) + sum (g \<circ> f) F" by (rule add_left_mono) 1630 also from insert(1, 2) have "\<dots> = sum (g \<circ> f) (insert x F)" by (simp add: sum.insert_if) 1631 finally show ?case . 1632qed 1633 1634end 1635