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; > > 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 <mailto: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 <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
