*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] ln on negative numbers*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Thu, 30 Apr 2015 08:54:49 +0200*In-reply-to*: <55411707.5060106@in.tum.de>*Organization*: TU München*References*: <5540E488.6070106@in.tum.de> <1430328335.11504.5.camel@lapnipkow5> <55411707.5060106@in.tum.de>

Am Mittwoch, den 29.04.2015, 19:38 +0200 schrieb Manuel Eberl: > I have no idea what you mean by a carrier set. For O(g::'a => 'b) a set-based restriction on the type 'a. > The definition of O is currently > `O(g) = {f. (âc>0. eventually (Îx. Âf xÂ â c * Âg xÂ) at_top)} > > I don't see how that could be augmented by a carrier set in a useful way. Ah I see; I thought the problem was not only related to c but also to x. > A generalisation to other filters than at_top would be straightforward, > but I decided not to do that quite yet because I don't need it yet. Yup. - Johannes > On 29/04/15 19:25, Johannes HÃlzl wrote: > > I don't object to give ln a known value for negative numbers. > > > > But I also think you need to add a carrier set (like a O_on A f) to your > > O-notation! Many definitions in Isabelle/HOL nowadays have it. > > Btw: if you integrate filters into your O-notation this is not necessary > > any more, as this is taken care of by the "at _ within _" filter. > > > > - Johannes > > > > Am Mittwoch, den 29.04.2015, 16:02 +0200 schrieb Manuel Eberl: > >> Hallo, > >> > >> I am currently in the process of writing some automation for Landau > >> symbols. One of the problems that I currently have is that I would like > >> to rewrite things like > >> > >> O(Îx. (c*x) powr p) > >> > >> to > >> > >> O(Îx. c powr p * x powr p) > >> > >> However, for c < 0 this is simply not true (well, morally not true). If > >> c < 0, and w.l.o.g. x > 0, we have > >> > >> c powr p = (c*x) powr p = exp (p * THE u. False) > >> > >> > >> I therefore suggest to define the real logarithm as "ln x = (if x â 0 > >> then 0 else THE u. exp u = x)". The practical implications of this > >> should be small, and it would allow stating a lot of lemmas involving > >> "powr" in a much simpler form and allow transformations such as the one > >> above. > >> > >> Cheers, > >> > >> Manuel > >> > > > > >

**References**:**[isabelle] ln on negative numbers***From:*Manuel Eberl

**Re: [isabelle] ln on negative numbers***From:*Johannes Hölzl

**Re: [isabelle] ln on negative numbers***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] ln on negative numbers
- Next by Date: Re: [isabelle] ln on negative numbers
- Previous by Thread: Re: [isabelle] ln on negative numbers
- Next by Thread: Re: [isabelle] ln on negative numbers
- Cl-isabelle-users April 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