Re: [isabelle] Proofability of a simple existential statement



Isabelle uses higher-order unification to solve such problems. I expect that Isabelle instantiates func with the identity function and arg with 0. You might want to try more complicated examples to see the extent of what can be done automatically.
Larry Paulson


On 3 Jun 2010, at 01:35, Steve W wrote:

> I have a quick, basic question: How come the following is provable, without
> the need of any fact:
> 
> lemma exzero: "EX func arg. func arg = 0"
> by auto
> 
> How are func and arg instantiated?
> 
> Thank you for any help in advance.
> 
> Steve






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