summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 35510 | 64d2d54cbf03 |

parent 35296 | 975b34b6cf5b |

child 35603 | c0db094d0d80 |

equal
deleted
inserted
replaced

35509:13e83ce8391b | 35510:64d2d54cbf03 |
---|---|

759 lemma ex_map_conv: |
759 lemma ex_map_conv: |

760 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)" |
760 "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)" |

761 by(induct ys, auto simp add: Cons_eq_map_conv) |
761 by(induct ys, auto simp add: Cons_eq_map_conv) |

762 |
762 |

763 lemma map_eq_imp_length_eq: |
763 lemma map_eq_imp_length_eq: |

764 assumes "map f xs = map f ys" |
764 assumes "map f xs = map g ys" |

765 shows "length xs = length ys" |
765 shows "length xs = length ys" |

766 using assms proof (induct ys arbitrary: xs) |
766 using assms proof (induct ys arbitrary: xs) |

767 case Nil then show ?case by simp |
767 case Nil then show ?case by simp |

768 next |
768 next |

769 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto |
769 case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto |

770 from Cons xs have "map f zs = map f ys" by simp |
770 from Cons xs have "map f zs = map g ys" by simp |

771 moreover with Cons have "length zs = length ys" by blast |
771 moreover with Cons have "length zs = length ys" by blast |

772 with xs show ?case by simp |
772 with xs show ?case by simp |

773 qed |
773 qed |

774 |
774 |

775 lemma map_inj_on: |
775 lemma map_inj_on: |