Re: [Hol-info] Proof related to REAL_BIGNUM

[giovanni g. <g_g...@ya...>]

Hi Osman.
I can believe you had problems to prove your statement, because it's false.

This is the proof of its negation:

g `~(?n:num. !(r:real). r < &n)`;;
e (REWRITE_TAC [NOT_EXISTS_THM]);;
e (GEN_TAC THEN REWRITE_TAC [NOT_FORALL_THM]);;
e (EXISTS_TAC `&(SUC n)`);;
e (REWRITE_TAC [REAL_OF_NUM_LT]);;
e (ARITH_TAC);;
let THM = top_thm();;

Giovanni Gherdovich
Osman Hasan <o_...@en...> ha scritto:  Hi HOL users,

I am trying to prove the following theorem in HOL

|- ?(n:num). !(r:real). r < & n

It is somewhat related to the REAL_BIGNUM theorem found in the realTheory:

|- !r. ?n. r < &n

and by looking at this REAL_BIGNUM theorem my goal seems provable: As for
every real number there exists a greater 'num' so there must be a 'num'
which is greater than the greatest real number.

I tried using quite a few different approaches but couldnt succeed so far
and the main bottleneck being the fact that the existential quantifier is
outside the universal one.

Any feedback/clues would be greatly appreciated.
Thanks and best regards,
--Osman



-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
hol-info mailing list
hol...@li...
https://lists.sourceforge.net/lists/listinfo/hol-info


 Chiacchiera con i tuoi amici in tempo reale! 
 http://it.yahoo.com/mail_it/foot/*http://it.messenger.yahoo.com