author lcp Tue, 21 Dec 1993 13:58:12 +0100 changeset 198 0f0ff91b07f6 parent 197 7c7179e687b2 child 199 ac55692ab41f
new section for equality properties
 src/ZF/equalities.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/equalities.ML	Tue Dec 14 14:02:52 1993 +0100
+++ b/src/ZF/equalities.ML	Tue Dec 21 13:58:12 1993 +0100
@@ -322,3 +322,28 @@
by (fast_tac eq_cs 1);
val converse_diff = result();

+(** Pow **)
+
+goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";
+by (fast_tac upair_cs 1);
+val Un_Pow_subset = result();
+
+goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
+by (fast_tac upair_cs 1);
+val UN_Pow_subset = result();
+
+goal ZF.thy "A <= Pow(Union(A))";
+by (fast_tac upair_cs 1);
+val subset_Pow_Union = result();
+
+goal ZF.thy "Union(Pow(A)) = A";
+by (fast_tac eq_cs 1);
+val Union_Pow_eq = result();
+
+goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)";
+by (fast_tac eq_cs 1);
+val Int_Pow_eq = result();
+
+goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+by (fast_tac eq_cs 1);
+val INT_Pow_subset = result();```