src/HOL/Hilbert_Choice_lemmas.ML
changeset 13585 db4005b40cc6
parent 12459 6978ab7cac64
     1.1 --- a/src/HOL/Hilbert_Choice_lemmas.ML	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice_lemmas.ML	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -212,10 +212,6 @@
     1.4  
     1.5  section "Inverse of a PI-function (restricted domain)";
     1.6  
     1.7 -Goalw [Inv_def] "f ` A = B ==> (%x:B. (Inv A f) x) : B funcset A";
     1.8 -by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
     1.9 -qed "Inv_funcset";
    1.10 -
    1.11  Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
    1.12  by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
    1.13  by (blast_tac (claset() addIs [someI2]) 1); 
    1.14 @@ -236,15 +232,6 @@
    1.15  by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
    1.16  qed "inj_on_Inv";
    1.17  
    1.18 -Goal "[| inj_on f A;  f ` A = B |] \
    1.19 -\     ==> compose A (%y:B. (Inv A f) y) f = (%x:A. x)";
    1.20 -by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
    1.21 -by (rtac restrict_ext 1); 
    1.22 -by Auto_tac; 
    1.23 -by (etac subst 1); 
    1.24 -by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
    1.25 -qed "compose_Inv_id";
    1.26 -
    1.27  
    1.28  
    1.29  section "split and SOME";