*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Approximation tactic for very large numbers*From*: Fabian Immler <immler at in.tum.de>*Date*: Mon, 5 Mar 2018 10:30:20 +0100*Cc*: Manuel Eberl <eberlm at in.tum.de>*In-reply-to*: <a14488f0-722c-7ffb-625f-bb17591edd8d@in.tum.de>*References*: <a14488f0-722c-7ffb-625f-bb17591edd8d@in.tum.de>

Hi Manuel, Your concrete example should not be out of reach of the approximation tactic. On my Mac, I can do e.g., lemma "exp (exp 16000 :: real) > 0" by (approximation 80) which proves the goal in about 10s (both in 32 and 64 bit mode). Therefore I am not sure if it is really the large exponents that pose the problem here. 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). Fabian > Am 03.03.2018 um 14:25 schrieb Manuel Eberl <eberlm at in.tum.de>: > > Hallo, > > I noticed that the approximation tactic behaves very poorly when the > input is very large. For instance, attempting to prove "exp (exp 16000 > :: real) > 0" with it results in the tactic running for about a minute > or two before. The entire Isabelle system becomes unresponsive and > eventually stops with one of Isabelle/jEdit's "total existence failure" > messages. > > Now, obviously, I am not expecting the tactic to be able to prove this – > it uses software floating-point numbers and the exponents here are > staggeringly large. However, I am wondering if it is possible to make > the tactic fail gracefully, or at least not take down the entire system. > Otherwise it is highly problematic to use this tactic as a solver in the > background, which I intend to do. > > Manuel >

**Attachment:
smime.p7s**

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

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

- Previous by Date: Re: [isabelle] 1/0 = 0?
- Next by Date: Re: [isabelle] Approximation tactic for very large numbers
- 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