Re: [isabelle] Obtaining the instantiation of variables in a proof



On Wed, Apr 15, 2009 at 10:53 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:

> Stephy Wong wrote:
> > Hi all,
> >
> > Given the trivial proof for EX x. x >' 0' by using the axiom 1' >' 0', is
> > there a way to see by which term x is instantiated (by 1' in this case)?
> Can
> > this be done in PG? If not, how can this be done in ML?
> >
> > Thanks
> >
> > Steph
> >
> If your goal is an EX, you can provide the witness by instantiating the
> exI thm before use:
>
> apply(rule_tac x = "1'" in exI)
>
> Pls read Section 5.9, Quantifiers, of the Tutorial.


Thanks. What I actually meant is that is it possible to obtain the
instantiation(s) that Isabelle has found automatically? The example I gave
is a trivial one that Isabelle can proof automatically, but I'm interested
in seeing how Isabelle instantiates the theorem. Does this need to be done
in ML? Sorry for the confusion.

Thanks

Steph


>
>
> Tobias
>




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