--- a/src/HOL/Typedef.thy Fri Jun 20 18:03:01 2008 +0200
+++ b/src/HOL/Typedef.thy Fri Jun 20 19:57:45 2008 +0200
@@ -90,8 +90,7 @@
ultimately show "P x" by simp
qed
-lemma Rep_range:
- shows "range Rep = A"
+lemma Rep_range: "range Rep = A"
proof
show "range Rep <= A" using Rep by (auto simp add: image_def)
show "A <= range Rep"
@@ -102,6 +101,19 @@
qed
qed
+lemma Abs_image: "Abs ` A = UNIV"
+proof
+ show "Abs ` A <= UNIV" by (rule subset_UNIV)
+next
+ show "UNIV <= Abs ` A"
+ proof
+ fix x
+ have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
+ moreover have "Rep x : A" by (rule Rep)
+ ultimately show "x : Abs ` A" by (rule image_eqI)
+ qed
+qed
+
end
use "Tools/typedef_package.ML"