equal
deleted
inserted
replaced
751 apply (unfold csucc_def) |
751 apply (unfold csucc_def) |
752 apply (rule LeastI) |
752 apply (rule LeastI) |
753 apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ |
753 apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+ |
754 done |
754 done |
755 |
755 |
756 lemmas Card_csucc = csucc_basic [THEN conjunct1, standard] |
756 lemmas Card_csucc = csucc_basic [THEN conjunct1] |
757 |
757 |
758 lemmas lt_csucc = csucc_basic [THEN conjunct2, standard] |
758 lemmas lt_csucc = csucc_basic [THEN conjunct2] |
759 |
759 |
760 lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" |
760 lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)" |
761 by (blast intro: Ord_0_le lt_csucc lt_trans1) |
761 by (blast intro: Ord_0_le lt_csucc lt_trans1) |
762 |
762 |
763 lemma csucc_le: "[| Card(L); K<L |] ==> csucc(K) le L" |
763 lemma csucc_le: "[| Card(L); K<L |] ==> csucc(K) le L" |
855 done |
855 done |
856 |
856 |
857 |
857 |
858 subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} |
858 subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*} |
859 |
859 |
860 lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard] |
860 lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel] |
861 |
861 |
862 lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n" |
862 lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n" |
863 apply (rule eqpoll_trans) |
863 apply (rule eqpoll_trans) |
864 apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym]) |
864 apply (rule well_ord_radd [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym]) |
865 apply (erule nat_implies_well_ord)+ |
865 apply (erule nat_implies_well_ord)+ |