src/HOL/equalities.ML
changeset 7516 a1d476251238
parent 7127 48e235179ffb
child 7648 8258b93cdd32
equal deleted inserted replaced
7515:0c05469cad57 7516:a1d476251238
    99 Goal "f``insert a B = insert (f a) (f``B)";
    99 Goal "f``insert a B = insert (f a) (f``B)";
   100 by (Blast_tac 1);
   100 by (Blast_tac 1);
   101 qed "image_insert";
   101 qed "image_insert";
   102 Addsimps[image_insert];
   102 Addsimps[image_insert];
   103 
   103 
   104 Goal "(%x. x) `` Y = Y";
       
   105 by (Blast_tac 1);
       
   106 qed "image_id";
       
   107 Addsimps [image_id];
       
   108 
       
   109 Goal "x:A ==> (%x. c) `` A = {c}";
   104 Goal "x:A ==> (%x. c) `` A = {c}";
   110 by (Blast_tac 1);
   105 by (Blast_tac 1);
   111 qed "image_constant";
   106 qed "image_constant";
   112 
   107 
   113 Goal "f``(g``A) = (%x. f (g x)) `` A";
   108 Goal "f``(g``A) = (%x. f (g x)) `` A";
   616 section "-";
   611 section "-";
   617 
   612 
   618 Goal "A-B = A Int (-B)";
   613 Goal "A-B = A Int (-B)";
   619 by (Blast_tac 1);
   614 by (Blast_tac 1);
   620 qed "Diff_eq";
   615 qed "Diff_eq";
       
   616 
       
   617 Goal "(A-B = {}) = (A<=B)";
       
   618 by (Blast_tac 1);
       
   619 qed "Diff_eq_empty_iff";
       
   620 Addsimps[Diff_eq_empty_iff];
   621 
   621 
   622 Goal "A-A = {}";
   622 Goal "A-A = {}";
   623 by (Blast_tac 1);
   623 by (Blast_tac 1);
   624 qed "Diff_cancel";
   624 qed "Diff_cancel";
   625 Addsimps[Diff_cancel];
   625 Addsimps[Diff_cancel];