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

[Makarius]

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
close_derivation/name_derivation).

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.


	Makarius