1257 case (insert i I) |
1257 case (insert i I) |
1258 then show ?case |
1258 then show ?case |
1259 using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) |
1259 using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) |
1260 qed auto |
1260 qed auto |
1261 |
1261 |
|
1262 lemma card_quotient_disjoint: |
|
1263 assumes "finite A" "inj_on (\<lambda>x. {x} // r) A" |
|
1264 shows "card (A//r) = card A" |
|
1265 proof - |
|
1266 have "\<forall>i\<in>A. \<forall>j\<in>A. i \<noteq> j \<longrightarrow> r `` {j} \<noteq> r `` {i}" |
|
1267 using assms by (fastforce simp add: quotient_def inj_on_def) |
|
1268 with assms show ?thesis |
|
1269 by (simp add: quotient_def card_UN_disjoint) |
|
1270 qed |
|
1271 |
1262 lemma sum_multicount_gen: |
1272 lemma sum_multicount_gen: |
1263 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" |
1273 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" |
1264 shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t" |
1274 shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t" |
1265 (is "?l = ?r") |
1275 (is "?l = ?r") |
1266 proof- |
1276 proof- |
1300 using insert |
1310 using insert |
1301 by (subst sum.insert) (auto simp: pairwise_insert) |
1311 by (subst sum.insert) (auto simp: pairwise_insert) |
1302 with insert show ?case by (simp add: pairwise_insert) |
1312 with insert show ?case by (simp add: pairwise_insert) |
1303 qed |
1313 qed |
1304 qed simp |
1314 qed simp |
|
1315 |
|
1316 text \<open>By Jakub Kądziołka:\<close> |
|
1317 |
|
1318 lemma sum_fun_comp: |
|
1319 assumes "finite S" "finite R" "g ` S \<subseteq> R" |
|
1320 shows "(\<Sum>x \<in> S. f (g x)) = (\<Sum>y \<in> R. of_nat (card {x \<in> S. g x = y}) * f y)" |
|
1321 proof - |
|
1322 let ?r = "relation_of (\<lambda>p q. g p = g q) S" |
|
1323 have eqv: "equiv S ?r" |
|
1324 unfolding relation_of_def by (auto intro: comp_equivI) |
|
1325 have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C |
|
1326 by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]]) |
|
1327 have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B |
|
1328 using eqv quotient_disj by blast |
|
1329 |
|
1330 let ?cls = "\<lambda>y. {x \<in> S. y = g x}" |
|
1331 have quot_as_img: "S//?r = ?cls ` g ` S" |
|
1332 by (auto simp add: relation_of_def quotient_def) |
|
1333 have cls_inj: "inj_on ?cls (g ` S)" |
|
1334 by (auto intro: inj_onI) |
|
1335 |
|
1336 have rest_0: "(\<Sum>y \<in> R - g ` S. of_nat (card (?cls y)) * f y) = 0" |
|
1337 proof - |
|
1338 have "of_nat (card (?cls y)) * f y = 0" if asm: "y \<in> R - g ` S" for y |
|
1339 proof - |
|
1340 from asm have *: "?cls y = {}" by auto |
|
1341 show ?thesis unfolding * by simp |
|
1342 qed |
|
1343 thus ?thesis by simp |
|
1344 qed |
|
1345 |
|
1346 have "(\<Sum>x \<in> S. f (g x)) = (\<Sum>C \<in> S//?r. \<Sum>x \<in> C. f (g x))" |
|
1347 using eqv finite disjoint |
|
1348 by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient) |
|
1349 also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f (g x))" |
|
1350 unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj]) |
|
1351 also have "... = (\<Sum>y \<in> g ` S. \<Sum>x \<in> ?cls y. f y)" |
|
1352 by auto |
|
1353 also have "... = (\<Sum>y \<in> g ` S. of_nat (card (?cls y)) * f y)" |
|
1354 by (simp flip: sum_constant) |
|
1355 also have "... = (\<Sum>y \<in> R. of_nat (card (?cls y)) * f y)" |
|
1356 using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>]) |
|
1357 finally show ?thesis |
|
1358 by (simp add: eq_commute) |
|
1359 qed |
|
1360 |
1305 |
1361 |
1306 |
1362 |
1307 subsubsection \<open>Cardinality of products\<close> |
1363 subsubsection \<open>Cardinality of products\<close> |
1308 |
1364 |
1309 lemma card_SigmaI [simp]: |
1365 lemma card_SigmaI [simp]: |