*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] proof terms & program extraction*From*: Daniel Weller <fraini at gmail.com>*Date*: Tue, 28 Oct 2014 11:12:46 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <544A464C.9030001@in.tum.de>*References*: <CA+aehLiwto30-tKaVho4S7HrRsLFcre=twy8giW984P6QjXs+w@mail.gmail.com> <544A464C.9030001@in.tum.de>

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

**References**:**[isabelle] proof terms & program extraction***From:*Daniel Weller

**Re: [isabelle] proof terms & program extraction***From:*Stefan Berghofer

- Previous by Date: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Date: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Previous by Thread: Re: [isabelle] proof terms & program extraction
- Next by Thread: [isabelle] Easier quick PDF generation possible?
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list