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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and