equal
deleted
inserted
replaced
482 lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)" |
482 lemma finite_set: "finite (UNIV :: 'a set set) \<longleftrightarrow> finite (UNIV :: 'a set)" |
483 by (simp only: finite_Pow_iff Pow_UNIV[symmetric]) |
483 by (simp only: finite_Pow_iff Pow_UNIV[symmetric]) |
484 |
484 |
485 lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A" |
485 lemma finite_UnionD: "finite (\<Union>A) \<Longrightarrow> finite A" |
486 by (blast intro: finite_subset [OF subset_Pow_Union]) |
486 by (blast intro: finite_subset [OF subset_Pow_Union]) |
|
487 |
|
488 lemma finite_bind: |
|
489 assumes "finite S" |
|
490 assumes "\<forall>x \<in> S. finite (f x)" |
|
491 shows "finite (Set.bind S f)" |
|
492 using assms by (simp add: bind_UNION) |
487 |
493 |
488 lemma finite_set_of_finite_funs: |
494 lemma finite_set_of_finite_funs: |
489 assumes "finite A" "finite B" |
495 assumes "finite A" "finite B" |
490 shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S") |
496 shows "finite {f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S") |
491 proof - |
497 proof - |