src/HOL/Typedef.thy
changeset 24269 4b2aac7669b3
parent 23710 a8ac2305eaf2
child 25535 4975b7529a14
     1.1 --- a/src/HOL/Typedef.thy	Tue Aug 14 23:04:27 2007 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Aug 14 23:05:55 2007 +0200
     1.3 @@ -91,20 +91,15 @@
     1.4  qed
     1.5  
     1.6  lemma Rep_range:
     1.7 -assumes "type_definition Rep Abs A"
     1.8 -shows "range Rep = A"
     1.9 -proof -
    1.10 -  from assms have A1: "!!x. Rep x : A"
    1.11 -              and A2: "!!y. y : A ==> y = Rep(Abs y)"
    1.12 -     by (auto simp add: type_definition_def)
    1.13 -  have "range Rep <= A" using A1 by (auto simp add: image_def)
    1.14 -  moreover have "A <= range Rep"
    1.15 +  shows "range Rep = A"
    1.16 +proof
    1.17 +  show "range Rep <= A" using Rep by (auto simp add: image_def)
    1.18 +  show "A <= range Rep"
    1.19    proof
    1.20      fix x assume "x : A"
    1.21 -    hence "x = Rep (Abs x)" by (rule A2)
    1.22 -    thus "x : range Rep" by (auto simp add: image_def)
    1.23 +    hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
    1.24 +    thus "x : range Rep" by (rule range_eqI)
    1.25    qed
    1.26 -  ultimately show ?thesis ..
    1.27  qed
    1.28  
    1.29  end