*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*: Sun, 18 Jul 2010 23:25:11 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <AANLkTimT1qdp2v436l9VmLeGGZKZgfnmJvfuB0SevMd0@mail.gmail.com>*References*: <AANLkTinrTaBPr1dIqPvVJgyJOBL92-jnc7TRXA_1wFYg@mail.gmail.com> <AANLkTimZ9yLWnR7XFXoAzNKmkHvn0bSOvd_XKT-J4qtW@mail.gmail.com> <4C3B1DE6.4040305@in.tum.de> <AANLkTimT1qdp2v436l9VmLeGGZKZgfnmJvfuB0SevMd0@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Steve W wrote:

Can one extract the term that was used to prove the existential statement by auto? I.e., that term should be 'c' due to ax1.

I've tried running 'full_prf' after 'apply auto', but I get an error about 'minimal proof object' even I have Full Proof switched on in PG.

Does auto instantiate the existential variable to 'c'? Now, if I have the following instead: lemma lem1: "EX x. f x = 0" using ax1 apply (rule exI [where x = c]) done full_prf gives: protectI % EX x::real. f x = (0::real) %% (exI % TYPE(real) % (%a::real. f a = (0::real)) % c %% (OfClass type_class % TYPE(real)) %% thm.Test.ax1) It's clearer now that 'x' is instantiated to 'c' (because the instantiation is explicit in the proof), which is a lambda term. However, how should 'c' be extracted from the proof?

Alex

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

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

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

**Re: [isabelle] Finding the instantiation of a variable***From:*Alexander Krauss

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

- Previous by Date: [isabelle] Conflicting locales with a common signature
- Next by Date: [isabelle] Questions about Isabelle
- 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