Re: [isabelle] Finding the instantiation of a variable



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




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