src/HOL/Map.thy
 changeset 53820 9c7e97d67b45 parent 53374 a14d2a854c02 child 55466 786edc984c98
```     1.1 --- a/src/HOL/Map.thy	Mon Sep 23 16:56:17 2013 -0700
1.2 +++ b/src/HOL/Map.thy	Tue Sep 24 13:35:27 2013 +0200
1.3 @@ -589,6 +589,24 @@
1.4    then show ?thesis by (simp add: dom_map_of_conv_image_fst)
1.5  qed
1.6
1.7 +lemma finite_set_of_finite_maps:
1.8 +assumes "finite A" "finite B"
1.9 +shows  "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
1.10 +proof -
1.11 +  let ?S' = "{m. \<forall>x. (x \<in> A \<longrightarrow> m x \<in> Some ` B) \<and> (x \<notin> A \<longrightarrow> m x = None)}"
1.12 +  have "?S = ?S'"
1.13 +  proof
1.14 +    show "?S \<subseteq> ?S'" by(auto simp: dom_def ran_def image_def)
1.15 +    show "?S' \<subseteq> ?S"
1.16 +    proof
1.17 +      fix m assume "m \<in> ?S'"
1.18 +      hence 1: "dom m = A" by force
1.19 +      hence 2: "ran m \<subseteq> B" using `m \<in> ?S'` by(auto simp: dom_def ran_def)
1.20 +      from 1 2 show "m \<in> ?S" by blast
1.21 +    qed
1.22 +  qed
1.23 +  with assms show ?thesis by(simp add: finite_set_of_finite_funs)
1.24 +qed
1.25
1.26  subsection {* @{term [source] ran} *}
1.27
```