Some new thm (ex_map_conv?)
authornipkow
Tue Jul 15 08:25:20 2003 +0200 (2003-07-15)
changeset 14111993471c762b8
parent 14110 c45c94fa16f4
child 14112 95d51043d2a3
Some new thm (ex_map_conv?)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon Jul 14 14:44:06 2003 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Jul 15 08:25:20 2003 +0200
     1.3 @@ -474,6 +474,10 @@
     1.4   "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
     1.5  by (cases ys) auto
     1.6  
     1.7 +lemma ex_map_conv:
     1.8 +  "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
     1.9 +by(induct ys, auto)
    1.10 +
    1.11  lemma map_injective:
    1.12   "!!xs. map f xs = map f ys ==> (\<forall>x y. f x = f y --> x = y) ==> xs = ys"
    1.13  by (induct ys) auto