Some new thm (ex_map_conv?)

--- a/src/HOL/List.thy	Mon Jul 14 14:44:06 2003 +0200
+++ b/src/HOL/List.thy	Tue Jul 15 08:25:20 2003 +0200
@@ -474,6 +474,10 @@
  "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
 by (cases ys) auto
 
+lemma ex_map_conv:
+  "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
+by(induct ys, auto)
+
 lemma map_injective:
  "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
 by (induct ys) auto