src/ZF/CardinalArith.ML
 changeset 516 1957113f0d7d parent 488 52f7447d4f1b child 517 a9f93400f307
```--- a/src/ZF/CardinalArith.ML	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Aug 12 12:51:34 1994 +0200
@@ -309,19 +309,24 @@

(*** Infinite Cardinals are Limit Ordinals ***)

-(*Using lam_injective might simplify this proof!*)
+goalw CardinalArith.thy [lepoll_def]
+    "!!i. nat <= A ==> succ(A) lepoll A";
+by (res_inst_tac [("x",
+    "lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
+by (res_inst_tac [("d", "%y. if(y:nat, nat_case(A,%z.z,y), y)")]
+    lam_injective 1);
+by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
+by (asm_simp_tac
+    (ZF_ss addsimps [nat_case_0, nat_case_succ, nat_0I, nat_succI]
+           setloop split_tac [expand_if]) 1);
+val nat_succ_lepoll = result();
+
goalw CardinalArith.thy [lepoll_def, inj_def]
"!!i. nat <= A ==> succ(A) lepoll A";
by (res_inst_tac [("x",
"lam z:succ(A). if(z=A, 0, if(z:nat, succ(z), z))")] exI 1);
by (rtac (lam_type RS CollectI) 1);
-by (rtac if_type 1);
-by (etac ([asm_rl, nat_0I] MRS subsetD) 1);
-by (etac succE 1);
-by (contr_tac 1);
-by (rtac if_type 1);
-by (assume_tac 2);
-by (etac ([asm_rl, nat_succI] MRS subsetD) 1 THEN assume_tac 1);
+by (fast_tac (ZF_cs addSIs [if_type, nat_0I, nat_succI]) 1);
by (REPEAT (rtac ballI 1));
by (asm_simp_tac
(ZF_ss addsimps [succ_inject_iff, succ_not_0, succ_not_0 RS not_sym]```