src/HOL/equalities.ML

 
 goal thy "f``(g``A) = (%x. f (g x)) `` A";
 by (Blast_tac 1);
 qed "image_image";
 
-qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
- (fn _ => [Blast_tac 1]);
-
 goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
 by (Blast_tac 1);
 qed "insert_image";
 Addsimps [insert_image];
 

 by (split_tac [expand_if] 1);
 by (Blast_tac 1);
 qed "if_image_distrib";
 Addsimps[if_image_distrib];
 
+val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
+by (rtac set_ext 1);
+by (simp_tac (simpset() addsimps image_def::prems) 1);
+qed "image_cong";
+
 
 section "Int";
 
 goal thy "A Int A = A";
 by (Blast_tac 1);

 qed "Inter_Un_distrib";
 
 section "UN and INT";
 
 (*Basic identities*)
+
+val not_empty = prove_goal Set.thy "A Û {} = (Ãx. xÎA)" (K [Blast_tac 1]);
+(*Addsimps[not_empty];*)
 
 goal thy "(UN x:{}. B x) = {}";
 by (Blast_tac 1);
 qed "UN_empty";
 Addsimps[UN_empty];

     ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
      "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
      "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
      "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
      "(ALL x:{}. P x) = True",
+     "(ALL x:UNIV. P x) = (ALL x. P x)",
      "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
      "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
      "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
      "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];

 
 val bex_simps = map prover
     ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
      "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
      "(EX x:{}. P x) = False",
+     "(EX x:UNIV. P x) = (EX x. P x)",
      "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
      "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
      "(EX x:f``A. P x) = (EX x:A. P(f x))",
      "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];