Re: [isabelle] a new power operator



hi,

as far as I understand now, (THE x. False) is treated by the system as some
real number, fixed but unknown. u can prove things about it only if they
hold for all reals. this is quite satisfactory for me. also, I think the
behavior of 'powr' for negative base is quite similar- it is defined using
the logarithm of the base which is "undefined" in a very similar way. this
is different in Coq, where the real power behaves like u said and for
negative base returns 1.

thanx, noam



On Fri, Sep 18, 2015 at 9:49 AM, Johannes HÃlzl <hoelzl at in.tum.de> wrote:

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