author paulson Mon, 22 Feb 1999 10:19:32 +0100 changeset 6288 694c9c1910e8 parent 6287 61904a3eafaa child 6289 062aa156a300
new theorems Pow_0 and Pow_insert; renamed other Pow theorems
 src/ZF/equalities.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/equalities.ML	Mon Feb 22 10:16:59 1999 +0100
+++ b/src/ZF/equalities.ML	Mon Feb 22 10:19:32 1999 +0100
@@ -555,6 +555,18 @@

(** Pow **)

+Goal "Pow(0) = {0}";
+by (Blast_tac 1);
+qed "Pow_0";
+
+Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}";
+br equalityI 1;
+by Safe_tac;
+by (etac swap 1);
+by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);
+by (ALLGOALS Blast_tac);
+qed "Pow_insert";
+
Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
by (Blast_tac 1);
qed "Un_Pow_subset";
@@ -573,13 +585,13 @@

Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
by (Blast_tac 1);
-qed "Int_Pow_eq";
+qed "Pow_Int_eq";

-Goal "x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
+Goal "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
by (Blast_tac 1);
-qed "INT_Pow_subset";
+qed "Pow_INT_eq";