summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 15 Jul 2003 08:25:20 +0200 | |

changeset 14111 | 993471c762b8 |

parent 14110 | c45c94fa16f4 |

child 14112 | 95d51043d2a3 |

Some new thm (ex_map_conv?)

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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