*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Finding the instantiation of a variable*From*: Steve W <s.wong.731 at gmail.com>*Date*: Tue, 13 Jul 2010 13:08:56 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C3B1DE6.4040305@in.tum.de>*References*: <AANLkTinrTaBPr1dIqPvVJgyJOBL92-jnc7TRXA_1wFYg@mail.gmail.com> <AANLkTimZ9yLWnR7XFXoAzNKmkHvn0bSOvd_XKT-J4qtW@mail.gmail.com> <4C3B1DE6.4040305@in.tum.de>

Hi Alexander, On Mon, Jul 12, 2010 at 2:51 PM, Alexander Krauss <krauss at in.tum.de> wrote: > 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: > > a) Given a proof of "EX x. P x", you want to extract the term "t" that was > used to prove the existential statement > > b) Given a proof of "EX x. P x", you want to find any term t such that "P > t" holds. > > > to a) This is not possible in general. Note that Isabelle/HOL implements > classical logic, which allows existential statements without providing the > values that are proved to exists. So there is no "instantiation" that can be > extracted, at least in general. You can find a simple example of such a > proof (of the well-known Drinker's Principle) in the file > "HOL/Isar_Examples/Drinker.thy". > I think my situation is similar to a). How about in the following: axiomatization f :: "real => real" and c :: real where ax1: "f c = 0" lemma lem1: "EX x. f x = 0" using ax1 apply auto done 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? Thanks again. Steve

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

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

- Previous by Date: Re: [isabelle] locales and 'types'
- Next by Date: Re: [isabelle] finite sets and code generation, once again
- 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