This was an artificial counterexample, which I tried out of curiosity, but having applications like caching of already proved theorems in mind.<br><br>Peter<div class="quote" style="line-height: 1.5"><br><br>-------- Originalnachricht --------<br>Betreff: Re: [isabelle-dev] Circular reasoning via multithreading seems too easy<br>Von: Makarius <makarius@sketis.net><br>An: Peter Lammich <lammich@in.tum.de>,isabelle-dev <isabelle-dev@in.tum.de><br>Cc: <br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 03/12/16 14:57, Peter Lammich wrote:<br>> <br>> the attached theory is accepted by all Isabelle's from 2015 to the<br>> latest 2016-1-RC4, without any complaints, even in batch mode <br>> (isabelle build). <br>> It just uses a prove_future, and proves the theorem with itself!<br><br>The behaviour is the same in Isabelle2014 and Isabelle2013, which<br>conforms to my intuition about this aspect of the system. It also means<br>it is not a regression, so not relevant for the Isabelle2016-1 release.<br><br>I can't say on the spot what is going on, and if there is a genuine<br>error somewhere, but I can imagine a conflict of the existing dependency<br>check of proof promises with PThm boxes of proof terms.<br><br>In general, the thm type in Isabelle is definitely not what is being<br>told in the common story about the "LCF approach", there is also not<br>"the kernel" in Isabelle. We need to stop telling these tales.<br><br><br>Did you encounter this situation in an actual application, or is it an<br>artificially constructed counter-example? That makes an important<br>difference, because it is theoretically obvious that Isabelle is not<br>100% correct (just like Coq, HOL-Light, ...).<br><br><br> Makarius<br><br></blockquote></div>