merged
authorhaftmann
Tue Jun 23 11:32:12 2009 +0200 (2009-06-23)
changeset 31770ba52fcfaec28
parent 31761 3585bebe49a8
parent 31769 d5f39775edd2
child 31771 1a92eb45060f
merged
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jun 23 10:22:11 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jun 23 11:32:12 2009 +0200
     1.3 @@ -285,6 +285,10 @@
     1.4    -- {* The image of a finite set is finite. *}
     1.5    by (induct set: finite) simp_all
     1.6  
     1.7 +lemma finite_image_set [simp]:
     1.8 +  "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
     1.9 +  by (simp add: image_Collect [symmetric])
    1.10 +
    1.11  lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
    1.12    apply (frule finite_imageI)
    1.13    apply (erule finite_subset, assumption)
     2.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jun 23 10:22:11 2009 +0200
     2.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 23 11:32:12 2009 +0200
     2.3 @@ -67,6 +67,9 @@
     2.4    "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     2.5  by(auto simp: Pi_def)
     2.6  
     2.7 +lemma funcset_id [simp]: "(\<lambda>x. x) \<in> A \<rightarrow> A"
     2.8 +  by (auto intro: Pi_I)
     2.9 +
    2.10  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
    2.11    by (simp add: Pi_def)
    2.12