New rule: image_subset
authorpaulson
Thu Jan 08 11:24:46 1998 +0100 (1998-01-08)
changeset 452316f5efe9812d
parent 4522 0218c486cf07
child 4524 7399288f5dd3
New rule: image_subset
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Jan 08 11:23:18 1998 +0100
     1.2 +++ b/src/HOL/Set.ML	Thu Jan 08 11:24:46 1998 +0100
     1.3 @@ -612,6 +612,13 @@
     1.4  by (Blast_tac 1);
     1.5  qed "image_iff";
     1.6  
     1.7 +(*This rewrite rule would confuse users if made default.*)
     1.8 +goal thy "(f``A <= B) = (ALL x:A. f(x): B)";
     1.9 +by (Blast_tac 1);
    1.10 +qed "image_subset_iff";
    1.11 +
    1.12 +(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too
    1.13 +  many existing proofs.*)
    1.14  val prems = goal thy "(!!x. x:A ==> f(x) : B) ==> f``A <= B";
    1.15  by (blast_tac (claset() addIs prems) 1);
    1.16  qed "image_subsetI";