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