Ah, thanks! sorry, I didn't see your replies before posting my last one.
Your proofs are much much shorter than mine, I'll use your versions instead!
--Chun
Il 16/02/19 22:48, Konrad Slind ha scritto:
> Rephrasing things might bring clarity:
>
> load "pred_setLib";
> open pred_setTheory;
>
>
Cancel above questions. They're finally proved by myself using
FINITE_WEAK_ENUMERATE, FINITE_BIJ_COUNT_EQ, etc. [1]
[infinity_bound_lemma] Theorem
⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N
[infinity_often_lemma] Theorem
⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n
This can be proved by contradiction, using the fact that the set of numbers
less than any given number is finite.
val lemB = Q.prove
(`!N m. INFINITE N ==> ?n. m <= n /\ n IN N`,
spose_not_then strip_assume_tac
>> `FINITE (count m)` by metis_tac [FINITE_COUNT]
>> `N SUBSET (count m)`
Rephrasing things might bring clarity:
load "pred_setLib";
open pred_setTheory;
val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss);
val lem = Q.prove
(`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`,
rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF]
>- (`FINITE P \/ ?n. P n
