Re: [isabelle] Approximation tactic for very large numbers

> Am 05.03.2018 um 12:33 schrieb Manuel Eberl <eberlm at>:
> 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
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.