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

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.

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

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

- Previous by Date: Re: [isabelle] some problems with the /\ quantifier
- Next by Date: Re: [isabelle] a new power operator
- Previous by Thread: [isabelle] a new power operator
- Next by Thread: Re: [isabelle] a new power operator
- 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