# HG changeset patch
# User paulson
# Date 830939894 -7200
# Node ID f50ec5b35937c25c253c470cd0440f24d5937f74
# Parent  220dd588bfc9233b6ca12c77744f1ce7d4fdd8c8
Simplified KG's proofs

diff -r 220dd588bfc9 -r f50ec5b35937 src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Wed May 01 10:37:07 1996 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Wed May 01 10:38:14 1996 +0200
@@ -85,13 +85,14 @@
 (*      to {v:Pow(x). v eqpoll n-k}                                       *)
 (* ********************************************************************** *)
 
+(*Proof simplified by LCP*)
 goal thy "!!A. [| ~(EX x:A. f`x=y); f : inj(A, B); y:B |]  \
 \       ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
-by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]
-                addIs [expand_if RS iffD2]) 1);
-by (REPEAT (split_tac [expand_if] 1));
-by (fast_tac (AC_cs addSEs [left_inverse]) 1);
+by (ALLGOALS
+    (asm_simp_tac 
+     (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] 
+      setloop (split_tac [expand_if] ORELSE' step_tac ZF_cs))));
 val succ_not_lepoll_lemma = result();
 
 goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def]
diff -r 220dd588bfc9 -r f50ec5b35937 src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Wed May 01 10:37:07 1996 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Wed May 01 10:38:14 1996 +0200
@@ -65,31 +65,8 @@
     THEN REPEAT (assume_tac 1));
 val Un_eqpoll_Inf_Ord = result();
 
-goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |]  \
-\                       ==> A Un C lepoll B Un D";
-by (REPEAT (etac exE 1));
-by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1);
-by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")]
-        lam_injective 1);
-by (split_tac [expand_if] 1);
-by (etac UnE 1);
-by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
-by (rtac conjI 1);
-by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
-by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1);
-by (REPEAT (split_tac [expand_if] 1));
-by (rtac conjI 1);
-by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type]
-        addEs [swap]) 1);
-by (rtac impI 1);
-by (etac UnE 1);
-by (contr_tac 1);
-by (rtac conjI 1);
-by (rtac impI 1);
-by (etac equals0D 1);
-by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
-by (fast_tac (AC_cs addSEs [left_inverse]) 1);
-val Un_lepoll_Un = result();
+val ss = ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] 
+               setloop (split_tac [expand_if] ORELSE' etac UnE);
 
 goal ZF.thy "{x, y} - {y} = {x} - {y}";
 by (fast_tac eq_cs 1);