--- a/src/ZF/Perm.ML Mon Jul 27 11:29:33 1998 +0200
+++ b/src/ZF/Perm.ML Mon Jul 27 16:04:20 1998 +0200
@@ -247,6 +247,11 @@
AddIs [compI];
AddSEs [compE,idE];
+Goal "converse(R O S) = converse(S) O converse(R)";
+by (Blast_tac 1);
+qed "converse_comp";
+
+
(** Domain and Range -- see Suppes, section 3.1 **)
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
--- a/src/ZF/domrange.ML Mon Jul 27 11:29:33 1998 +0200
+++ b/src/ZF/domrange.ML Mon Jul 27 16:04:20 1998 +0200
@@ -49,6 +49,11 @@
Addsimps [converse_prod, converse_empty];
+val converse_subset_iff = prove_goal ZF.thy
+ "!!z. A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
+ (fn _=> [ (Blast_tac 1) ]);
+
+
(*** domain ***)
qed_goalw "domain_iff" ZF.thy [domain_def]
--- a/src/ZF/func.ML Mon Jul 27 11:29:33 1998 +0200
+++ b/src/ZF/func.ML Mon Jul 27 16:04:20 1998 +0200
@@ -234,6 +234,20 @@
Addsimps [eta];
+val fun_extension_iff = prove_goal ZF.thy
+ "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> (ALL a:A. f`a = g`a) <-> f=g"
+ (fn _=> [ (blast_tac (claset() addIs [fun_extension]) 1) ]);
+
+(*thanks to Mark Staples*)
+val fun_subset_eq = prove_goal ZF.thy
+ "!!z. [| f:Pi(A,B); g:Pi(A,C) |] ==> f <= g <-> (f = g)"
+ (fn _=>
+ [ (rtac iffI 1), (asm_full_simp_tac ZF_ss 2),
+ (rtac fun_extension 1), (REPEAT (atac 1)),
+ (dtac (apply_Pair RSN (2,subsetD)) 1), (REPEAT (atac 1)),
+ (rtac (apply_equality RS sym) 1), (REPEAT (atac 1)) ]);
+
+
(*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
val prems = goal ZF.thy
"[| f: Pi(A,B); \
--- a/src/ZF/simpdata.ML Mon Jul 27 11:29:33 1998 +0200
+++ b/src/ZF/simpdata.ML Mon Jul 27 16:04:20 1998 +0200
@@ -45,10 +45,11 @@
prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
val Rep_simps = map prover
- ["{x:0. P(x)} = 0",
+ ["{x. y:0, R(x,y)} = 0", (*Replace*)
+ "{x:0. P(x)} = 0", (*Collect*)
"{x:A. False} = 0",
"{x:A. True} = A",
- "RepFun(0,f) = 0",
+ "RepFun(0,f) = 0", (*RepFun*)
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]