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 /\ ~P n` by metis_tac []
>> imp_res_tac SUBSET_FINITE
>> full_simp_tac std_ss [SUBSET_DEF, IN_DEF])
>- metis_tac[]);
>From this and the original assumption, you should be able to get that P is
finite, so has a maximum element.
Konrad.
On Fri, Feb 15, 2019 at 1:12 PM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> Hi,
>
> I'm blocked at the following (strange) situation:
>
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
>
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>
> ?m. !n. m <= n ==> ~(P n)
>
> Thanks in advance,
>
> Chun Tian
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
