Add support of "SUC" aliens in REAL_LINEAR_PROVER (for REAL_ARITH)

[binghe]

Hi,

recently I ported HOL-Light's latest version of REAL_ARITH to HOL4 [1] as an alternative of the old port by Joe Hurd in 1998, which doesn't support rational-valued coefficients and max, min, etc. and has created extra difficulties when porting some HOL-Light proofs to HOL4. During this porting work, I found a possible minor improvement to your REAL_LINEAR_PROVER. Konrad Slind suggested me to send my findings to "upstream", here.

In REAL_LINEAR_PROVER, when it's preparing for the lists of "le" inequalities, all terms like &n are treated as "alien" terms, and eventually additional inequalities like &n >= 0 are also added. But if the terms look like &(SUC n), it's still treated as &(SUC n) >= 0, which can be sharpened to &(SUC n) > 0.

After my changes, REAL_ARITH will be able to prove the following statements which is previously impossible:

# REAL_ARITH `&0 < &(SUC n)`;;
val it : thm = |- &0 < &(SUC n)

Regards, Chun Tian

[1] https://github.com/HOL-Theorem-Prover/HOL/pull/1043

[jrh13]

Belated thanks, just merged

[binghe]

Thanks.