src/HOL/Set.ML
changeset 11007 438f31613093
parent 10832 e33b47e4246d
child 11166 eca861fd1eb5
     1.1 --- a/src/HOL/Set.ML	Wed Jan 31 10:13:22 2001 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Jan 31 10:15:01 2001 +0100
     1.3 @@ -530,6 +530,10 @@
     1.4  qed "singleton_conv2";
     1.5  Addsimps [singleton_conv2];
     1.6  
     1.7 +Goal "[| A - {x} <= B; x : A |] ==> A <= insert x B"; 
     1.8 +by(Blast_tac 1);
     1.9 +qed "diff_single_insert";
    1.10 +
    1.11  
    1.12  section "Unions of families -- UNION x:A. B(x) is Union(B`A)";
    1.13  
    1.14 @@ -687,13 +691,19 @@
    1.15  by (Blast_tac 1);
    1.16  qed "image_subset_iff";
    1.17  
    1.18 +Goal "B <= f ` A = (? AA. AA <= A & B = f ` AA)";
    1.19 +by Safe_tac;
    1.20 +by  (Fast_tac 2);
    1.21 +by (res_inst_tac [("x","{a. a : A & f a : B}")] exI 1);
    1.22 +by (Fast_tac 1);
    1.23 +qed "subset_image_iff";
    1.24 +
    1.25  (*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
    1.26    many existing proofs.*)
    1.27  val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f`A <= B";
    1.28  by (blast_tac (claset() addIs prems) 1);
    1.29  qed "image_subsetI";
    1.30  
    1.31 -
    1.32  (*** Range of a function -- just a translation for image! ***)
    1.33  
    1.34  Goal "b=f(x) ==> b : range(f)";