Re: [isabelle] a new power operator



Hi Noam,

yes THE x. False, SOME x. False, SOME x. True, undefined. This are all
fixed but unknown values. The main reason I prefer a default value like
0 is that such functions are easier to handle.

For example to prove measurability of ln, or log one needs to prove that
the ln is _constant_ for x <= 0. So now "THE x. False" is not an
arbitrary value but this specific one. Imagine ln was defined to be
  ln = SOME f. f = the_inv_on {0 <..} exp
then we can prove measurability only for the non-negative reals, which
is very annoying.

TL;DR using THE x. False or any other 'undefined' value is annoying and
does not buy you anything...

 - Johannes




Am Freitag, den 18.09.2015, 10:00 +0300 schrieb noam neer:
> 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.