equal
deleted
inserted
replaced
486 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
486 by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); |
487 by (asm_simp_tac (simpset() addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
487 by (asm_simp_tac (simpset() addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); |
488 by (blast_tac (claset() addSEs [lt_irrefl]) 1); |
488 by (blast_tac (claset() addSEs [lt_irrefl]) 1); |
489 qed "nat_into_Card"; |
489 qed "nat_into_Card"; |
490 |
490 |
|
491 bind_thm ("cardinal_0", nat_0I RS nat_into_Card RS Card_cardinal_eq); |
|
492 bind_thm ("cardinal_1", nat_1I RS nat_into_Card RS Card_cardinal_eq); |
|
493 AddIffs [cardinal_0, cardinal_1]; |
|
494 |
491 (*Part of Kunen's Lemma 10.6*) |
495 (*Part of Kunen's Lemma 10.6*) |
492 Goal "[| succ(n) lepoll n; n:nat |] ==> P"; |
496 Goal "[| succ(n) lepoll n; n:nat |] ==> P"; |
493 by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); |
497 by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); |
494 by (REPEAT (ares_tac [nat_succI] 1)); |
498 by (REPEAT (ares_tac [nat_succI] 1)); |
495 qed "succ_lepoll_natE"; |
499 qed "succ_lepoll_natE"; |
621 |
625 |
622 Goal "|{a}| = 1"; |
626 Goal "|{a}| = 1"; |
623 by (resolve_tac [singleton_eqpoll_1 RS cardinal_cong RS trans] 1); |
627 by (resolve_tac [singleton_eqpoll_1 RS cardinal_cong RS trans] 1); |
624 by (simp_tac (simpset() addsimps [nat_into_Card RS Card_cardinal_eq]) 1); |
628 by (simp_tac (simpset() addsimps [nat_into_Card RS Card_cardinal_eq]) 1); |
625 qed "cardinal_singleton"; |
629 qed "cardinal_singleton"; |
|
630 |
|
631 Goal "A ~= 0 ==> 1 lepoll A"; |
|
632 by (etac not_emptyE 1); |
|
633 by (res_inst_tac [("a", "cons(x, A-{x})")] subst 1); |
|
634 by (res_inst_tac [("a", "cons(0,0)"), |
|
635 ("P", "%y. y lepoll cons(x, A-{x})")] subst 2); |
|
636 by (blast_tac (claset() addIs [cons_lepoll_cong, subset_imp_lepoll]) 3); |
|
637 by Auto_tac; |
|
638 qed "not_0_is_lepoll_1"; |
626 |
639 |
627 (*Congruence law for succ under equipollence*) |
640 (*Congruence law for succ under equipollence*) |
628 Goalw [succ_def] |
641 Goalw [succ_def] |
629 "A eqpoll B ==> succ(A) eqpoll succ(B)"; |
642 "A eqpoll B ==> succ(A) eqpoll succ(B)"; |
630 by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); |
643 by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); |
821 qed "Finite_well_ord_converse"; |
834 qed "Finite_well_ord_converse"; |
822 |
835 |
823 Goalw [Finite_def] "n:nat ==> Finite(n)"; |
836 Goalw [Finite_def] "n:nat ==> Finite(n)"; |
824 by (fast_tac (claset() addSIs [eqpoll_refl]) 1); |
837 by (fast_tac (claset() addSIs [eqpoll_refl]) 1); |
825 qed "nat_into_Finite"; |
838 qed "nat_into_Finite"; |
|
839 |
|
840 |