src/HOL/Fun.ML
changeset 3341 89fe22bf9f54
parent 2935 998cb95fdd43
child 3842 b55686a7b22c
equal deleted inserted replaced
3340:a886795c9dce 3341:89fe22bf9f54
    94 by (rtac contrapos 1);
    94 by (rtac contrapos 1);
    95 by (etac (major RS inj_ontoD) 2);
    95 by (etac (major RS inj_ontoD) 2);
    96 by (REPEAT (resolve_tac prems 1));
    96 by (REPEAT (resolve_tac prems 1));
    97 qed "inj_onto_contraD";
    97 qed "inj_onto_contraD";
    98 
    98 
       
    99 goalw Fun.thy [inj_onto_def]
       
   100     "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
       
   101 by (Blast_tac 1);
       
   102 qed "subset_inj_onto";
       
   103 
    99 
   104 
   100 (*** Lemmas about inj ***)
   105 (*** Lemmas about inj ***)
   101 
   106 
   102 goalw Fun.thy [o_def]
   107 goalw Fun.thy [o_def]
   103     "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
   108     "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";