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

[John H. <Joh...@cl...>]

Hi Giovanni,

| 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?

There is a definition, together with some useful lemmas, in a rather
obscure place: "Multivariate/misc.ml". I should probably move it
somewhere more accessible.

| 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?

No, you're right, it's not currently defined in HOL Light. I've
occasionally thought how useful it would be, but never taken the
plunge and added 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)))`

That looks good to me. If you get a nice series of lemmas about it,
I'd be happy to add them somewhere in the HOL Light distribution.

John.