added lemmas
authornipkow
Wed Jun 20 14:38:24 2007 +0200 (2007-06-20)
changeset 23433c2c10abd2a1e
parent 23432 cec811764a38
child 23434 b2e7d4c29614
added lemmas
src/HOL/Hilbert_Choice.thy
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jun 20 08:09:56 2007 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jun 20 14:38:24 2007 +0200
     1.3 @@ -126,6 +126,16 @@
     1.4  apply (blast intro: inj_on_inverseI inv_f_f)
     1.5  done
     1.6  
     1.7 +lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
     1.8 +by (simp add: inj_iff)
     1.9 +
    1.10 +lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
    1.11 +by (simp add: o_assoc[symmetric])
    1.12 +
    1.13 +lemma inv_image_cancel[simp]:
    1.14 +  "inj f ==> inv f ` f ` S = S"
    1.15 +by (simp add: image_compose[symmetric])
    1.16 + 
    1.17  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
    1.18  by (blast intro: surjI inv_f_f)
    1.19  
     2.1 --- a/src/HOL/Typedef.thy	Wed Jun 20 08:09:56 2007 +0200
     2.2 +++ b/src/HOL/Typedef.thy	Wed Jun 20 14:38:24 2007 +0200
     2.3 @@ -90,6 +90,23 @@
     2.4    finally show "P x" .
     2.5  qed
     2.6  
     2.7 +lemma Rep_range:
     2.8 +assumes "type_definition Rep Abs A"
     2.9 +shows "range Rep = A"
    2.10 +proof -
    2.11 +  from assms have A1: "!!x. Rep x : A"
    2.12 +              and A2: "!!y. y : A ==> y = Rep(Abs y)"
    2.13 +     by (auto simp add: type_definition_def)
    2.14 +  have "range Rep <= A" using A1 by (auto simp add: image_def)
    2.15 +  moreover have "A <= range Rep"
    2.16 +  proof
    2.17 +    fix x assume "x : A"
    2.18 +    hence "x = Rep (Abs x)" by (rule A2)
    2.19 +    thus "x : range Rep" by (auto simp add: image_def)
    2.20 +  qed
    2.21 +  ultimately show ?thesis ..
    2.22 +qed
    2.23 +
    2.24  end
    2.25  
    2.26  use "Tools/typedef_package.ML"