Re: [isabelle] proof terms & program extraction



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

On Fri, Oct 24, 2014 at 2:30 PM, Stefan Berghofer <berghofe at in.tum.de>
wrote:

> 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
>> 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
>
>
>



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