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

author | paulson |

Tue, 02 Mar 2010 17:36:16 +0000 | |

changeset 35510 | 64d2d54cbf03 |

parent 35509 | 13e83ce8391b |

child 35511 | 99b3fce7e475 |

Slightly generalised a theorem

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

--- a/src/HOL/List.thy Tue Mar 02 12:59:16 2010 +0000 +++ b/src/HOL/List.thy Tue Mar 02 17:36:16 2010 +0000 @@ -761,13 +761,13 @@ by(induct ys, auto simp add: Cons_eq_map_conv) lemma map_eq_imp_length_eq: - assumes "map f xs = map f ys" + assumes "map f xs = map g ys" shows "length xs = length ys" using assms proof (induct ys arbitrary: xs) case Nil then show ?case by simp next case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto - from Cons xs have "map f zs = map f ys" by simp + from Cons xs have "map f zs = map g ys" by simp moreover with Cons have "length zs = length ys" by blast with xs show ?case by simp qed