changeset 14111 | 993471c762b8 |
parent 14099 | 55d244f3c86d |
child 14187 | 26dfcd0ac436 |
--- 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