--- a/src/HOL/Finite_Set.thy Mon Sep 23 16:56:17 2013 -0700
+++ b/src/HOL/Finite_Set.thy Tue Sep 24 13:35:27 2013 +0200
@@ -440,6 +440,16 @@
lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
by (blast intro: finite_subset [OF subset_Pow_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")
+proof-
+ let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}"
+ have "?F ` ?S \<subseteq> Pow(A \<times> B)" by auto
+ from finite_subset[OF this] assms have 1: "finite (?F ` ?S)" by simp
+ have 2: "inj_on ?F ?S"
+ by(fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)
+ show ?thesis by(rule finite_imageD[OF 1 2])
+qed
subsubsection {* Further induction rules on finite sets *}