[isabelle-dev] Circular reasoning via multithreading seems too easy
makarius at sketis.net
Tue Dec 6 11:36:50 CET 2016
On 05/12/16 17:13, Ondřej Kunčar wrote:
> If you remove the call of the function Thm.name_derivation, the cycle gets caught. The function
> is internally used in Goal.prove_future. It seems that the promises of the theorem in question
> are dropped in the function but we don’t understand whether this was intended or not.
This is what I have explained already abstractly: there is a conceptual
conflict of proof futures vs. proof terms (via
Usually everything that is trivial or easy works properly in Isabelle.
Only hard problems are open, sometimes for years.
There might be a quick "fix", but such surgery usually degrades the
overall system quality. Isabelle development follows a different model.
More information about the isabelle-dev