The point is that the claim is not a theorem, because it would need a contradiction rule in Pure. Note that auto, metis, etc. also fail.
One could consider modifying blast to forbid all variables of type prop. That may be overkill, however. I can’t think of a reason to devote much effort to handling this sort of example. Larry On 7 Jan 2014, at 23:32, Makarius <[email protected]> wrote: > On Tue, 31 Dec 2013, Lawrence Paulson wrote: > >> (1) Do we need a general way to prevent warnings from breaking interfaces? >> That would be great, if possible, and maybe just requires inserting some >> sort of pause between messages to allow their interruption, or some way to >> count messages and stop them after a limit is exceeded. > > Already since 2001 we have the Output.tracing channel, which is intended for > potentially unbounded and usually less interesting high-volume output, with > some special treatment in the front-end. That was originally done for Proof > General. > > The current Isabelle/jEdit implementation of that stops emitting tracing > messages after the limit given by system option editor_tracing_messages is > exceeded (for each command transaction separately). Afterwards it waits for > the user clicking on the output to stop or continue. This is a bit awkward, > but avoids bombing the front-end. Although sometimes surprises remain about > executions that should continue, but actually wait. > > > I have now modernized blast.ML a bit, to warp it from 1997 into 2001 in that > respect. See also Isabelle/ed36358c20d5. > > You can try it like this: > > setup {* Config.put_global Blast.trace true *} > > lemma "(⋀P. P::bool) ⟹ PROP P" by blast > > With Blast.trace = false, that example loops without emitting anything, just > some ambient heating via CPU power. Bombing no longer happens in that > version. I have also made one separate warning subject to context > visibility, which is quite common these days. > > So for my part, the issue is resolved. You should nonetheless take a look if > it is possible to get the treatment of Trueprop vs. non-Trueprop right. If > the left-over development tool of Blast.trace is of any use, it should point > out the situation. (In general, cumulative maintenance costs over the years > are greatly reduced by removing built-in tracing once things are properly > implemented. Such add-ons greatly complicate the code and are hard to get > right in the first place.) > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
