src/HOL/Typedef.thy
changeset 23433 c2c10abd2a1e
parent 23247 b99dce43d252
child 23710 a8ac2305eaf2
     1.1 --- a/src/HOL/Typedef.thy	Wed Jun 20 08:09:56 2007 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed Jun 20 14:38:24 2007 +0200
     1.3 @@ -90,6 +90,23 @@
     1.4    finally show "P x" .
     1.5  qed
     1.6  
     1.7 +lemma Rep_range:
     1.8 +assumes "type_definition Rep Abs A"
     1.9 +shows "range Rep = A"
    1.10 +proof -
    1.11 +  from assms have A1: "!!x. Rep x : A"
    1.12 +              and A2: "!!y. y : A ==> y = Rep(Abs y)"
    1.13 +     by (auto simp add: type_definition_def)
    1.14 +  have "range Rep <= A" using A1 by (auto simp add: image_def)
    1.15 +  moreover have "A <= range Rep"
    1.16 +  proof
    1.17 +    fix x assume "x : A"
    1.18 +    hence "x = Rep (Abs x)" by (rule A2)
    1.19 +    thus "x : range Rep" by (auto simp add: image_def)
    1.20 +  qed
    1.21 +  ultimately show ?thesis ..
    1.22 +qed
    1.23 +
    1.24  end
    1.25  
    1.26  use "Tools/typedef_package.ML"