src/HOL/Set.ML
changeset 2912 3fac3e8d5d3e
parent 2891 d8f254ad1ab9
child 2935 998cb95fdd43
     1.1 --- a/src/HOL/Set.ML	Fri Apr 04 16:27:39 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Apr 04 16:33:28 1997 +0200
     1.3 @@ -602,6 +602,51 @@
     1.4  AddEs  [InterD, InterE];
     1.5  
     1.6  
     1.7 +(*** Image of a set under a function ***)
     1.8 +
     1.9 +(*Frequently b does not have the syntactic form of f(x).*)
    1.10 +val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
    1.11 +by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
    1.12 +qed "image_eqI";
    1.13 +
    1.14 +bind_thm ("imageI", refl RS image_eqI);
    1.15 +
    1.16 +(*The eta-expansion gives variable-name preservation.*)
    1.17 +val major::prems = goalw thy [image_def]
    1.18 +    "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
    1.19 +by (rtac (major RS CollectD RS bexE) 1);
    1.20 +by (REPEAT (ares_tac prems 1));
    1.21 +qed "imageE";
    1.22 +
    1.23 +AddIs  [image_eqI];
    1.24 +AddSEs [imageE]; 
    1.25 +
    1.26 +goalw thy [o_def] "(f o g)``r = f``(g``r)";
    1.27 +by (Fast_tac 1);
    1.28 +qed "image_compose";
    1.29 +
    1.30 +goal thy "f``(A Un B) = f``A Un f``B";
    1.31 +by (Fast_tac 1);
    1.32 +qed "image_Un";
    1.33 +
    1.34 +
    1.35 +(*** Range of a function -- just a translation for image! ***)
    1.36 +
    1.37 +goal thy "!!b. b=f(x) ==> b : range(f)";
    1.38 +by (EVERY1 [etac image_eqI, rtac UNIV_I]);
    1.39 +bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI));
    1.40 +
    1.41 +bind_thm ("rangeI", UNIV_I RS imageI);
    1.42 +
    1.43 +val [major,minor] = goal thy 
    1.44 +    "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
    1.45 +by (rtac (major RS imageE) 1);
    1.46 +by (etac minor 1);
    1.47 +qed "rangeE";
    1.48 +
    1.49 +AddIs  [rangeI]; 
    1.50 +AddSEs [rangeE]; 
    1.51 +
    1.52  
    1.53  (*** Set reasoning tools ***)
    1.54