Re: [isabelle] finished proof contains coloured proof method



Hi Gergely,

> the purple colour means that a prover process is still running.

proofs in Isar are "forked" by default. That means if you state a
proposition with "have" or "show", it will run the proof (in your
example, using "by") in the background. In order to increase
parallelism, it'll continue processing the remaining theory. It does
that by optimistically assuming that the proof will proceed, hence
"asserting" the statement. To notify the user that there are still some
pending proofs, Isabelle/jEdit uses the purple background.

> Is this a valid proof? Can I simply ignore this colouring?

No, you can't. The system continues processing the rest of your theory
so that you can go on with your work, but that doesn't mean you can just
assume that everything still pending is ultimately correct.

Obviously the system doesn't know how long it should wait for the proof
to complete. That's up to the user to decide.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.