equal
deleted
inserted
replaced
|
1 (* Title: ZF/AC/AC16_WO4.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Gr`abczewski |
|
4 |
|
5 The proof of AC16(n, k) ==> WO4(n-k) |
|
6 *) |
1 |
7 |
2 open AC16_WO4; |
8 open AC16_WO4; |
3 |
9 |
4 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
5 (* The case of finite set *) |
11 (* The case of finite set *) |
445 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
451 by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
446 val well_ord_subsets_eqpoll_n = result(); |
452 val well_ord_subsets_eqpoll_n = result(); |
447 |
453 |
448 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
454 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
449 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
455 \ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
450 by (fast_tac (ZF_cs addSIs [le_refl, leI, |
456 by (fast_tac (ZF_cs addIs [le_refl, leI, |
451 le_imp_lepoll, equalityI] |
457 le_imp_lepoll, equalityI] |
452 addSDs [lepoll_succ_disj] |
458 addSDs [lepoll_succ_disj] |
453 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
459 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
454 val subsets_lepoll_succ = result(); |
460 val subsets_lepoll_succ = result(); |
455 |
461 |