equal
deleted
inserted
replaced
415 by (assume_tac 1); |
415 by (assume_tac 1); |
416 qed "well_ord_lepoll_imp_Card_le"; |
416 qed "well_ord_lepoll_imp_Card_le"; |
417 |
417 |
418 |
418 |
419 goal Cardinal.thy "!!A. [| A lepoll i; Ord(i) |] ==> |A| le i"; |
419 goal Cardinal.thy "!!A. [| A lepoll i; Ord(i) |] ==> |A| le i"; |
420 br le_trans 1; |
420 by (rtac le_trans 1); |
421 be (well_ord_Memrel RS well_ord_lepoll_imp_Card_le) 1; |
421 by (etac (well_ord_Memrel RS well_ord_lepoll_imp_Card_le) 1); |
422 ba 1; |
422 by (assume_tac 1); |
423 be Ord_cardinal_le 1; |
423 by (etac Ord_cardinal_le 1); |
424 qed "lepoll_cardinal_le"; |
424 qed "lepoll_cardinal_le"; |
425 |
425 |
426 |
426 |
427 (*** The finite cardinals ***) |
427 (*** The finite cardinals ***) |
428 |
428 |
673 by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1); |
673 by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1); |
674 by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1); |
674 by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1); |
675 by (split_tac [expand_if] 1); |
675 by (split_tac [expand_if] 1); |
676 by (fast_tac (ZF_cs addSIs [InlI, InrI]) 1); |
676 by (fast_tac (ZF_cs addSIs [InlI, InrI]) 1); |
677 by (asm_full_simp_tac (ZF_ss addsimps [Inl_def, Inr_def] |
677 by (asm_full_simp_tac (ZF_ss addsimps [Inl_def, Inr_def] |
678 setloop split_tac [expand_if]) 1); |
678 setloop split_tac [expand_if]) 1); |
679 qed "Un_lepoll_sum"; |
679 qed "Un_lepoll_sum"; |
680 |
680 |
681 |
681 |
682 (*** Finite and infinite sets ***) |
682 (*** Finite and infinite sets ***) |
683 |
683 |
698 by (fast_tac (ZF_cs addSEs [eqpollE] |
698 by (fast_tac (ZF_cs addSEs [eqpollE] |
699 addEs [lepoll_trans RS |
699 addEs [lepoll_trans RS |
700 rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1); |
700 rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1); |
701 qed "lepoll_Finite"; |
701 qed "lepoll_Finite"; |
702 |
702 |
703 bind_thm ("Finite_Diff", Diff_subset RS subset_imp_lepoll RS lepoll_Finite); |
703 bind_thm ("subset_Finite", subset_imp_lepoll RS lepoll_Finite); |
|
704 |
|
705 bind_thm ("Finite_Diff", Diff_subset RS subset_Finite); |
704 |
706 |
705 goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))"; |
707 goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))"; |
706 by (excluded_middle_tac "y:x" 1); |
708 by (excluded_middle_tac "y:x" 1); |
707 by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2); |
709 by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2); |
708 by (etac bexE 1); |
710 by (etac bexE 1); |
724 qed "nat_le_infinite_Ord"; |
726 qed "nat_le_infinite_Ord"; |
725 |
727 |
726 goalw Cardinal.thy [Finite_def, eqpoll_def] |
728 goalw Cardinal.thy [Finite_def, eqpoll_def] |
727 "!!A. Finite(A) ==> EX r. well_ord(A,r)"; |
729 "!!A. Finite(A) ==> EX r. well_ord(A,r)"; |
728 by (fast_tac (ZF_cs addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, |
730 by (fast_tac (ZF_cs addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel, |
729 nat_into_Ord]) 1); |
731 nat_into_Ord]) 1); |
730 qed "Finite_imp_well_ord"; |
732 qed "Finite_imp_well_ord"; |
731 |
733 |
732 |
734 |
733 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered |
735 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered |
734 set is well-ordered. Proofs simplified by lcp. *) |
736 set is well-ordered. Proofs simplified by lcp. *) |