Re: [isabelle] a new power operator



Hi Noam,

for 2. you can not enforce anything, if you chose (THE x. False) it may
be also = 0 or = 1, you just can not prove it. This makes only sense if
you want to have the option to change the value later on. In a total
logic like HOL we usually fix it to a default value, like 0 (or in this
case 1).

I think a simpler definition of mrpow would be:
   x ** y = (if y : Nats then x ^ nat (floor y)
        else if - y : Nats then (1 / x) ^ nat (floor (-y))
        else x powr y)

Then you can prove:
  0 < x ==> x ** y = x powr y
  x ** real n = x ^ n
  x ** - real n = (1 / x) ^ n

Of course you get x ** 0 = 1, but just imagine that
(THE x. False) = 1 ;-)

Another question is: 
  What are your application for this operator?

Maybe an extension of ^ to integers would be enough?

ipow :: 'a::field => int => 'a
ipow x 0 = 1
ipow x (- n) = (1 / x) ^ n
ipow x (+ n) = x ^ n

  - Johannes



Am Mittwoch, den 16.09.2015, 20:29 +0300 schrieb noam neer:
> hi,
> 
> 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
> analysis.)
> 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.