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