add lemma Abs_image
authorhuffman
Fri Jun 20 19:57:45 2008 +0200 (2008-06-20)
changeset 27295cfe5244301dd
parent 27294 c11e716fafeb
child 27296 eec7a1889ca5
add lemma Abs_image
src/HOL/Typedef.thy
     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"