Search code examples
isabelle

Are purple colored Isabelle proofs valid?

I've a Metis proof acquired by Sledgehammer highlighted in purple color. What does its being highlighted mean exactly? The proof seems valid; is it indeed?

Solution

  • Purple means that the metis call is still running. There are three possible outcomes:

    • metis finishes: the proof is valid (no background) ;
    • metis fails: the proof is invalid (red background) ;
    • metis does not terminate: The proof is invalid (purple background remains forever).

    Isabelle is multithreaded and it is only once all previous tactics have finished that you are safe.

    The time you decide to wait is up to you, but more that a few seconds usually means that you have to rerun Sledgehammer...