1004 with assms show ?thesis |
1004 with assms show ?thesis |
1005 by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant) |
1005 by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant) |
1006 qed |
1006 qed |
1007 |
1007 |
1008 lemma card_Union_disjoint: |
1008 lemma 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> |
1009 assumes "pairwise disjnt C" and fin: "\<And>A. A \<in> C \<Longrightarrow> finite A" |
1010 card (\<Union>C) = sum card C" |
1010 shows "card (\<Union>C) = sum card C" |
1011 by (frule card_UN_disjoint [of C id]) simp_all |
1011 proof (cases "finite C") |
|
1012 case True |
|
1013 then show ?thesis |
|
1014 using card_UN_disjoint [OF True, of "\<lambda>x. x"] assms |
|
1015 by (simp add: disjnt_def fin pairwise_def) |
|
1016 next |
|
1017 case False |
|
1018 then show ?thesis |
|
1019 using assms card_eq_0_iff finite_UnionD by fastforce |
|
1020 qed |
1012 |
1021 |
1013 lemma sum_multicount_gen: |
1022 lemma sum_multicount_gen: |
1014 assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" |
1023 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" |
1024 shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t" |
1016 (is "?l = ?r") |
1025 (is "?l = ?r") |
1033 finally show ?thesis by auto |
1042 finally show ?thesis by auto |
1034 qed |
1043 qed |
1035 |
1044 |
1036 lemma sum_card_image: |
1045 lemma sum_card_image: |
1037 assumes "finite A" |
1046 assumes "finite A" |
1038 assumes "\<forall>s\<in>A. \<forall>t\<in>A. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}" |
1047 assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) A" |
1039 shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A" |
1048 shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A" |
1040 using assms |
1049 using assms |
1041 proof (induct A) |
1050 proof (induct A) |
1042 case empty |
|
1043 from this show ?case by simp |
|
1044 next |
|
1045 case (insert a A) |
1051 case (insert a A) |
1046 show ?case |
1052 show ?case |
1047 proof cases |
1053 proof cases |
1048 assume "f a = {}" |
1054 assume "f a = {}" |
1049 from this insert show ?case |
1055 with insert show ?case |
1050 by (subst sum.mono_neutral_right[where S="f ` A"]) auto |
1056 by (subst sum.mono_neutral_right[where S="f ` A"]) (auto simp: pairwise_insert) |
1051 next |
1057 next |
1052 assume "f a \<noteq> {}" |
1058 assume "f a \<noteq> {}" |
1053 from this have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)" |
1059 then have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)" |
1054 using insert by (subst sum.insert) auto |
1060 using insert |
1055 from this insert show ?case by simp |
1061 by (subst sum.insert) (auto simp: pairwise_insert) |
|
1062 with insert show ?case by (simp add: pairwise_insert) |
1056 qed |
1063 qed |
1057 qed |
1064 qed simp |
1058 |
1065 |
1059 lemma card_Union_image: |
1066 lemma card_Union_image: |
1060 assumes "finite S" |
1067 assumes "finite S" |
1061 assumes "\<forall>s\<in>f ` S. finite s" |
1068 assumes "\<And>s. s \<in> S \<Longrightarrow> finite (f s)" |
1062 assumes "\<forall>s\<in>S. \<forall>t\<in>S. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}" |
1069 assumes "pairwise (\<lambda>s t. disjnt (f s) (f t)) S" |
1063 shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S" |
1070 shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S" |
1064 proof - |
1071 proof - |
1065 have "\<forall>A\<in>f ` S. \<forall>B\<in>f ` S. A \<noteq> B \<longrightarrow> A \<inter> B = {}" |
1072 have "pairwise disjnt (f ` S)" |
1066 using assms(3) by (metis image_iff) |
1073 using assms(3) |
1067 from this have "card (\<Union>(f ` S)) = sum card (f ` S)" |
1074 by (metis pairwiseD pairwise_imageI) |
1068 using assms(1, 2) by (subst card_Union_disjoint) auto |
1075 then have "card (\<Union>(f ` S)) = sum card (f ` S)" |
|
1076 by (subst card_Union_disjoint) (use assms in auto) |
1069 also have "... = sum (\<lambda>x. card (f x)) S" |
1077 also have "... = sum (\<lambda>x. card (f x)) S" |
1070 using assms(1, 3) by (auto simp add: sum_card_image) |
1078 by (metis (mono_tags, lifting) assms(1) assms(3) sum_card_image) |
1071 finally show ?thesis . |
1079 finally show ?thesis . |
1072 qed |
1080 qed |
|
1081 |
1073 |
1082 |
1074 subsubsection \<open>Cardinality of products\<close> |
1083 subsubsection \<open>Cardinality of products\<close> |
1075 |
1084 |
1076 lemma card_SigmaI [simp]: |
1085 lemma 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))" |
1086 "finite A \<Longrightarrow> \<forall>a\<in>A. finite (B a) \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
1150 |
1159 |
1151 subsubsection \<open>Properties in more restricted classes of structures\<close> |
1160 subsubsection \<open>Properties in more restricted classes of structures\<close> |
1152 |
1161 |
1153 context linordered_nonzero_semiring |
1162 context linordered_nonzero_semiring |
1154 begin |
1163 begin |
1155 |
1164 |
1156 lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A" |
1165 lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A" |
1157 proof (induct A rule: infinite_finite_induct) |
1166 proof (induct A rule: infinite_finite_induct) |
1158 case infinite |
1167 case infinite |
1159 then show ?case by simp |
1168 then show ?case by simp |
1160 next |
1169 next |