src/ZF/equalities.ML
changeset 198 0f0ff91b07f6
parent 192 3dc5c8016a0e
child 268 1a038ec6f923
equal deleted inserted replaced
197:7c7179e687b2 198:0f0ff91b07f6
   320 
   320 
   321 goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
   321 goal ZF.thy "converse(A) - converse(B) = converse(A - B)";
   322 by (fast_tac eq_cs 1);
   322 by (fast_tac eq_cs 1);
   323 val converse_diff = result();
   323 val converse_diff = result();
   324 
   324 
       
   325 (** Pow **)
       
   326 
       
   327 goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
       
   328 by (fast_tac upair_cs 1);
       
   329 val Un_Pow_subset = result();
       
   330 
       
   331 goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
       
   332 by (fast_tac upair_cs 1);
       
   333 val UN_Pow_subset = result();
       
   334 
       
   335 goal ZF.thy "A <= Pow(Union(A))";
       
   336 by (fast_tac upair_cs 1);
       
   337 val subset_Pow_Union = result();
       
   338 
       
   339 goal ZF.thy "Union(Pow(A)) = A";
       
   340 by (fast_tac eq_cs 1);
       
   341 val Union_Pow_eq = result();
       
   342 
       
   343 goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";
       
   344 by (fast_tac eq_cs 1);
       
   345 val Int_Pow_eq = result();
       
   346 
       
   347 goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
       
   348 by (fast_tac eq_cs 1);
       
   349 val INT_Pow_subset = result();