*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Finding the instantiation of a variable*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Mon, 12 Jul 2010 15:51:34 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTimZ9yLWnR7XFXoAzNKmkHvn0bSOvd_XKT-J4qtW@mail.gmail.com>*References*: <AANLkTinrTaBPr1dIqPvVJgyJOBL92-jnc7TRXA_1wFYg@mail.gmail.com> <AANLkTimZ9yLWnR7XFXoAzNKmkHvn0bSOvd_XKT-J4qtW@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Steve,

Does anyone know how one would go about finding the instantiation of a variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x. f x > 0', how do I work with the proof term in order to find the instantiations of 'f' and 'x'?

There are at least two ways in which your question can be understood:

Stefan Berghofer. Program Extraction in simply-typed Higher Order Logic. TYPES 2002 http://www4.informatik.tu-muenchen.de/~berghofe/papers/TYPES2002.pdf

Would the first step be to reconstruct the proof using Reconstruct.reconstruct_proof? If so, what would subsequent steps involve?

Any help will be appreciated.

Alex

**Follow-Ups**:**Re: [isabelle] Finding the instantiation of a variable***From:*Steve W

**References**:**[isabelle] Finding the instantiation of a variable***From:*Steve W

**Re: [isabelle] Finding the instantiation of a variable***From:*Steve W

- Previous by Date: Re: [isabelle] Finding the instantiation of a variable
- Next by Date: Re: [isabelle] x-symbols and AFS?
- Previous by Thread: Re: [isabelle] Finding the instantiation of a variable
- Next by Thread: Re: [isabelle] Finding the instantiation of a variable
- Cl-isabelle-users July 2010 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