Re: [isabelle] Proof mode still on after failed by (Isabelle 2013-RC2)



On Mon, 4 Feb 2013, Joachim Breitner wrote:

I installed 2013-RC2 to play around and see what has changed, and found
this issue:

       theory Scratch imports Main
       begin
       lemma "True"
         by (rule conjI)
       lemma "True ∨ True"
        sorry
       end

works fine, i.e. despite the "by" command failing to prove the lemma, Isabelle still accepts the following "lemma" command. So "by" managed to switch from proof mode to theory mode. This is good and important for non-linear proof editing.

This tiny little bit of structural error handling in 'by' steps is merely an indirect effect of its default policy to fork the proof step. So any failures in the forked part are deferred.


But this does not work reliably. With just a small small change, such as
giving the lemma a name:

       theory Scratch imports Main
       begin
       lemma name: "True"
         by (rule conjI)
       lemma "True ∨ True"
        sorry
       end

the "lemma" command is now under-wiggled and shows the error message “Illegal application of command "lemma" in proof mode”. I was expecting the same behavior as above.

There is a nother effect involved here: for historical reasons, the proof-ending that is implicit in the 'by' step does the name binding for the result. That fails here, but on the surface, not in the forked part.


Proper structured proof checking is still something to be done in the (near) future. It is important for systematic proof construction in the editor. Such funny effects will then go away.

Right now you can also try parallel_proofs=0 instead of the default 2 (e.g. via Isabelle/jEdit plugin options). The error behaviour should then be mostly that of Isabelle2012. You are loosing potential for parallel proof checking, though.


	Makarius


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