Discussion:
[isabelle] using oops in document preparation
(too old to reply)
Gergely Buday
2016-07-12 10:22:58 UTC
Permalink
Raw Message
Hi,



I have



lemma "¬ False"

proof (simp only: ) (*<*) oops (*>*)



which leads to the



Failed to apply initial proof method



error message in the interactive development.



oops recovers from the error and I can write other theorem statements.



The Isabelle/Isar reference manual writes:



A typical application of oops is to explain Isar proofs within the system
itself,

in conjunction with the document preparation tools of Isabelle described in

chapter 4. Thus partial or even wrong proof attempts can be discussed in a

logically sound manner. Note that the Isabelle LaTeX macros can be easily

adapted to print something like “...” instead of the keyword “oops”.



When I use



isabelle build –D .



I get the same error as above and no output is produced.



I tried –o quick_and_dirty but in vain.



How can I include failed proof attempts into a proof document?



I use Isabelle2016.



- Gergely
Makarius
2016-07-12 10:46:43 UTC
Permalink
Raw Message
Post by Gergely Buday
lemma "¬ False"
proof (simp only: ) (*<*) oops (*>*)
oops recovers from the error and I can write other theorem statements.
When I use
isabelle build –D .
I get the same error as above and no output is produced.
Batch build is strict about errors and won't recover.
Post by Gergely Buday
How can I include failed proof attempts into a proof document?
I use Isabelle2016.
I recommend the new document antiquotation @{theory_text} (see also NEWS).


Makarius
Andreas Lochbihler
2016-07-12 10:52:05 UTC
Permalink
Raw Message
Hi Gergely,

You can only generate documents from theories in which no errors occur during processing.
Failed proof attempts in the documentation mean that you start a proof and decide to abort
it, but all the proof steps before the oops must succeed.

If you want to print failing proof attempts in the document, too, you need a bit more of
cheating. You can make every proof method succeed by adding "?". So

lemma "~ False"
proof (simp only: )(*<*)?(*>*) (*<*) oops (*>*)

should do the job.

Hope this helps,
Andreas
Post by Gergely Buday
Hi,
I have
lemma "¬ False"
proof (simp only: ) (*<*) oops (*>*)
which leads to the
Failed to apply initial proof method
error message in the interactive development.
oops recovers from the error and I can write other theorem statements.
A typical application of oops is to explain Isar proofs within the system
itself,
in conjunction with the document preparation tools of Isabelle described in
chapter 4. Thus partial or even wrong proof attempts can be discussed in a
logically sound manner. Note that the Isabelle LaTeX macros can be easily
adapted to print something like "..." instead of the keyword "oops".
When I use
isabelle build -D .
I get the same error as above and no output is produced.
I tried -o quick_and_dirty but in vain.
How can I include failed proof attempts into a proof document?
I use Isabelle2016.
- Gergely
Loading...