Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof mode still on after failed by (Isabelle ...

Email Gateway (Aug 19 2022 at 10:06):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 19 2022 at 10:15):

From: Joachim Breitner <breitner@kit.edu>
Hi,

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.

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.

Greetings,
Joachim
signature.asc

Last updated: Apr 26 2024 at 16:20 UTC