*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] a new power operator*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 18 Sep 2015 09:12:53 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAGOKs08bmKvQVFzsBrjOV3KBq1YL7H4Q+Aj-ykbN6peMoDqFhA@mail.gmail.com>*Organization*: TU München*References*: <CAGOKs0955JAEf75HD4oBTn0L+4nwvLVS1_O-qyn_qw7RXCvhog@mail.gmail.com> <1442558980.21178.27.camel@in.tum.de> <CAGOKs08bmKvQVFzsBrjOV3KBq1YL7H4Q+Aj-ykbN6peMoDqFhA@mail.gmail.com>

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

**References**:**[isabelle] a new power operator***From:*noam neer

**Re: [isabelle] a new power operator***From:*Johannes Hölzl

**Re: [isabelle] a new power operator***From:*noam neer

- Previous by Date: Re: [isabelle] a new power operator
- Next by Date: Re: [isabelle] some problems with the /\ quantifier
- Previous by Thread: Re: [isabelle] a new power operator
- Next by Thread: Re: [isabelle] Isabelle Foundation & Certification
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list