# HG changeset patch
# User nipkow
# Date 1058250320 -7200
# Node ID 993471c762b86237c03522710d6c03e7cbdbc94e
# Parent  c45c94fa16f4d7355e77e8043c32860b0f004e54
Some new thm (ex_map_conv?)

diff -r c45c94fa16f4 -r 993471c762b8 src/HOL/List.thy
--- 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