*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Approximation tactic for very large numbers*From*: Fabian Immler <immler at in.tum.de>*Date*: Wed, 7 Mar 2018 11:28:57 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4623bbc4-4f2a-bfb9-cf2c-5ef40694faac@in.tum.de>*References*: <a14488f0-722c-7ffb-625f-bb17591edd8d@in.tum.de> <6FC44817-43DF-46A9-A355-17A532C83B7A@in.tum.de> <4623bbc4-4f2a-bfb9-cf2c-5ef40694faac@in.tum.de>

> Am 05.03.2018 um 12:33 schrieb Manuel Eberl <eberlm at in.tum.de>: > > 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. We actually do something similar in quickcheck[approximation] (~~/src/HOL/Decision_Procs/approximation_generator.ML): Trying to find counterexamples with IEEE floating point arithmetic and certifying them by approximation. > > 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. Yes, this would be a solution. One could also think of computing the bounds with IEEE floating point numbers. >> 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 >

**Attachment:
smime.p7s**

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

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

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

- Previous by Date: [isabelle] 16 PhD Positions on Logical Methods in Computer Science 30 percent for Female Candidates
- Next by Date: [isabelle] Nested locales
- Previous by Thread: Re: [isabelle] Approximation tactic for very large numbers
- Next by Thread: [isabelle] Annoying message about "unknown files"
- 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