Knowing when an Isar-style proof is actually valid in Isabelle

Question

I am working on an exercise while trying to learn the Isar language. I have the following script for a lemma about lists.

lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length zs + 1)"
proof -
show ?thesis by blast (* L *) 
qed

Isabelle seems to accept this, but there are some things confusing me.

First, although Isabelle states "Successful attempt to solve goal" and "No subgoals!" at position (* L *), the string "by blast" continues to be highlighted, which suggests to me that this method has not terminated. Is this the case? If so, is my proof actually valid according to Isabelle?

In general, I have noticed that if I write anything at all in place of "blast" in my script, then Isabelle will state the same things in the output except that it may also state at the bottom in red that there is some failure. Even so, if I write "qed" afterwards, Isabelle seems to accept the lemma as proved. What is going on here? How exactly do I know when my proof is considered valid?

Any insight is much appreciated!

Answer 1

If some method did not terminate, or there is some explicit failure message, then your proof is not accepted. Just the parallel processing of the prover-IDE permits you to continue as if the proof would have been successful.

To check whether all of your proofs are okay, the safest way is to run isabelle build, or you can inspect in the theory panel in Isabelle/jEdit, whether your theory got a bold black border, which also indicates successful processing.