Re: [Hol-info] Proof related to REAL_BIGNUM - powers with integerexp

[Chou, Ching-T. <chi...@in...>]

>Actually, Osman put the statement "inf P IN P" in the
>hypotheses so, according to the Hol type system,
>the case "inf P =3D -inf" shouldn't be in the game.

I haven't used HOL for a long time.  But last time I checked, HOL
implements a logic of TOTAL functions.  Therefor, if inf has type
(real->bool)->real (as the expression "inf P in P" implies), then inf P
must denote a real even when P is not bounded from below.  So "inf P IN
P" does not imply that inf P is not -inf.

This is of course somewhat counterintuitive, but it is a necessary
consequence of using a logic of total functions and there are other
"anomalies" (e.g., "1/0 < 1/0 + 1" should be provable in HOL).  One can
envision using a logic of partial functions and some theorem provers do
do that.  But that approach is not without its own complexities.

- Ching Tsun