[isabelle] a new power operator


I'm looking for a power operator for real numbers that is closer to the
mathematical conventions of real analysis than either ^ or powr. if we
denote it by **, my requirements from it are

1. its type is "real => real => real".
2. 0**y is undefined for y<=0.
    (formally it can be (THE x. False). note that the definition of '0^0=1'
is appropriate in algebra, combinatorics and set theory, but not in
3. for negative base and real integer exponent (that is, reals in the set
Ints) the result should be the expected one.
    (powr, which is defined using the logarithm of the base, doesn't
satisfy this.)

I'd like to know if anybody have already developed such an operator. If not
I guess I'll try it myself. a possible definition is

  definition mrpow :: "real â real â real"
    (infixr "**" 80)
    where "x ** y == if   x>0
                     then (x powr y)
                     else (if   x=0
                           then (if   y>0
                                 then 0
                                 else (THE z::real. False))
                           else (if   y â Ints
                                 then (if   y â 0
                                       then    x ^(nat(  floor y))
                                       else (1/x)^(nat(- floor y)))
                                 else (THE z::real. False)

and if necessary I'll work on proving its properties until it is easy to
use. again any comments or suggestions are welcome.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.