src/HOL/Fun.ML
changeset 7536 5c094aec523d
parent 7514 3235863a069a
child 7876 1b3b683c092e
equal deleted inserted replaced
7535:599d3414b51d 7536:5c094aec523d
    64 Addsimps [o_id];
    64 Addsimps [o_id];
    65 
    65 
    66 Goalw [o_def] "(f o g)``r = f``(g``r)";
    66 Goalw [o_def] "(f o g)``r = f``(g``r)";
    67 by (Blast_tac 1);
    67 by (Blast_tac 1);
    68 qed "image_compose";
    68 qed "image_compose";
       
    69 
       
    70 Goal "f``g``A = (UN x:A. {f (g x)})";
       
    71 by (Blast_tac 1);
       
    72 qed "image_image_eq_UN";
    69 
    73 
    70 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
    74 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
    71 by (Blast_tac 1);
    75 by (Blast_tac 1);
    72 qed "UN_o";
    76 qed "UN_o";
    73 
    77