[isabelle] proof terms & program extraction

[Daniel Weller]

Dear all,

I'd like to try out the Isabelle program extraction mechanism "extract",
but I have been unsuccessful so far.

I found examples for this mechanism in
Isabelle2014/src/HOL/Proofs/Extraction, but trying e.g. Euclid.thy, I get
the error "reconstruct_proof: minimal proof object" on the line "extract
Euclid".

I found some information on that (maybe explicit proof terms have not been
generated by Isabelle?), but it seems outdated: [1] gives a solution to the
problem, but I could not apply that to the current version of Isabelle
("Isabelle -> Settings -> Full Proofs" does not exist in the jEdit IDE, the
"usedir" tool does not exist anymore, ...)

I'd really appreciate any pointers on how to use this feature with the
current version of Isabelle.

Best,
Daniel

[1] https://groups.google.com/forum/#!topic/fa.isabelle/rASlPIW8i_Y

[Stefan Berghofer]

Post by Daniel Weller
Dear all,
I'd like to try out the Isabelle program extraction mechanism "extract",
but I have been unsuccessful so far.
I found examples for this mechanism in
Isabelle2014/src/HOL/Proofs/Extraction, but trying e.g. Euclid.thy, I get
the error "reconstruct_proof: minimal proof object" on the line "extract
Euclid".
I found some information on that (maybe explicit proof terms have not been
generated by Isabelle?), but it seems outdated: [1] gives a solution to the
problem, but I could not apply that to the current version of Isabelle
("Isabelle -> Settings -> Full Proofs" does not exist in the jEdit IDE, the
"usedir" tool does not exist anymore, ...)

Hi Daniel,

it should be sufficient to start Isabelle/jEdit with the HOL-Proofs image, i.e.

isabelle jedit -l HOL-Proofs Euclid.thy

When using this image, it is no longer necessary to switch on proof objects
explicitly. See also the following NEWS entry for Isabelle2013-1 (November 2013):

* System option "proofs" has been discontinued. Instead the global
state of Proofterm.proofs is persistently compiled into logic images
as required, notably HOL-Proofs. Users no longer need to change
Proofterm.proofs dynamically. Minor INCOMPATIBILITY.

Note that compiling the HOL-Proofs image may require quite some time and memory.

Greetings,
Stefan

[Daniel Weller]

Hi Stefan,

thank you very much for your fast reply, using the HOL-Proofs image did
indeed do the trick!

If I understand correctly, the implementation of "extract" is based on a
variant of Kreisel's realizability interpretation. Hence I was not
surprised that when trying to extract programs from my own (classical)
proofs, the algorithm failed.

Hence I was wondering: Are you (or of course anyone else on the list) aware
of any work on implementing some functional interpretation of classical
proofs (e.g. by using double-negation + A-translation, or the Shoenfield
functional interpretation) in Isabelle?

Best,
Daniel

Post by Stefan Berghofer

Post by Daniel Weller
Dear all,
I'd like to try out the Isabelle program extraction mechanism "extract",
but I have been unsuccessful so far.
I found examples for this mechanism in
Isabelle2014/src/HOL/Proofs/Extraction, but trying e.g. Euclid.thy, I get
the error "reconstruct_proof: minimal proof object" on the line "extract
Euclid".
I found some information on that (maybe explicit proof terms have not been
generated by Isabelle?), but it seems outdated: [1] gives a solution to the
problem, but I could not apply that to the current version of Isabelle
("Isabelle -> Settings -> Full Proofs" does not exist in the jEdit IDE, the
"usedir" tool does not exist anymore, ...)

Hi Daniel,
it should be sufficient to start Isabelle/jEdit with the HOL-Proofs image, i.e.
isabelle jedit -l HOL-Proofs Euclid.thy
When using this image, it is no longer necessary to switch on proof objects
* System option "proofs" has been discontinued. Instead the global
state of Proofterm.proofs is persistently compiled into logic images
as required, notably HOL-Proofs. Users no longer need to change
Proofterm.proofs dynamically. Minor INCOMPATIBILITY.
Note that compiling the HOL-Proofs image may require quite some time and memory.
Greetings,
Stefan