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"
apply (rule exI [where x = c])
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and