*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Approximation tactic for very large numbers*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 5 Mar 2018 12:33:50 +0100*In-reply-to*: <6FC44817-43DF-46A9-A355-17A532C83B7A@in.tum.de>*References*: <a14488f0-722c-7ffb-625f-bb17591edd8d@in.tum.de> <6FC44817-43DF-46A9-A355-17A532C83B7A@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Ah sorry, I misread. Try it again with 160000. ;) My current workaround is to first do the computation in ML using hardware floating-point numbers. If the result is finite (i.e. not NaN or Infinity) and the proposition holds for the resulting numbers, I call approximation. It's not pretty and certainly not "complete", but it handles all of my use cases pretty well so far. The only proper solution I can think of would be to add some kind of precision for the exponent as well, and if an exponent exceeds that number, the computation is aborted with an error. > As a side note on the tactic in general, if you care about performance: In my experience, > you get good results (here about 5s) by setting the precision to about half the precision of the native integer type (i.e., 15 for x86 and 30 for x86_64). That's not an issue here since I chose 10 anyway. That's usually enough for my needs. Manuel

**Follow-Ups**:**Re: [isabelle] Approximation tactic for very large numbers***From:*Fabian Immler

**References**:**[isabelle] Approximation tactic for very large numbers***From:*Manuel Eberl

**Re: [isabelle] Approximation tactic for very large numbers***From:*Fabian Immler

- Previous by Date: Re: [isabelle] Approximation tactic for very large numbers
- Next by Date: [isabelle] Annoying message about "unknown files"
- Previous by Thread: Re: [isabelle] Approximation tactic for very large numbers
- Next by Thread: Re: [isabelle] Approximation tactic for very large numbers
- Cl-isabelle-users March 2018 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