Re: [isabelle] proof terms & program extraction
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?
On Fri, Oct 24, 2014 at 2:30 PM, Stefan Berghofer <berghofe at in.tum.de>
> On 10/23/2014 11:28 AM, Daniel Weller wrote:
>> 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
>> I found some information on that (maybe explicit proof terms have not been
>> generated by Isabelle?), but it seems outdated:  gives a solution to
>> problem, but I could not apply that to the current version of Isabelle
>> ("Isabelle -> Settings -> Full Proofs" does not exist in the jEdit IDE,
>> "usedir" tool does not exist anymore, ...)
> Hi Daniel,
> it should be sufficient to start Isabelle/jEdit with the HOL-Proofs image,
> 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
> * 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and