Re: [isabelle] Finding the instantiation of a variable



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 think in general the answer is no, since auto may perform classical reasoning. In special cases, this may be possible but is certainly not trivial. You would probably have to study some decent proof theory...

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.

I am surprised by this myself. I would also have expected a full proof here. Maybe someone else has an idea?

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?

You can read about the format of proof terms in the paper that I mentioned. From this, I guess, you will have to work out the details yourself (starting from a precise problem definition), since it hasn't been done yet AFAIK.

Alex





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