src/HOL/Typedef.thy
changeset 27295 cfe5244301dd
parent 26802 9eede540a5e8
child 28083 103d9282a946
     1.1 --- a/src/HOL/Typedef.thy	Fri Jun 20 18:03:01 2008 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Fri Jun 20 19:57:45 2008 +0200
     1.3 @@ -90,8 +90,7 @@
     1.4    ultimately show "P x" by simp
     1.5  qed
     1.6  
     1.7 -lemma Rep_range:
     1.8 -  shows "range Rep = A"
     1.9 +lemma Rep_range: "range Rep = A"
    1.10  proof
    1.11    show "range Rep <= A" using Rep by (auto simp add: image_def)
    1.12    show "A <= range Rep"
    1.13 @@ -102,6 +101,19 @@
    1.14    qed
    1.15  qed
    1.16  
    1.17 +lemma Abs_image: "Abs ` A = UNIV"
    1.18 +proof
    1.19 +  show "Abs ` A <= UNIV" by (rule subset_UNIV)
    1.20 +next
    1.21 +  show "UNIV <= Abs ` A"
    1.22 +  proof
    1.23 +    fix x
    1.24 +    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
    1.25 +    moreover have "Rep x : A" by (rule Rep)
    1.26 +    ultimately show "x : Abs ` A" by (rule image_eqI)
    1.27 +  qed
    1.28 +qed
    1.29 +
    1.30  end
    1.31  
    1.32  use "Tools/typedef_package.ML"