# HG changeset patch
# User huffman
# Date 1213984665 -7200
# Node ID cfe5244301dd661c78eaf38d0234dc5cd63bc38a
# Parent  c11e716fafeb99caa12a077014ef8766af19efda
add lemma Abs_image

diff -r c11e716fafeb -r cfe5244301dd src/HOL/Typedef.thy
--- 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"