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



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.

Tobias





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