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

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

hallo.

First of all, excuse me for posting my last message
after other answers were already written: it was a
synchronization problem, the last messages were 
delivered to me after I wrote mine.

> Your original goal cannot true.  For example, if P
> contains all reals,
> then inf P is negative infinity, which is not a
> real.  But inf P must be
> a real, for otherwise "inf P IN P" would not even
> type-check.

Actually, Osman put the statement "inf P IN P" in the
hypotheses so, according to the Hol type system,
the case "inf P = -inf" shouldn't be in the game.
Anyway, it can be that "inf Q = -inf", so the problem
arises with the conclusion, that cannot be
type-checked.

> For your goal to be true, either the type "real" has
> to be extended with
> negative infinity, or your goal has to be refined by
> saying that both P
> and Q have real lower bounds.

I think it's a shame that we cannot do proofs like
the one of Osman's statement, because we are used to 
that kind of theorems in "blackboard maths".

I didn't find the definition of infimum in any file
of Hol Light; did I miss some libraries, or it isn't
at all?

I've got a question too:
I would like to express powers with integer exponent.
It seems to be not defined yet, isn't it?
If so, I'm going to define somthing like

let (pow_int:real->int->real) = new_definition
`a pow_int b = if b >= 0 then a pow (num_of_int b)
               else inv(a pow (num_of_int (--b)))`

Regards

Giovanni Gherdovich


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