# HG changeset patch
# User huffman
# Date 1187125555 -7200
# Node ID 4b2aac7669b3452d942a60912690f42cca613177
# Parent  9b4d7c59cc906c639ebc2d54936c5aed1d2990e6
remove redundant assumption from Rep_range lemma

diff -r 9b4d7c59cc90 -r 4b2aac7669b3 src/HOL/Typedef.thy
--- 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