[isabelle-dev] Circular reasoning via multithreading seems too easy

[Makarius]

On 03/12/16 14:57, Peter Lammich wrote:
> 
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode 
> (isabelle build). 
> It just uses a prove_future, and proves the theorem with itself!

The behaviour is the same in Isabelle2014 and Isabelle2013, which
conforms to my intuition about this aspect of the system. It also means
it is not a regression, so not relevant for the Isabelle2016-1 release.

I can't say on the spot what is going on, and if there is a genuine
error somewhere, but I can imagine a conflict of the existing dependency
check of proof promises with PThm boxes of proof terms.

In general, the thm type in Isabelle is definitely not what is being
told in the common story about the "LCF approach", there is also not
"the kernel" in Isabelle. We need to stop telling these tales.


Did you encounter this situation in an actual application, or is it an
artificially constructed counter-example? That makes an important
difference, because it is theoretically obvious that Isabelle is not
100% correct (just like Coq, HOL-Light, ...).


	Makarius