1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Feb 19 15:57:34 2004 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Feb 19 16:44:21 2004 +0100
     1.3 @@ -51,6 +51,23 @@
     1.4  apply (fast intro: someI2)
     1.5  done
     1.6  
     1.7 +lemma Inv_f_eq:
     1.8 +  "[| inj_on f A; f x = y; x : A |] ==> Inv A f y = x"
     1.9 +  apply (erule subst)
    1.10 +  apply (erule Inv_f_f)
    1.11 +  apply assumption
    1.12 +  done
    1.13 +
    1.14 +lemma Inv_comp:
    1.15 +  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
    1.16 +  Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
    1.17 +  apply simp
    1.18 +  apply (rule Inv_f_eq)
    1.19 +    apply (fast intro: comp_inj_on)
    1.20 +   apply (simp add: f_Inv_f Inv_mem)
    1.21 +  apply (simp add: Inv_mem)
    1.22 +  done
    1.23 +
    1.24  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.25    -- {* dynamically-scoped fact for TFL *}
    1.26    by (blast intro: someI)