# HG changeset patch
# User nipkow
# Date 1380022527 -7200
# Node ID 9c7e97d67b456167c6b48547f796b262425a88dc
# Parent  0a62ad289c4d7ea8b58095090c32b9639db4f202
added lemmas

diff -r 0a62ad289c4d -r 9c7e97d67b45 src/HOL/Finite_Set.thy
--- 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 *}
 
diff -r 0a62ad289c4d -r 9c7e97d67b45 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Sep 23 16:56:17 2013 -0700
+++ b/src/HOL/Map.thy	Tue Sep 24 13:35:27 2013 +0200
@@ -589,6 +589,24 @@
   then show ?thesis by (simp add: dom_map_of_conv_image_fst)
 qed
 
+lemma finite_set_of_finite_maps:
+assumes "finite A" "finite B"
+shows  "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
+proof -
+  let ?S' = "{m. \<forall>x. (x \<in> A \<longrightarrow> m x \<in> Some ` B) \<and> (x \<notin> A \<longrightarrow> m x = None)}"
+  have "?S = ?S'"
+  proof
+    show "?S \<subseteq> ?S'" by(auto simp: dom_def ran_def image_def)
+    show "?S' \<subseteq> ?S"
+    proof
+      fix m assume "m \<in> ?S'"
+      hence 1: "dom m = A" by force
+      hence 2: "ran m \<subseteq> B" using `m \<in> ?S'` by(auto simp: dom_def ran_def)
+      from 1 2 show "m \<in> ?S" by blast
+    qed
+  qed
+  with assms show ?thesis by(simp add: finite_set_of_finite_funs)
+qed
 
 subsection {* @{term [source] ran} *}