summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | bulwahn |

Sat, 27 Jan 2018 10:27:57 +0100 | |

changeset 67511 | a6f5a78712af |

parent 67510 | 9624711ef2de |

child 67512 | 166c1659ac75 |

include lemmas generally useful for combinatorial proofs

src/HOL/Finite_Set.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Groups_Big.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Finite_Set.thy Fri Jan 26 21:16:03 2018 +0100 +++ b/src/HOL/Finite_Set.thy Sat Jan 27 10:27:57 2018 +0100 @@ -485,6 +485,12 @@ lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A" by (blast intro: finite_subset [OF subset_Pow_Union]) +lemma finite_bind: + assumes "finite S" + assumes "\<forall>x \<in> S. finite (f x)" + shows "finite (Set.bind S f)" +using assms by (simp add: bind_UNION) + lemma finite_set_of_finite_funs: assumes "finite A" "finite B" shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")

--- a/src/HOL/Groups_Big.thy Fri Jan 26 21:16:03 2018 +0100 +++ b/src/HOL/Groups_Big.thy Sat Jan 27 10:27:57 2018 +0100 @@ -1027,6 +1027,43 @@ finally show ?thesis by auto qed +lemma sum_card_image: + assumes "finite A" + assumes "\<forall>s\<in>A. \<forall>t\<in>A. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}" + shows "sum card (f ` A) = sum (\<lambda>a. card (f a)) A" +using assms +proof (induct A) + case empty + from this show ?case by simp +next + case (insert a A) + show ?case + proof cases + assume "f a = {}" + from this insert show ?case + by (subst sum.mono_neutral_right[where S="f ` A"]) auto + next + assume "f a \<noteq> {}" + from this have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)" + using insert by (subst sum.insert) auto + from this insert show ?case by simp + qed +qed + +lemma card_Union_image: + assumes "finite S" + assumes "\<forall>s\<in>f ` S. finite s" + assumes "\<forall>s\<in>S. \<forall>t\<in>S. s \<noteq> t \<longrightarrow> (f s) \<inter> (f t) = {}" + shows "card (\<Union>(f ` S)) = sum (\<lambda>x. card (f x)) S" +proof - + have "\<forall>A\<in>f ` S. \<forall>B\<in>f ` S. A \<noteq> B \<longrightarrow> A \<inter> B = {}" + using assms(3) by (metis image_iff) + from this have "card (\<Union>(f ` S)) = sum card (f ` S)" + using assms(1, 2) by (subst card_Union_disjoint) auto + also have "... = sum (\<lambda>x. card (f x)) S" + using assms(1, 3) by (auto simp add: sum_card_image) + finally show ?thesis . +qed subsubsection \<open>Cardinality of products\<close>