src/HOL/Hilbert_Choice.thy
changeset 23433 c2c10abd2a1e
parent 22690 0b08f218f260
child 26072 f65a7fa2da6c
     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