added lemmas
authornipkow
Tue Sep 24 13:35:27 2013 +0200 (2013-09-24)
changeset 538209c7e97d67b45
parent 53813 0a62ad289c4d
child 53821 9bae89bb032c
added lemmas
src/HOL/Finite_Set.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Mon Sep 23 16:56:17 2013 -0700
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 24 13:35:27 2013 +0200
     1.3 @@ -440,6 +440,16 @@
     1.4  lemma finite_UnionD: "finite(\<Union>A) \<Longrightarrow> finite A"
     1.5    by (blast intro: finite_subset [OF subset_Pow_Union])
     1.6  
     1.7 +lemma finite_set_of_finite_funs: assumes "finite A" "finite B"
     1.8 +shows "finite{f. \<forall>x. (x \<in> A \<longrightarrow> f x \<in> B) \<and> (x \<notin> A \<longrightarrow> f x = d)}" (is "finite ?S")
     1.9 +proof-
    1.10 +  let ?F = "\<lambda>f. {(a,b). a \<in> A \<and> b = f a}"
    1.11 +  have "?F ` ?S \<subseteq> Pow(A \<times> B)" by auto
    1.12 +  from finite_subset[OF this] assms have 1: "finite (?F ` ?S)" by simp
    1.13 +  have 2: "inj_on ?F ?S"
    1.14 +    by(fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)
    1.15 +  show ?thesis by(rule finite_imageD[OF 1 2])
    1.16 +qed
    1.17  
    1.18  subsubsection {* Further induction rules on finite sets *}
    1.19  
     2.1 --- a/src/HOL/Map.thy	Mon Sep 23 16:56:17 2013 -0700
     2.2 +++ b/src/HOL/Map.thy	Tue Sep 24 13:35:27 2013 +0200
     2.3 @@ -589,6 +589,24 @@
     2.4    then show ?thesis by (simp add: dom_map_of_conv_image_fst)
     2.5  qed
     2.6  
     2.7 +lemma finite_set_of_finite_maps:
     2.8 +assumes "finite A" "finite B"
     2.9 +shows  "finite {m. dom m = A \<and> ran m \<subseteq> B}" (is "finite ?S")
    2.10 +proof -
    2.11 +  let ?S' = "{m. \<forall>x. (x \<in> A \<longrightarrow> m x \<in> Some ` B) \<and> (x \<notin> A \<longrightarrow> m x = None)}"
    2.12 +  have "?S = ?S'"
    2.13 +  proof
    2.14 +    show "?S \<subseteq> ?S'" by(auto simp: dom_def ran_def image_def)
    2.15 +    show "?S' \<subseteq> ?S"
    2.16 +    proof
    2.17 +      fix m assume "m \<in> ?S'"
    2.18 +      hence 1: "dom m = A" by force
    2.19 +      hence 2: "ran m \<subseteq> B" using `m \<in> ?S'` by(auto simp: dom_def ran_def)
    2.20 +      from 1 2 show "m \<in> ?S" by blast
    2.21 +    qed
    2.22 +  qed
    2.23 +  with assms show ?thesis by(simp add: finite_set_of_finite_funs)
    2.24 +qed
    2.25  
    2.26  subsection {* @{term [source] ran} *}
    2.27