# HG changeset patch
# User paulson
# Date 1045735824 -3600
# Node ID ef4c41e7956affc33f9b96a4f64625fc690e5e47
# Parent  e4d8dea6dfc2998dbcdbf32c940a170b3bcb8136
new inverse image lemmas

diff -r e4d8dea6dfc2 -r ef4c41e7956a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 20 11:09:48 2003 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Feb 20 11:10:24 2003 +0100
@@ -119,16 +119,6 @@
   apply blast
   done
 
-lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
-  -- {* The image of a finite set is finite. *}
-  by (induct set: Finites) simp_all
-
-lemma finite_range_imageI:
-    "finite (range g) ==> finite (range (%x. f (g x)))"
-  apply (drule finite_imageI)
-  apply simp
-  done
-
 lemma finite_empty_induct:
   "finite A ==>
   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"
@@ -173,6 +163,18 @@
   done
 
 
+subsubsection {* Image and Inverse Image over Finite Sets *}
+
+lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
+  -- {* The image of a finite set is finite. *}
+  by (induct set: Finites) simp_all
+
+lemma finite_range_imageI:
+    "finite (range g) ==> finite (range (%x. f (g x)))"
+  apply (drule finite_imageI)
+  apply simp
+  done
+
 lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
 proof -
   have aux: "!!A. finite (A - {}) = finite A" by simp
@@ -195,6 +197,22 @@
 qed (rule refl)
 
 
+lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
+  -- {* The inverse image of a singleton under an injective function
+         is included in a singleton. *}
+  apply (auto simp add: inj_on_def) 
+  apply (blast intro: the_equality [symmetric]) 
+  done
+
+lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
+  -- {* The inverse image of a finite set under an injective function
+         is finite. *}
+  apply (induct set: Finites, simp_all) 
+  apply (subst vimage_insert) 
+  apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton]) 
+  done
+
+
 subsubsection {* The finite UNION of finite sets *}
 
 lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"