74 |
74 |
75 (*Proof simplified by LCP*) |
75 (*Proof simplified by LCP*) |
76 Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
76 Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
77 \ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
77 \ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
78 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
78 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
79 by (ALLGOALS |
79 by (auto_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type])); |
80 (asm_simp_tac |
|
81 (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] |
|
82 setloop (split_tac [split_if] ORELSE' Step_tac)))); |
|
83 qed "succ_not_lepoll_lemma"; |
80 qed "succ_not_lepoll_lemma"; |
84 |
81 |
85 Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] |
82 Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] |
86 "[| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
83 "[| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
87 by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
84 by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |