--- a/src/ZF/Cardinal.ML Wed May 01 10:35:06 1996 +0200
+++ b/src/ZF/Cardinal.ML Wed May 01 10:37:07 1996 +0200
@@ -120,6 +120,11 @@
by (fast_tac (ZF_cs addIs [lepoll_0_is_0, lepoll_refl]) 1);
qed "lepoll_0_iff";
+goalw Cardinal.thy [lepoll_def]
+ "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] ==> A Un C lepoll B Un D";
+by (fast_tac (ZF_cs addIs [inj_disjoint_Un]) 1);
+qed "Un_lepoll_Un";
+
(*A eqpoll 0 ==> A=0*)
bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0);
--- a/src/ZF/Perm.ML Wed May 01 10:35:06 1996 +0200
+++ b/src/ZF/Perm.ML Wed May 01 10:37:07 1996 +0200
@@ -459,8 +459,17 @@
(** Unions of functions -- cf similar theorems on func.ML **)
-(*For proof of analogous theorem for injections, see
- AC/Cardinal_aux/Un_lepoll_Un*)
+(*Theorem by KG, proof by LCP*)
+goal Perm.thy
+ "!!f g. [| f: inj(A,B); g: inj(C,D); B Int D = 0 |] ==> \
+\ (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
+by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
+ lam_injective 1);
+by (ALLGOALS
+ (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse]
+ setloop (split_tac [expand_if] ORELSE' etac UnE))));
+by (fast_tac (ZF_cs addSEs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
+qed "inj_disjoint_Un";
goalw Perm.thy [surj_def]
"!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \