--- a/src/HOL/Typedef.thy Wed Jun 20 08:09:56 2007 +0200
+++ b/src/HOL/Typedef.thy Wed Jun 20 14:38:24 2007 +0200
@@ -90,6 +90,23 @@
finally show "P x" .
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"
+ proof
+ fix x assume "x : A"
+ hence "x = Rep (Abs x)" by (rule A2)
+ thus "x : range Rep" by (auto simp add: image_def)
+ qed
+ ultimately show ?thesis ..
+qed
+
end
use "Tools/typedef_package.ML"