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

author | huffman |

Tue, 14 Aug 2007 23:05:55 +0200 | |

changeset 24269 | 4b2aac7669b3 |

parent 24268 | 9b4d7c59cc90 |

child 24270 | f53b7dab4426 |

remove redundant assumption from Rep_range lemma

--- a/src/HOL/Typedef.thy Tue Aug 14 23:04:27 2007 +0200 +++ b/src/HOL/Typedef.thy Tue Aug 14 23:05:55 2007 +0200 @@ -91,20 +91,15 @@ qed lemma Rep_range: -assumes "type_definition Rep Abs A" -shows "range Rep = A" -proof - - from assms have A1: "!!x. Rep x : A" - and A2: "!!y. y : A ==> y = Rep(Abs y)" - by (auto simp add: type_definition_def) - have "range Rep <= A" using A1 by (auto simp add: image_def) - moreover have "A <= range Rep" + shows "range Rep = A" +proof + show "range Rep <= A" using Rep by (auto simp add: image_def) + show "A <= range Rep" proof fix x assume "x : A" - hence "x = Rep (Abs x)" by (rule A2) - thus "x : range Rep" by (auto simp add: image_def) + hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric]) + thus "x : range Rep" by (rule range_eqI) qed - ultimately show ?thesis .. qed end