# HG changeset patch
# User huffman
# Date 1261062133 28800
# Node ID 1b015caba46cf6a26a238681836be933e9119bd5
# Parent  4c113c744b869b571f216806382813fb8872810c
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff

diff -r 4c113c744b86 -r 1b015caba46c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Nov 29 11:31:39 2009 -0800
+++ b/src/HOL/Finite_Set.thy	Thu Dec 17 07:02:13 2009 -0800
@@ -204,6 +204,9 @@
   qed
 qed
 
+lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A"
+by (rule finite_subset)
+
 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
 
@@ -355,6 +358,18 @@
   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   done
 
+lemma finite_vimageD:
+  assumes fin: "finite (h -` F)" and surj: "surj h"
+  shows "finite F"
+proof -
+  have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
+  also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
+  finally show "finite F" .
+qed
+
+lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
+  unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
+
 
 text {* The finite UNION of finite sets *}