[isabelle] Approximation tactic for very large numbers



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




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