# HG changeset patch
# User paulson
# Date 901548260 -7200
# Node ID 084ceb3844f5b52f7429f45619f36f4960be34b9
# Parent  fac6fea3b7827e23d9a92c16ec18a0085150e3a6
A few new lemmas by Mark Staples

diff -r fac6fea3b782 -r 084ceb3844f5 src/ZF/Perm.ML
--- 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*)
diff -r fac6fea3b782 -r 084ceb3844f5 src/ZF/domrange.ML
--- 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]
diff -r fac6fea3b782 -r 084ceb3844f5 src/ZF/func.ML
--- 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);        \
diff -r fac6fea3b782 -r 084ceb3844f5 src/ZF/simpdata.ML
--- 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))"]