src/HOL/Fun.ML
changeset 2499 0bc87b063447
parent 2031 03a843f0f447
child 2890 f27002fc531d
     1.1 --- a/src/HOL/Fun.ML	Thu Jan 09 10:22:42 1997 +0100
     1.2 +++ b/src/HOL/Fun.ML	Thu Jan 09 10:23:39 1997 +0100
     1.3 @@ -35,14 +35,15 @@
     1.4  by (REPEAT (ares_tac prems 1));
     1.5  qed "imageE";
     1.6  
     1.7 +AddIs  [imageI]; 
     1.8 +AddSEs [imageE]; 
     1.9 +
    1.10  goalw Fun.thy [o_def] "(f o g)``r = f``(g``r)";
    1.11 -by (rtac set_ext 1);
    1.12 -by (fast_tac (!claset addIs [imageI] addSEs [imageE]) 1);
    1.13 +by (Fast_tac 1);
    1.14  qed "image_compose";
    1.15  
    1.16  goal Fun.thy "f``(A Un B) = f``A Un f``B";
    1.17 -by (rtac set_ext 1);
    1.18 -by (fast_tac (!claset addIs [imageI,UnCI] addSEs [imageE,UnE]) 1);
    1.19 +by (Fast_tac 1);
    1.20  qed "image_Un";
    1.21  
    1.22  (*** Range of a function -- just a translation for image! ***)
    1.23 @@ -108,7 +109,7 @@
    1.24  
    1.25  val prems = goalw Fun.thy [inj_onto_def]
    1.26      "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
    1.27 -by (fast_tac (!claset addIs prems addSIs [ballI]) 1);
    1.28 +by (fast_tac (!claset addIs prems) 1);
    1.29  qed "inj_ontoI";
    1.30  
    1.31  val [major] = goal Fun.thy 
    1.32 @@ -141,7 +142,7 @@
    1.33  val prems = goalw Fun.thy [o_def]
    1.34      "[| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
    1.35  by (cut_facts_tac prems 1);
    1.36 -by (fast_tac (!claset addIs [injI,rangeI]
    1.37 +by (fast_tac (!claset addIs [injI]
    1.38                       addEs [injD,inj_ontoD]) 1);
    1.39  qed "comp_inj";
    1.40  
    1.41 @@ -163,20 +164,12 @@
    1.42      "[| inj(f);  A<=range(f) |] ==> inj_onto (Inv f) A";
    1.43  by (cut_facts_tac prems 1);
    1.44  by (fast_tac (!claset addIs [inj_ontoI] 
    1.45 -                     addEs [Inv_injective,injD,subsetD]) 1);
    1.46 +                      addEs [Inv_injective,injD]) 1);
    1.47  qed "inj_onto_Inv";
    1.48  
    1.49  
    1.50 -(*** Set reasoning tools ***)
    1.51 -
    1.52 -AddSIs [ballI, PowI, subsetI, InterI, INT_I, INT1_I, CollectI, 
    1.53 -            ComplI, IntI, DiffI, UnCI, insertCI]; 
    1.54 -AddIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI]; 
    1.55 -AddSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
    1.56 -            make_elim singleton_inject,
    1.57 -            CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE]; 
    1.58 -AddEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
    1.59 -            subsetD, subsetCE];
    1.60 +AddIs  [rangeI]; 
    1.61 +AddSEs [rangeE]; 
    1.62  
    1.63  val set_cs = !claset delrules [equalityI];
    1.64