# HG changeset patch
# User paulson
# Date 830939827 -7200
# Node ID 220dd588bfc9233b6ca12c77744f1ce7d4fdd8c8
# Parent  8f782b919043c88f8ada0b4149ca67b832d8e59d
New lemma inspired by KG

diff -r 8f782b919043 -r 220dd588bfc9 src/ZF/Cardinal.ML
--- 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);
 
diff -r 8f782b919043 -r 220dd588bfc9 src/ZF/Perm.ML
--- 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 |] ==> \